ステートマシン
ワイヤフォーマットだけではプロトコルの正しい実装には足りません。パケットを完璧にデコードできても、不正なシーケンスは防げない。クローズ済みコネクションへのデータ送信、未完了のハンドシェイク後の再送、非アクティブパスの放棄など。wirespec ではステートマシンを第一級の言語プリミティブとして扱います。ワイヤフォーマットと同じ .wspec ファイルで宣言し、検証可能な C ディスパッチコードにコンパイルされ、他の言語機能と同じ型チェック規則が適用されます。
基本構造
state machine Name { ... } で定義します。内部で状態・初期状態・遷移を宣言します。
state machine PathState {
state Init { path_id: VarInt }
state Validating { path_id: VarInt, challenge: bytes[8] }
state Active { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
state Standby { path_id: VarInt }
state Closing { path_id: VarInt, error_code: VarInt }
state Closed [terminal]
initial Init
...
}各状態は波括弧内に型付きの関連データを持てます。デフォルト値も指定可能（rtt: u64 = 0）。データのない状態は波括弧不要です（state Idle）。
[terminal] はその状態から出られないことを示します。ターミナル状態にイベントを送ると（吸収するワイルドカード遷移がなければ）WIRESPEC_ERR_INVALID_STATE が返ります。
initial Name で開始状態を指定します。
遷移
イベントに応じてマシンをある状態から別の状態へ移します。
transition Validating -> Active {
on recv_path_response(r: bytes[8])
guard r == src.challenge
action { dst.path_id = src.path_id; }
}遷移の 3 つの節:
| 節 | 役割 |
|---|---|
on event(params) | 遷移のトリガーとなるイベント（必須） |
guard expr | 条件式。偽なら遷移をスキップ（任意） |
action { ... } | 遷移先状態の初期化代入（任意） |
src と dst
src— 現在の状態データ（読み取り専用）dst— 遷移先の状態データ（書き込み専用）guardはsrcのみ参照可能actionはsrcを読みdstに書く
action 内の代入はセミコロン区切り:
action {
dst.path_id = src.path_id;
dst.error_code = code;
}末尾のセミコロンは省略可能です。
完全初期化
コンパイラはデフォルト値のない dst フィールドがすべて action 内で代入されていることを検証します。未代入はコンパイルエラー。ゼロ初期化も暗黙コピーもありません。
transition Active -> Closing {
on send_path_abandon(code: VarInt)
action {
dst.path_id = src.path_id; # required: Closing has path_id (no default)
dst.error_code = code; # required: Closing has error_code (no default)
}
}デフォルト値のあるフィールド（rtt: u64 = 0）は省略可能で、自動的にデフォルト値が使われます。
ワイルドカード遷移
transition * -> State は任意のソース状態にマッチします。「どの状態にいてもこのイベントでコネクションを終了する」といった表現に使います:
transition * -> Closed { on connection_closed }具体的な遷移は常にワイルドカードより優先されます。A -> B { on ev } と * -> Closed { on ev } が両方あり、状態 A にいる場合は具体的な方が適用されます。
状態コンストラクタ
配列要素の初期化など、状態値をリテラルとして作る場合に使います:
PathState::Active(path_id, 0, 0)引数はフィールドの宣言順（位置引数）。デフォルト値付きフィールドは末尾から省略可能:
# Active has: path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0
PathState::Active(pid) # equivalent to PathState::Active(pid, 0, 0)
PathState::Active(pid, 10) # equivalent to PathState::Active(pid, 10, 0)フィールドのないターミナル状態は括弧不要:
PathState::Closed # not PathState::Closed()配列のための fill()
状態フィールドに他のステートマシンの配列を持たせられます。全要素を同じ値で初期化するには fill() を使います:
dst.paths = fill(PathState::Closed, 4) # set all 4 slots to Closedfill(value, count) は組み込みの特殊形式で、関数呼び出しではありません。値として渡すことはできません。
配列サブスクリプトと +=
配列の個々の要素を読み書きできます:
action {
dst.paths = src.paths;
dst.paths[src.active_path_count] = PathState::Init(path_id);
dst.active_path_count = src.active_path_count + 1;
}カウンタのインクリメントは += で書けます:
action {
dst.paths = src.paths;
dst.paths[src.active_path_count] = PathState::Init(path_id);
dst.active_path_count += 1;
}まとめ: PathState
examples/mpquic/path.wspec の PathState マシン全体:
module mpquic.path
import quic.varint.VarInt
state machine PathState {
state Init { path_id: VarInt }
state Validating { path_id: VarInt, challenge: bytes[8] }
state Active { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
state Standby { path_id: VarInt }
state Closing { path_id: VarInt, error_code: VarInt }
state Closed [terminal]
initial Init
transition Init -> Validating {
on send_path_challenge(c: bytes[8])
action { dst.path_id = src.path_id; dst.challenge = c; }
}
transition Validating -> Active {
on recv_path_response(r: bytes[8])
guard r == src.challenge
action { dst.path_id = src.path_id; }
}
transition Validating -> Closed { on validation_timeout }
transition Active -> Standby {
on recv_path_standby
action { dst.path_id = src.path_id; }
}
transition Standby -> Active {
on recv_path_available
action { dst.path_id = src.path_id; }
}
transition Active -> Closing {
on send_path_abandon(code: VarInt)
action { dst.path_id = src.path_id; dst.error_code = code; }
}
transition Standby -> Closing {
on send_path_abandon(code: VarInt)
action { dst.path_id = src.path_id; dst.error_code = code; }
}
transition Closing -> Closed { on closing_complete }
transition * -> Closed { on connection_closed }
}Active <-> Standby の遷移で分かるように、同じイベント名を異なるソース状態の遷移で使えます。末尾の * -> Closed により、connection_closed はどの状態からでもパスを終了させます。
階層的ステートマシンのための delegate
ステートマシンは別のステートマシンをフィールドに持てます。delegate で親から子へイベントを転送します:
module mpquic.connection
state machine ChildProcess {
state Running { value: u8 }
state Stopped [terminal]
initial Running
transition Running -> Stopped { on halt }
transition * -> Stopped { on force_stop }
}
state machine SimpleDelegateExample {
state Active { child: ChildProcess, data: u64 }
state Closed [terminal]
initial Active
transition Active -> Active {
on child_event(ev: u8)
delegate src.child <- ev
}
transition Active -> Closed { on disconnect }
transition * -> Closed { on error }
}delegate src.child <- ev で ev を src.child（ChildProcess サブマシン）に転送しています。
delegate の規則:
- 自己遷移（
Active -> Activeのようにソースと遷移先が同じ状態）でのみ有効 delegateのある遷移に明示的なactionは書けない- 対象フィールドの型は別の
state machineでなければならない
dst の自動初期化
delegate 遷移では、コンパイラがイベント転送前に src を dst へ自動コピーします。dst.data = src.data を手書きする必要はありません。子の更新はコピー済みの dst に対してインプレースで適用されます。
child_state_changed
delegate でイベントを転送した結果、子の状態が実際に変わった場合、ランタイムは child_state_changed 内部イベントを親に発行します。親側でこれに反応する遷移を定義できます:
transition Connected -> Draining {
on child_state_changed
guard all(src.paths[0..src.active_path_count], in_state(Closed))
}child_state_changed は、一致する遷移がない場合に無音で破棄される唯一のイベントです。他の未処理イベントはすべて WIRESPEC_ERR_INVALID_STATE になります。これにより頻繁に発行されても安全で、親は必要な場合にだけ反応します。
child_state_changed は予約識別子です。ユーザーイベント名には使えません。
all() 量化子と in_state()
all(collection, predicate) はコレクションの全要素が述語を満たすか検査します:
guard all(src.paths[0..src.active_path_count], in_state(Closed))- コレクションはスライス式（後述）
- 述語は
in_state(StateName)のみ（v1.0 で唯一サポートされる形式） all()は組み込みの特殊形式で、汎用の高階関数ではない
in_state(S) は要素が状態 S にあるかをチェックします。state machine 型のフィールドまたは配列要素にのみ使えます。
スライス式
collection[start..end] で start から end の直前まで（半開区間）を選択します。Rust の .. と同じ規約です:
src.paths[0..src.active_path_count] # first active_path_count elements
src.paths[1..4] # elements at indices 1, 2, 3主な用途:
all(slice, predicate)— 配列のサブセットを検査exists i in 0..N: ...— インデックス範囲を走査（verifyプロパティ内）
verify 宣言
ステートマシンに verify 宣言を含められます:
verify NoDeadlock
verify AllReachClosed
verify property AbandonIsFinal:
in_state(Closing) -> [] not in_state(Active)verify NoDeadlock と verify AllReachClosed はコンパイラ組み込みの名前付きプロパティです。verify property Name: formula は guard と同じ式言語に時相演算子（[] 常に、<> いつか、~> leads-to）を加えた時相論理プロパティを定義します。
TLA+ 生成は未実装
verify 宣言は現在パースと型チェックのみ行われます。TLA+ モデル生成は Phase 3 で予定。今書いておいても実行時の効果はありませんが、設計意図を明示でき、TLA+ バックエンド実装時に自動的に有効になります。
生成される C コード
各ステートマシンに対してダブルスイッチのディスパッチ関数が生成されます。FooState マシンの場合:
wirespec_result_t foo_state_dispatch(
foo_state_t *sm,
foo_state_event_t event,
const void *event_data);生成されるコードのイメージ:
switch (sm->tag) {
case FOO_STATE_ACTIVE:
switch (event) {
case FOO_STATE_EVENT_TIMEOUT:
/* evaluate guard, then action */
...
return WIRESPEC_OK;
default:
return WIRESPEC_ERR_INVALID_STATE;
}
case FOO_STATE_CLOSED:
return WIRESPEC_ERR_INVALID_STATE; /* terminal */
...
}外側のスイッチで現在の状態を選択し、内側のスイッチでイベントをディスパッチします。コンパイラは全ての非ワイルドカード遷移がカバーされていること、同一 (状態, イベント) ペアに競合する遷移がないことを静的に検証します。
状態データはタグ付きユニオンで表現されます:
typedef struct {
foo_state_tag_t tag;
union {
foo_state_active_t active;
foo_state_validating_t validating;
/* ... */
} data;
} foo_state_t;次のステップ
- モジュール・インポート — 定義を複数の
.wspecファイルに分割 - 言語ツアー — プリミティブ、フレーム、カプセル、式
- C API リファレンス — parse / serialize / dispatch 関数の完全リファレンス