فرض کنید دو نقطهٔ یک منوی تلفنی، اکنون همان پیامِ قابل‌مشاهده را نشان می‌دهند. آیا می‌توان گفت رفتارشان یکسان است؟ شاید پس از دو انتخابِ دیگر، یکی به مسیرِ علامت‌خورده برسد و دیگری نرسد. یک آزمایشِ مفید، دنباله‌ای از انتخاب‌هاست که این تفاوت را آشکار کند. در این درس، چنین شاهدی را برای یک جدولِ کوچک و کاملاً داده‌شده پیدا می‌کنیم؛ سپس روشن می‌کنیم چرا نبودنِ شاهد در این مدل، مجوزِ ادغامِ منوهای واقعی نیست.

۱. ظاهرِ یکسانِ دو منو، رفتارِ آیندهٔ یکسان نیست

دو درِ بی‌نوشته با نمای یکسان و محفظه‌های داخلیِ متفاوت
تصویر مفهومی: دو درِ بی‌نوشته با نمای یکسان و محفظه‌های داخلیِ متفاوت؛ بدون مقیاس عددی و مستقل از نتایج اجرای کد.

مدلِ ما بین یک تا شش حالت دارد. از هر حالت، برای هر یک از دو نمادِ انتزاعیِ صفر و یک، دقیقاً یک حالتِ بعدی تعیین شده است. هر حالت نیز یک پرچمِ مشاهدهٔ صفر یا یک دارد؛ مثلاً برچسبی آزمایشی که طراح برای یک مسیر انتخاب کرده است. این پرچم، معنای موفقیتِ تماس، دسترسیِ مجاز، پاسخِ کارشناس یا کیفیتِ صوت ندارد. نمادهای ورودی نیز رویدادِ واقعیِ DTMF یا زمانِ سپری‌شده نیستند. جدول، دادهٔ آزمایش است و از سامانهٔ بیرونی کشف نمی‌شود.

دو حالت زمانی هم‌ارزند که برای هر ادامهٔ متناهی از ورودی‌ها، پرچمِ انتهاییِ برابر بدهند. خودِ دنبالهٔ خالی هم یک ادامه است؛ پس اگر پرچم‌های فعلی متفاوت باشند، همان لحظه تفاوت دیده می‌شود. اگر برابر باشند، باید رفتارِ آینده را بررسی کنیم. برابر بودنِ شمارهٔ حالت‌ها لازم نیست: دو ردیفِ متفاوت می‌توانند از نظرِ همین مشاهده، آیندهٔ یکسانی داشته باشند. برعکس، برابر بودنِ پرچمِ فعلی برای این نتیجه کافی نیست.

این پرسش با ابهامِ پیشوند در پارسرِ منوی چندرقمی فرق دارد. آنجا پایانِ کد با مهلت یا پایان‌دهنده مشخص می‌شد؛ اینجا ورودی از پیش به دو نماد تعبیر شده و هیچ ساعت یا بافرِ رقم نداریم. همچنین ماشینِ حالتِ ورودیِ نامعتبر IVR مسئولِ بودجهٔ خطا و مسیرِ جایگزین بود. برابریِ زبانِ مشاهده، آن سیاست‌ها را جایگزین نمی‌کند. این دو مطلب در نسخهٔ ذخیره‌شدهٔ منتشرشده مطالعه شده‌اند؛ وضعیتِ فعلیِ پیوندها در این اجرای آفلاین معلوم نیست.

۲. دنبالهٔ تمایز را روی دو حالت هم‌زمان دنبال کنیم

دو حاملِ مستقلِ نمونه با مجموعه‌های مشابهِ مهره‌های ورودیِ بی‌نوشته
تصویر مفهومی: دو حاملِ مستقلِ نمونه با مجموعه‌های مشابهِ مهره‌های ورودیِ بی‌نوشته؛ بدون مقیاس عددی و مستقل از نتایج اجرای کد.

برای مقایسهٔ دو حالت، آن‌ها را هم‌زمان جلو می‌بریم. هر گرهِ جست‌وجو یک جفتِ حالت است. با خواندنِ صفر، ستونِ صفرِ هر دو ردیف را دنبال می‌کنیم؛ برای یک نیز همین کار انجام می‌شود. اگر پرچم‌های جفت متفاوت شد، واژه‌ای که ما را به آن رسانده شاهدِ تمایز است. چون مقایسه متقارن است، جفت را با شمارهٔ کوچک‌تر در ابتدا نگه می‌داریم. این مرتب‌سازی، ترتیبِ نمادهای واژه را عوض نمی‌کند.

نمونهٔ دستی شش ردیف دارد: صفر به یک یا دو می‌رود؛ یک با هر ورودی به سه، و دو با هر ورودی به چهار می‌رود. حالت‌های سه، چهار و پنج در خودشان می‌مانند. پرچمِ چهار و پنج یک و بقیه صفر است؛ شروع از صفر است. برای مقایسهٔ صفر و یک، دنبالهٔ خالی و هر واژهٔ تک‌نمادی هنوز پرچمِ برابر می‌دهند. واژهٔ «یک، صفر» آن‌ها را به چهار و سه می‌رساند و تفاوت را آشکار می‌کند. واژه‌های کوتاه‌تر چنین کاری نمی‌کنند و دو واژهٔ هم‌طولِ پیش از آن نیز شاهد نیستند.

در همین نمونه، حالت‌های یک و سه هم‌ارزند: هر ادامه آن‌ها را در ناحیهٔ پرچمِ صفر نگه می‌دارد. اما سه و چهار همین اکنون متفاوت‌اند. حالتِ پنج از شروع دسترس‌پذیر نیست؛ بنابراین خروجیِ درس برای آن جفت یا کلاسِ هم‌ارزی نمی‌سازد. این حذف از دامنهٔ گزارش، به معنای معاف بودنِ ردیفِ پنج از اعتبارسنجی نیست. پرچمِ یک نیز پایانیِ جذب‌کننده فرض نمی‌شود؛ اگر جدول برای آن گذارِ خروجی داشته باشد، همان گذار اجرا می‌شود.

۳. کوتاه‌ترین شاهد و معنای نبودنِ شاهد

دو ابزارِ آزمون با طولِ متفاوت کنارِ بلوکِ شفافِ بررسیِ مفهومی
تصویر مفهومی: دو ابزارِ آزمون با طولِ متفاوت کنارِ بلوکِ شفافِ بررسیِ مفهومی؛ بدون مقیاس عددی و مستقل از نتایج اجرای کد.

جست‌وجوی پهنااول، ابتدا واژه‌های کوتاه‌تر را بررسی می‌کند. برای رفعِ تساوی، همواره فرزندِ صفر پیش از یک واردِ صف می‌شود؛ در نتیجه بین شاهدهای کوتاه‌ترین طول، ترتیبِ واژه‌نامه‌ای با صفرِ مقدم انتخاب می‌شود. نخستین رسیدن به هر جفت کافی است: اگر مسیرِ دیگری همان جفت را بسازد، آیندهٔ ممکن از آن نقطه تغییر نکرده و پیشوندِ دیرتر مزیتی ندارد. چرخه‌ها نیز مشکلی ایجاد نمی‌کنند، چون هر جفت فقط یک بار وارد صف می‌شود.

پایانِ صف بدونِ دیدنِ پرچم‌های متفاوت، صرفاً «در چند آزمون تفاوتی ندیدیم» نیست. همهٔ گره‌های دسترس‌پذیرِ گرافِ جفت‌ها پیموده شده‌اند و هر واژهٔ ممکن، مسیری در همین گراف دارد. پس در جدولِ داده‌شده هیچ ادامهٔ متناهی تمایز ایجاد نمی‌کند. مقدارِ بازگشتیِ None برای این وضعیت است. دنبالهٔ خالی، یعنی همین حالا تفاوت داریم و معنایی کاملاً مخالف دارد. محدودیتِ شش حالت باعث می‌شود این استدلالِ متناهی را بتوان با کدِ آموزشیِ ساده دنبال کرد؛ حدِ زمانیِ دلخواهی برای توقف نگذاشته‌ایم.

تعریفِ هم‌ارزی و انتشارِ تفاوت از جانشین‌ها در بخشِ کاملِ کمینه‌سازیِ درسِ Cornell آمده است. جهتِ اندیس‌ها در متنِ مثلثِ جدول و مقداردهیِ شبه‌کدِ همان صفحه یکدست نیست؛ بنابراین آن شبه‌کد را کپی یا اجرا نکرده‌ایم و ادعای هزینهٔ آن را به برنامهٔ خود نسبت نمی‌دهیم. صفحهٔ McCloskey در Scranton، رابطهٔ برابری برای واژه‌های با طولِ محدود و دلیلِ تثبیتِ افراز را توضیح می‌دهد. تاریخِ نخستین انتشارِ این دو صفحه معلوم نیست؛ عنوانِ نیم‌سالِ Cornell و تاریخِ دسترسی را باید از تاریخِ انتشار جدا نگه داشت.

۴. کدِ کامل و مرجعِ مستقلِ جدولِ واژه‌ها

ابزارِ جفتی و نوارهای نمونهٔ جدا برای دو روشِ مستقلِ بررسی
تصویر مفهومی: ابزارِ جفتی و نوارهای نمونهٔ جدا برای دو روشِ مستقلِ بررسی؛ بدون مقیاس عددی و مستقل از نتایج اجرای کد.

تابعِ عمومی، سه ورودیِ صریح می‌گیرد: جدولِ گذار، ردیفِ پرچم‌ها و حالتِ شروع. فقط tuple و int دقیق پذیرفته می‌شوند؛ bool، زیرکلاس، ورودیِ تنبل و تبدیلِ ضمنی مردودند. ابتدا تمامِ ردیف‌ها، حتی ردیف‌های دسترس‌ناپذیر، بررسی می‌شوند؛ سپس صف و جست‌وجو ساخته می‌شود. گزارش، رکوردها و tupleهای تغییرناپذیر دارد: حالت‌های قابل‌دسترسی، حالت‌های بیرونِ دسترسی، کلاس‌های مرتب و شاهدِ هر جفت. شماره‌گذاری و ترتیبِ خروجی قراردادی و تکرارپذیر است.

"""Finite supplied-menu observation equivalence; Python standard library only.

Symbols0/1 and observation0/1 are abstract integers, not real IVR events.
None is a proof of equivalence in this whole supplied table; () means the
current flags differ. No real menu transformation or implementation is tested.
"""
from collections import deque as _queue
from itertools import product
from typing import NamedTuple
import json
import platform
import sys

AUTHOR_MAIN_ENABLED = True


class PairWitness(NamedTuple):
    left: int
    right: int
    word: tuple[int, ...] | None


class MenuDistinctionReport(NamedTuple):
    reachable: tuple[int, ...]
    unreachable: tuple[int, ...]
    classes: tuple[tuple[int, ...], ...]
    witnesses: tuple[PairWitness, ...]


def _admit(transitions, observations, entry):
    if type(transitions) is not tuple:
        raise TypeError("transitions must be an exact tuple")
    n = len(transitions)
    if not 1 <= n <= 6:
        raise ValueError("state count must be1..6")
    for row in transitions:
        if type(row) is not tuple:
            raise TypeError("each row must be an exact tuple")
        if len(row) != 2:
            raise ValueError("each row needs symbols0 and1")
        for target in row:
            if type(target) is not int:
                raise TypeError("target must be an exact int")
            if not 0 <= target < n:
                raise ValueError("target outside supplied table")
    if type(observations) is not tuple:
        raise TypeError("observations must be an exact tuple")
    if len(observations) != n:
        raise ValueError("one observation per state is required")
    for flag in observations:
        if type(flag) is not int:
            raise TypeError("observation must be an exact int")
        if flag not in (0, 1):
            raise ValueError("observations must be0/1")
    if type(entry) is not int:
        raise TypeError("entry must be an exact int")
    if not 0 <= entry < n:
        raise ValueError("entry outside supplied table")
    return n


def _reachable(transitions, entry):
    seen = {entry}
    pending = _queue((entry,))
    while pending:
        state = pending.popleft()
        for target in transitions[state]:
            if target not in seen:
                seen.add(target)
                pending.append(target)
    return tuple(sorted(seen))


def _shortest_pair_word(transitions, observations, left, right):
    pending = _queue(((left, right, ()),))
    seen = {(left, right)}
    while pending:
        a, b, word = pending.popleft()
        if observations[a] != observations[b]:
            return word
        for symbol in (0, 1):
            x, y = transitions[a][symbol], transitions[b][symbol]
            pair = (x, y) if x <= y else (y, x)
            if pair not in seen:
                seen.add(pair)
                pending.append((pair[0], pair[1], word + (symbol,)))
    return None


def menu_distinction_report(transitions, observations, entry):
    """Validate the whole table, then report reachable Boolean languages.

    Each pair search visits a finite product graph. BFS and0-before1 order
    select a shortest word, then the lexicographically first such word.
    No library DFA, timeout, live call or unknown implementation is used.
    """
    n = _admit(transitions, observations, entry)
    reachable = _reachable(transitions, entry)
    witnesses = tuple(
        PairWitness(a, b, _shortest_pair_word(transitions, observations, a, b))
        for i, a in enumerate(reachable) for b in reachable[i + 1:]
    )
    equivalent = {(w.left, w.right) for w in witnesses if w.word is None}
    remaining = set(reachable)
    classes = []
    for state in reachable:
        if state not in remaining:
            continue
        block = tuple(q for q in reachable if q == state or (state, q) in equivalent)
        classes.append(block)
        remaining.difference_update(block)
    return MenuDistinctionReport(
        reachable, tuple(q for q in range(n) if q not in reachable),
        tuple(classes), witnesses,
    )


def word_table_reference(transitions, observations, entry, counters=None):
    """Independent test oracle for already valid fixtures, no product BFS.

    Original-graph Boolean Floyd closure supplies reachability. Every binary
    word through length n-1 is folded directly from each state. The finite
    partition-refinement theorem justifies that length bound; it is not an
    arbitrary search cutoff. No main validator/search helper is called here.
    """
    n = len(transitions)
    closure = [[i == j for j in range(n)] for i in range(n)]
    for i in range(n):
        for target in transitions[i]:
            closure[i][target] = True
    for middle in range(n):
        for source in range(n):
            for target in range(n):
                closure[source][target] = closure[source][target] or (
                    closure[source][middle] and closure[middle][target]
                )
    reachable = tuple(i for i in range(n) if closure[entry][i])
    words = tuple(word for size in range(n) for word in product((0, 1), repeat=size))
    signatures = []
    for start in range(n):
        flags = []
        for word in words:
            state = start
            for symbol in word:
                state = transitions[state][symbol]
            flags.append(observations[state])
            if counters is not None:
                counters['state_word_evaluations'] += 1
        signatures.append(tuple(flags))
    classes = []
    pending = list(reachable)
    while pending:
        leader = pending[0]
        block = tuple(q for q in pending if signatures[q] == signatures[leader])
        classes.append(block)
        pending = [q for q in pending if q not in block]
    witnesses = []
    for i, a in enumerate(reachable):
        for b in reachable[i + 1:]:
            first = next((word for word, x, y in zip(words, signatures[a], signatures[b]) if x != y), None)
            witnesses.append(PairWitness(a, b, first))
            if counters is not None:
                counters['reachable_pair_queries'] += 1
    return MenuDistinctionReport(reachable, tuple(i for i in range(n) if i not in reachable), tuple(classes), tuple(witnesses))


def _word(report, a, b):
    return next(row.word for row in report.witnesses if row.left == a and row.right == b)


def _rejects(args, expected):
    try:
        menu_distinction_report(*args)
    except Exception as error:
        return type(error) is expected
    return False


def run_example():
    checks = {}
    table = ((1, 2), (3, 3), (4, 4), (3, 3), (4, 4), (5, 5))
    flags = (0, 0, 0, 0, 1, 1)
    manual = menu_distinction_report(table, flags, 0)
    checks['manual_two_symbol_witness'] = (
        manual.classes == ((0,), (1, 3), (2,), (4,))
        and _word(manual, 0, 1) == (1, 0)
    )
    checks['None_is_not_empty_word'] = _word(manual, 1, 3) is None
    checks['unequal_current_flags_empty_word'] = _word(manual, 3, 4) == ()
    tie = menu_distinction_report(((2, 2), (3, 3), (2, 2), (3, 3), (0, 1)), (0, 0, 0, 1, 0), 4)
    checks['shortest_then_lexicographic_zero_first'] = _word(tie, 0, 1) == (0,)
    checks['unreachable_domain_excluded'] = (
        manual.reachable == (0, 1, 2, 3, 4) and manual.unreachable == (5,)
        and all(w.left != 5 and w.right != 5 for w in manual.witnesses)
    )
    cycle = menu_distinction_report(((1, 1), (0, 0)), (0, 0), 0)
    checks['cycle_exhaustion_proves_equivalence'] = cycle.classes == ((0, 1),) and _word(cycle, 0, 1) is None
    ring = tuple(((i + 1) % 6, (i + 1) % 6) for i in range(6))
    uniform = menu_distinction_report(ring, (1,) * 6, 0)
    checks['uniform_observation_single_class'] = uniform.classes == ((0, 1, 2, 3, 4, 5),)
    moving = menu_distinction_report(((1, 1), (0, 0)), (1, 0), 0)
    checks['observation_one_not_implicitly_absorbing'] = moving.reachable == (0, 1) and _word(moving, 0, 1) == ()

    counts = {'profiles': 0, 'state_word_evaluations': 0, 'reachable_pair_queries': 0}
    family_ok = True
    for flat in product(range(3), repeat=6):
        transitions = tuple((flat[2 * i], flat[2 * i + 1]) for i in range(3))
        for observations in product((0, 1), repeat=3):
            actual = menu_distinction_report(transitions, observations, 0)
            expected = word_table_reference(transitions, observations, 0, counts)
            family_ok = family_ok and actual == expected
            counts['profiles'] += 1
    checks['independent_word_table_family_ONE_group'] = family_ok and counts['profiles'] == 5832

    permutation = (4, 2, 0, 5, 1, 3)
    renamed_table = [None] * 6
    renamed_flags = [None] * 6
    for old in range(6):
        renamed_table[permutation[old]] = tuple(permutation[t] for t in table[old])
        renamed_flags[permutation[old]] = flags[old]
    renamed = menu_distinction_report(tuple(renamed_table), tuple(renamed_flags), permutation[0])
    mapped_classes = tuple(sorted(tuple(sorted(permutation[q] for q in block)) for block in manual.classes))
    rename_ok = renamed.classes == mapped_classes
    for witness in manual.witnesses:
        a, b = sorted((permutation[witness.left], permutation[witness.right]))
        rename_ok = rename_ok and _word(renamed, a, b) == witness.word
    checks['renaming_covariance_canonical_classes'] = rename_ok
    swapped = menu_distinction_report(tuple((b, a) for a, b in table), flags, 0)
    checks['symbol_swap_equivalence_not_lex_word_assumption'] = (
        swapped.classes == manual.classes and _word(swapped, 0, 1) == (0, 0)
        and swapped == word_table_reference(tuple((b, a) for a, b in table), flags, 0)
    )

    class IntSubclass(int):
        pass
    class TupleSubclass(tuple):
        pass
    valid = (((0, 0),), (0,), 0)
    invalids = [
        (([], (0,), 0), TypeError),
        ((TupleSubclass(((0, 0),)), (0,), 0), TypeError),
        (((), (), 0), ValueError),
        ((((0, 0),) * 7, (0,) * 7, 0), ValueError),
        ((([0, 0],), (0,), 0), TypeError),
        (((TupleSubclass((0, 0)),), (0,), 0), TypeError),
        ((((0,),), (0,), 0), ValueError),
        ((((0, 0, 0),), (0,), 0), ValueError),
        ((((True, 0),), (0,), 0), TypeError),
        ((((IntSubclass(0), 0),), (0,), 0), TypeError),
        ((((0.0, 0),), (0,), 0), TypeError),
        ((((-1, 0),), (0,), 0), ValueError),
        ((((1, 0),), (0,), 0), ValueError),
        ((((0, 0),), [0], 0), TypeError),
        ((((0, 0),), TupleSubclass((0,)), 0), TypeError),
        ((((0, 0),), (), 0), ValueError),
        ((((0, 0),), (0, 0), 0), ValueError),
        ((((0, 0),), (False,), 0), TypeError),
        ((((0, 0),), (IntSubclass(0),), 0), TypeError),
        ((((0, 0),), (2,), 0), ValueError),
        ((((0, 0),), (-1,), 0), ValueError),
        ((((0, 0),), (0,), False), TypeError),
        ((((0, 0),), (0,), IntSubclass(0)), TypeError),
        ((((0, 0),), (0,), 0.0), TypeError),
        ((((0, 0),), (0,), -1), ValueError),
        ((((0, 0),), (0,), 1), ValueError),
    ]
    checks['strict_types_shapes_bounds_and_caps'] = all(_rejects(args, expected) for args, expected in invalids)
    global _queue
    saved_queue = _queue
    queue_calls = []
    hooks = []
    def forbidden_queue(*args, **kwargs):
        queue_calls.append(1)
        raise AssertionError('queue constructed before whole admission')
    class Lazy:
        def __iter__(self):
            hooks.append('iter')
            raise AssertionError('iteration hook')
        def __index__(self):
            hooks.append('index')
            raise AssertionError('index hook')
    _queue = forbidden_queue
    try:
        late_ok = (
            _rejects((((0, 0), (1, 2)), (0, 1), 0), ValueError)
            and _rejects((((0, 0), (1, 1)), (0, True), 0), TypeError)
            and _rejects((Lazy(), (0,), 0), TypeError)
            and _rejects((((Lazy(), 0),), (0,), 0), TypeError)
            and _rejects((((0, 0),), (0,), Lazy()), TypeError)
        )
    finally:
        _queue = saved_queue
    checks['late_unreachable_invalid_before_queue_or_hooks'] = late_ok and queue_calls == [] and hooks == []

    fresh = menu_distinction_report(table, flags, 0)
    immutable = False
    try:
        fresh.classes[0][0] = 8
    except TypeError:
        immutable = True
    max_report = menu_distinction_report(ring, (0, 1, 0, 1, 0, 1), 0)
    ascii_report = json.dumps(max_report._asdict(), ensure_ascii=True)
    checks['maximum_domain_fresh_nested_immutable_ASCII_report'] = (
        len(max_report.reachable) == 6 and len(max_report.witnesses) == 15
        and max_report == word_table_reference(ring, (0, 1, 0, 1, 0, 1), 0)
        and fresh == manual and fresh is not manual and immutable
        and ascii_report.isascii() and table == ((1, 2), (3, 3), (4, 4), (3, 3), (4, 4), (5, 5))
    )
    assert len(checks) == 14 and all(type(value) is bool for value in checks.values())
    if not all(checks.values()):
        raise AssertionError([name for name, passed in checks.items() if not passed])
    return {
        'runtime': {'implementation': platform.python_implementation(), 'python': platform.python_version()},
        'contract': {'max_states': 6, 'alphabet': [0, 1], 'observation': 'supplied Boolean flag', 'word_units': 'abstract symbols', 'live_IVR_tested': False},
        'manual_report': manual._asdict(),
        'manual_tie_word': _word(tie, 0, 1),
        'equivalent_word': None,
        'different_now_word': (),
        'finite_family': {**counts, 'meaningful_groups': 1, 'scope': 'all three-state binary tables and flags, entry0 fixed; not all1..6 inputs'},
        'validation': {'type_shape_bound_profiles': len(invalids), 'late_or_lazy_profiles': 5, 'production_queue_calls_on_rejected_inputs': len(queue_calls), 'lazy_hook_calls': len(hooks)},
        'self_checks': checks,
        'self_checks_passed': len(checks),
        'limitations': ['Only the supplied total deterministic Boolean-observation table.', 'None proves model-language equivalence, not permission to merge real menus.', 'No actual DTMF, timeout, audio, device, library DFA or service execution.'],
    }


if __name__ == '__main__':
    if not AUTHOR_MAIN_ENABLED:
        raise SystemExit('author main disabled pending ROOT authorization')
    sys.stdout.reconfigure(encoding='utf-8', newline='\n')
    print(json.dumps(run_example(), ensure_ascii=True, indent=2))

مرجعِ آزمون، جست‌وجوی جفت‌ها را تکرار نمی‌کند. دسترسی را با بستارِ بولیِ جدول به دست می‌آورد و همهٔ واژه‌های دودویی تا طولِ تعدادِ حالت‌ها منهای یک را مستقیماً از هر حالت می‌خواند. چرا این کران کافی است؟ رابطهٔ برابری تا طولِ k، در مرحلهٔ بعد با دو جانشین پالایش می‌شود. اگر افراز تغییر نکند، ثابت شده است؛ هر تغییرِ واقعی تعدادِ کلاس‌ها را زیاد می‌کند و بیش از تعدادِ حالت‌ها کلاس نداریم. پس کران، نتیجهٔ استدلالِ افراز است، نه حدسِ آزمایش.

خانوادهٔ متناهیِ برنامه همهٔ جدول‌های سه‌حالتی با دو ورودی و همهٔ ردیف‌های پرچمِ دودویی را با شروعِ صفر مقایسه می‌کند: ۵۸۳۲ پروفایل، در یک گروهِ آزمون. این خانواده تمامِ دامنهٔ یک تا شش حالت را نمی‌پوشاند. شاهدهای دستی، تغییرِ نام، جابه‌جاییِ نمادها، چرخه، ورودیِ نامعتبرِ دیرهنگام و مرزِ شش حالت جدا بررسی می‌شوند. تعدادِ واقعیِ جفت‌ها و ارزیابیِ واژه‌ها از حلقهٔ اجرا در گزارش ثبت می‌شود؛ هر نمونه یک گروهِ مستقل نامیده نمی‌شود.

{
  "runtime": {
    "implementation": "CPython",
    "python": "3.14.5"
  },
  "contract": {
    "max_states": 6,
    "alphabet": [
      0,
      1
    ],
    "observation": "supplied Boolean flag",
    "word_units": "abstract symbols",
    "live_IVR_tested": false
  },
  "manual_report": {
    "reachable": [
      0,
      1,
      2,
      3,
      4
    ],
    "unreachable": [
      5
    ],
    "classes": [
      [
        0
      ],
      [
        1,
        3
      ],
      [
        2
      ],
      [
        4
      ]
    ],
    "witnesses": [
      [
        0,
        1,
        [
          1,
          0
        ]
      ],
      [
        0,
        2,
        [
          0
        ]
      ],
      [
        0,
        3,
        [
          1,
          0
        ]
      ],
      [
        0,
        4,
        []
      ],
      [
        1,
        2,
        [
          0
        ]
      ],
      [
        1,
        3,
        null
      ],
      [
        1,
        4,
        []
      ],
      [
        2,
        3,
        [
          0
        ]
      ],
      [
        2,
        4,
        []
      ],
      [
        3,
        4,
        []
      ]
    ]
  },
  "manual_tie_word": [
    0
  ],
  "equivalent_word": null,
  "different_now_word": [],
  "finite_family": {
    "profiles": 5832,
    "state_word_evaluations": 122472,
    "reachable_pair_queries": 12096,
    "meaningful_groups": 1,
    "scope": "all three-state binary tables and flags, entry0 fixed; not all1..6 inputs"
  },
  "validation": {
    "type_shape_bound_profiles": 26,
    "late_or_lazy_profiles": 5,
    "production_queue_calls_on_rejected_inputs": 0,
    "lazy_hook_calls": 0
  },
  "self_checks": {
    "manual_two_symbol_witness": true,
    "None_is_not_empty_word": true,
    "unequal_current_flags_empty_word": true,
    "shortest_then_lexicographic_zero_first": true,
    "unreachable_domain_excluded": true,
    "cycle_exhaustion_proves_equivalence": true,
    "uniform_observation_single_class": true,
    "observation_one_not_implicitly_absorbing": true,
    "independent_word_table_family_ONE_group": true,
    "renaming_covariance_canonical_classes": true,
    "symbol_swap_equivalence_not_lex_word_assumption": true,
    "strict_types_shapes_bounds_and_caps": true,
    "late_unreachable_invalid_before_queue_or_hooks": true,
    "maximum_domain_fresh_nested_immutable_ASCII_report": true
  },
  "self_checks_passed": 14,
  "limitations": [
    "Only the supplied total deterministic Boolean-observation table.",
    "None proves model-language equivalence, not permission to merge real menus.",
    "No actual DTMF, timeout, audio, device, library DFA or service execution."
  ]
}

۵. چهار پرسش دربارهٔ هم‌ارزی و مرزِ آزمون

مدلِ کوچکِ روی سینی، جدا از کارگاهِ بزرگ‌تر در پس‌زمینهٔ محو
تصویر مفهومی: مدلِ کوچکِ روی سینی، جدا از کارگاهِ بزرگ‌تر در پس‌زمینهٔ محو؛ بدون مقیاس عددی و مستقل از نتایج اجرای کد.

پرسشِ اول: چرا پرچمِ برابر و پاسخِ برابر به هر ورودیِ تک‌مرحله‌ای کافی نیست؟ در نمونهٔ صفر و یک، همهٔ این مشاهده‌ها برابرند، اما واژهٔ «یک، صفر» به چهار و سه می‌رسد. آزمونِ تک‌مرحله‌ای عمقِ لازم را ندیده است. روشِ گرافِ جفت‌ها این عمق را از خودِ جدول پیدا می‌کند؛ به جای افزایشِ حدِ دلخواه، تا تمام شدنِ فضایِ متناهی پیش می‌رود.

پرسشِ دوم: آیا None همان شاهدِ خالی است؟ خیر. برای سه و چهار، شاهدِ خالی یعنی اختلافِ فعلی و طولِ صفر. برای یک و سه، None یعنی هیچ واژهٔ متناهی اختلاف نمی‌سازد. اگر رابطِ آزمون این دو را یکسان نمایش دهد، نتیجهٔ هم‌ارزی را با ساده‌ترین اختلاف اشتباه گرفته است. خروجیِ JSON نیز null را از آرایهٔ خالی جدا نگه می‌دارد.

پرسشِ سوم: آیا کلاسِ مشترک یعنی دو منوی واقعی را می‌توان ادغام کرد؟ خیر. فقط یک پرچمِ دودویی و گذارهای همین مدل دیده شده‌اند. متن و صوتِ پیام، هزینه، اقدامِ جانبی، مجوز، زمان، ورودیِ نامعتبر و معنای کسب‌وکار می‌توانند متفاوت باشند. برای ادغام باید مدل و مشاهده‌های متناسب با آن تصمیم جدا طراحی و با پیاده‌سازی سنجیده شوند؛ این برنامه چنین کاری انجام نمی‌دهد.

پرسشِ چهارم: چرا دادهٔ بد در حالتِ دسترس‌ناپذیر هم رد می‌شود؟ قرارداد، جدولِ کامل و معتبر می‌خواهد. اگر فقط مسیرهای فعلی را اعتبارسنجی کنیم، تغییرِ شروع می‌تواند همان ورودی را ناگهان معتبر یا نامعتبر کند و خطای مدل پنهان بماند. ابتدا صحتِ کلِ داده، سپس محدود کردنِ دامنهٔ گزارش به دسترس‌پذیرها انجام می‌شود. این ترتیب، خاصیتِ همین API است و ادعای تحلیلِ تمامِ رفتارهای یک مرکزِ تماس نیست.

منابع و مطالعهٔ بیشتر

بررسی منابع: ۳۰ مهر ۱۴۰۵. تحلیل‌ها و پیشنهادهای اجرایی، جمع‌بندی نویسنده‌اند.