フォーマル検証

wirespec はステートマシンを 2 つのレベルで検証します: コンパイル時の静的解析と、より深いプロパティのための TLA+ モデル検査です。

wirespec verify はデフォルトで組み込みの Rust モデルチェッカー（tla-checker）を自動実行します（Java のインストール不要）。より大きな状態空間には --run-tlc で外部の Java ベース TLC を使うこともできます。

静的解析

コンパイラはすべてのステートマシンに対して以下のプロパティを自動チェックします:

チェック	検出内容
ターミナル不可逆性	[terminal] 状態からの遷移
デリゲート非循環性	ステートマシン間の循環デリゲーションチェーン
構造的到達可能性	ターミナル状態に到達できない状態
網羅的遷移	出力遷移のない非ターミナル状態
ワイルドカード優先度	具体的遷移によるワイルドカードの正しいオーバーライド

これらはコンパイル時に設定不要で実行されます。

TLA+ モデル検査

より深い検証のために、wirespec は TLA+ 仕様を生成し組み込みモデルチェッカーを実行します。

プロパティの宣言

ステートマシン内に verify 宣言を追加します:

@verify(bound = 3)
state machine PathState {
    state Init { path_id: u8 }
    state Active { path_id: u8, rtt: u8 = 0 }
    state Closed [terminal]
    initial Init

    transition Init -> Active {
        on activate(id: u8)
        action { dst.path_id = src.path_id; }
    }
    transition Active -> Closed { on close }
    transition * -> Closed { on abort }

    verify NoDeadlock
    verify AllReachClosed
    verify property AbandonIsFinal:
        in_state(Closing) -> [] not in_state(Active)
}

組み込みプロパティ

プロパティ	種類	チェック内容
NoDeadlock	安全性（不変条件）	すべての非ターミナル状態に有効な遷移が 1 つ以上ある
AllReachClosed	活性	公平スケジューリングの下で、すべてのパスが最終的にターミナル状態に到達する

ユーザー定義プロパティ

verify property で時相論理演算子を使用します:

演算子	意味	例
[]	常に（グローバルに）	[] not in_state(Error)
<>	いつか（最終的に）	<> in_state(Closed)
~>	leads-to	in_state(Active) ~> in_state(Closed)
->	ならば（含意）	in_state(B) -> not in_state(A)
and / or / not	論理演算	in_state(A) and not in_state(B)
in_state(S)	状態述語	in_state(Active)

検証の実行

# デフォルト: TLA+ 仕様を生成して組み込み Rust モデルチェッカーを実行（Java 不要）
wirespec verify path.wspec -o build/tla/

# 外部 Java TLC を使用（大きな状態空間向け）
wirespec verify path.wspec --run-tlc --bound 3

バウンドパラメータ

@verify(bound = N) はモデル検査の値ドメインのサイズを制御します。各整数フィールドは 0..N-1 の範囲を取ります。バウンドが大きいほど多くの状態を探索しますが、時間がかかります。

バウンド	探索状態数	時間
2	約 100	1 秒未満
3	約 1,000	約 1 秒
5	約 10,000	約 5 秒

CLI の --bound N はアノテーションをオーバーライドします。

ガードの排他性

同一の（状態、イベント）ペアに異なるガードを持つ遷移が複数ある場合、wirespec はガードが相互排他的であることを検証する TLA+ 不変条件を自動生成します:

transition Trying -> Trying {
    on retry
    guard src.count < 3
    action { dst.count = src.count + 1; }
}
transition Trying -> Done {
    on retry
    guard src.count >= 3
}

モデルチェッカーは count < 3 と count >= 3 が同時に成立しないことを検証します。

階層ステートマシンの検証

delegate を使うステートマシンも検証できます。wirespec は子ステートマシンの状態と遷移を親の TLA+ 仕様にインライン展開するため、モデルチェッカーは親と子の結合状態空間を一度に探索します。

state machine Child {
    state Idle {}
    state Done [terminal]
    initial Idle
    transition Idle -> Done { on finish }
}

state machine Parent {
    state Running { child: Child }
    state Closed [terminal]
    initial Running

    transition Running -> Running {
        on forward(ev: u8)
        delegate src.child <- ev
    }
    transition Running -> Closed {
        on child_state_changed
        guard src.child in_state(Done)
    }

    verify NoDeadlock
    verify AllReachClosed
}

wirespec verify parent.wspec

生成される TLA+ 仕様では、子の状態が親の状態レコードのフィールドとして追跡されます。ChildDispatch オペレータがイベント番号を子の遷移にマッピングし、child_state_changed 遷移は子の状態が変わったときに発火します。

子ステートマシンの配列にも対応しています:

state machine Connection {
    state Open { paths: [PathState; 4] }
    state Done [terminal]
    initial Open

    transition Open -> Open {
        on close_path(idx: u8, ev: u8)
        delegate src.paths[idx] <- ev
    }
    transition Open -> Done { on shutdown }
    verify NoDeadlock
}

バウンドパラメータは親と子の両方の値ドメインに適用されます。子ステートマシンの配列は状態空間を乗算するため、検証を実用的に保つには小さなバウンド（2 や 3）を使ってください。

現在、検証がサポートされるのは 1 段のデリゲーションのみです。子ステートマシン自身が delegate を使っている場合、wirespec verify はエラーを報告します。