第3回：性質を書く――安全性・活性・反例による修正¶

第2回では，初期状態と遷移を記述しました．今回は，モデルが満たすべき要求を検証する性質として記述します．「異常状態に入らない」「処理を開始したらいつか応答する」を別々に調べ，反例を使ってモデルを修正します．

演習は，予想 → 実行 → 解答・解説との比較 → 理由の説明，の順で進めます．成果物の提出は求めません．性質が真になった場合も，何を確認できたのか，要求の前提となる状況が起こり得るかを自分で確かめます．

3.1 到達目標と準備¶

モデルの振る舞いと，検証したい要求を区別できる．
不変条件と安全性，活性の違いを例で説明できる．
LTLのG・F・Xを使って基本的な性質を書ける．
活性の反例にあるループを読み，応答しない経路を説明できる．
空虚な成立を見つけ，要求の前提が到達可能か確認できる．
CTLのEFによる到達可能性と，LTLの全経路についての検証を区別できる．

内容	目安
準備と要求の整理	15分
不変条件とLTLの基本	25分
実行結果と反例による修正	20分
空虚な成立と到達可能性	15分
演習と振り返り	25〜40分

第1・2回を終え，nuXmv 2.1.0を実行できることを前提とします．作業フォルダーと実行ファイルの場所を設定します．実行ファイルのパスは，自分の展開先に合わせてください．

Windows（PowerShell）macOS（Terminal）

New-Item -ItemType Directory -Force -Path "$HOME\nuxmv-tutorial\lesson03"
Set-Location "$HOME\nuxmv-tutorial\lesson03"
$nuxmvExe = "$HOME\Downloads\nuXmv-2.1.0-win64\bin\nuXmv.exe"
Test-Path $nuxmvExe

最後の結果がTrueであることを確認します．

mkdir -p "$HOME/nuxmv-tutorial/lesson03"
cd "$HOME/nuxmv-tutorial/lesson03"
nuxmvExe="$HOME/Downloads/nuXmv-2.1.0-macos-universal/bin/nuXmv"
ls -l "$nuxmvExe"

実行ファイルの情報が表示されることを確認します．

.smvファイルはプレーンテキスト，UTF-8（BOMなし）で保存します．拡張子とスマートダッシュなどの設定は第1回と同じです．

3.2 モデルと要求を分ける¶

今回の制御器には，待機中idle，処理中busy，応答段階done，異常状態errorがあります．待機から処理に進むかどうかを非決定的に選び，正常なら処理の次に応答します．

stateDiagram-v2
    [*] --> idle
    idle --> idle
    idle --> busy
    busy --> done
    done --> idle
    error --> error

要求をまず自然言語で整理します．

要求	調べる内容	違反する振る舞いの例
異常状態に入らない	到達するどの状態も`error`ではない	`idle → busy → error`
処理を開始したら，いつか応答する	`busy`になった後，いずれ`done`になる	`idle → busy → busy → …`
処理中なら，次の状態で応答する	`busy`の直後が`done`である	`idle → busy → finish → done → …`

最後の例は，応答が1段階遅れる例です．「いつか」と「次の状態」は同じ要求ではありません．性質を書く前に，成立する経路と違反する経路を考えると，要求の強さを確認できます．

今回の要求の範囲

外部の要求信号はまだ導入しません．今回はbusyを処理開始・処理中の状態として使い，その状態からの応答を調べます．「外部から来た要求を必ず受理する」ことまでは確認していません．環境入力は第4回で扱います．

3.3 不変条件と安全性¶

状態についての不変条件¶

INVARSPEC phase != error;

不変条件は，初期状態を含むすべての到達可能な状態で成立する条件です．INVARSPECの後には，今回のような現在状態についての条件式を書きます．

安全性は「悪いことが起きない」という性質です．異常状態に入った場合，そこまでの有限の経路を示せば違反を説明できます．今回の不変条件は安全性の例です．安全性には状態間の順序に関するものもあるため，すべての安全性が単純な不変条件として書けるわけではありません．

性質は遷移を制限しない¶

INVARSPEC phase != error;を追加しても，errorへ進む遷移は消えません．性質は「このモデルで成立するか」を調べる対象です．状態を制限するINVARとは役割が違います．制約によって違反する振る舞いを除外することと，元のモデルを検証することを混同しないでください．

3.4 実行経路について書くLTL¶

G・F・Xの読み方¶

LTL（Linear Temporal Logic，線形時相論理）は，実行経路に沿った性質を表します．まず1つの経路の，ある位置から先を考えます．

式	意味	注意点
`G p`	現在以降，常に`p`	現在の位置も含む
`F p`	現在以降のどこかで`p`	現在すでに`p`でも成立する
`X p`	次の状態で`p`	現在の状態ではなく，1回遷移した後

nuXmvのLTLSPECでは，式がモデルのすべての実行経路で成立するかを検証します．今回は公平性の制約を使わず，各状態から次状態があるモデルを扱います．

「処理したらいつか応答する」¶

LTLSPEC G ((phase = busy) -> F (phase = done));

外側のGによって，経路のどの位置でも条件を確認します．その位置でbusyなら，その位置以降のどこかにdoneが必要です．含意p -> qは，pが偽なら成立し，pが真ならqの成立を要求します．

これは活性の例です．「いつか応答する」の違反を説明するには，応答しないまま続く振る舞いを示します．有限の途中経過で応答していなくても，その後で応答する可能性があるため，それだけで違反とは言えません．

今回の応答の対応付け

この式は，各busyの位置から先にdoneがあることを要求します．複数の要求が同時に存在する場合の個別の対応付けや，要求番号までは表しません．今回の簡単な制御器についての式です．

「次の状態で応答する」¶

LTLSPEC G ((phase = busy) -> X (phase = done));

FをXに変えると，応答までの遷移を1回に限定します．busy → finish → doneという経路なら，「いつか」は成立しますが，「次の状態」は成立しません．今回の図のようにbusyとdoneが異なる状態なら，次で応答する性質の方が強い要求です．

外側のGが必要な理由¶

LTLSPEC (phase = busy) -> F (phase = done);

この式を初期状態idleで評価すると，前提phase = busyが偽なので成立します．後からbusyになっても，その位置についての要求は書かれていません．「いつ処理を始めても」という要求には，外側のGを付けます．

3.5 正常なモデルを検証する¶

controller_response.smvを作業フォルダーに保存します．リンク先を保存するか，次の内容をコピーして作成してください．

controller_response.smv

MODULE main
VAR
  phase : {idle, busy, done, error};
ASSIGN
  init(phase) := idle;
  next(phase) := case
    phase = idle : {idle, busy};
    phase = busy : done;
    phase = done : idle;
    TRUE : phase;
  esac;
INVARSPEC phase != error;
LTLSPEC G ((phase = busy) -> F (phase = done));
LTLSPEC G ((phase = busy) -> X (phase = done));
CTLSPEC EF (phase = busy);
CTLSPEC EF (phase = done);

最後の2行は到達可能性の確認で，3.7節で説明します．まずは先の3つの性質に注目します．

Windows（PowerShell）macOS（Terminal）

& $nuxmvExe .\controller_response.smv

"$nuxmvExe" controller_response.smv

表示順序がファイルの記述順と異なることがあるため，出力に表示された式と真偽を対応させて読みます．空白や括弧の整形も変わる場合があります．

検証した式	期待結果	理由
`phase != error`	`true`	初期状態から異常に進まない
`G ((phase = busy) -> F (phase = done))`	`true`	処理中になれば次に応答する
`G ((phase = busy) -> X (phase = done))`	`true`	処理中の次は必ず応答段階
`EF (phase = busy)`	`true`	処理中に至る経路がある
`EF (phase = done)`	`true`	応答段階に至る経路がある

待機し続ける経路もありますが，その経路では処理を開始しないため，処理開始後の応答要求には違反しません．「必ず処理を開始する」を確認した結果ではありません．

ほかのファイルも，同じコマンドのファイル名を置き換えて実行します．編集後は必ず保存してから再実行してください．

3.6 安全性と活性の反例を読む¶

異常状態に入るモデル¶

controller_error.smvでは，phase = busy : error;に変えてあります．安全性と2つの応答要求が偽になります．安全性の反例はidle → busy → errorで，異常に到達した時点で違反です．

修正する場合は，要求と動作の説明に立ち戻ります．今回の意図は「処理の次に応答」なので，phase = busy : done;へ戻します．性質を削除したり，異常への遷移を除外する制約を追加したりして真にすることは，このバグを修正したことにはなりません．

処理を続けられるモデル¶

controller_stuck.smvでは，処理中の分岐を次のようにします．

phase = busy : {busy, done};

安全性は真ですが，応答の活性は偽です．doneへ進めることに加えて，busyを選び続ける経路があるからです．活性の反例の主要部分は，次のようなループで表されます．

idle → [busy → busy → …]

nuXmvの出力の-- Loop starts hereは，繰り返し部分の開始位置を示します．最後に表示された状態からループの開始状態へ戻り，その部分が無限に繰り返されると読みます．表示されない変数は直前の値を引き継ぎます．状態数やループの位置がこの説明と違っても，遷移が合法で，busyになった後にdoneが現れないことを確認してください．

nuXmv 2.1.0で得られた出力の例です．

-- specification  G (phase = busy ->  F phase = done)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    phase = idle
  -- Loop starts here
  -> State: 1.2 <-
    phase = busy
  -- Loop starts here
  -> State: 1.3 <-
  -> State: 1.4 <-

状態1.3と1.4にもphase = busyが引き継がれます．この例では同じ状態を表す位置が複数あり，ループ開始の印も複数表示されています．どちらの印の位置から繰り返してもbusyに留まり，doneは現れません．各状態の値を復元することが，活性の違反を読むポイントです．

flowchart LR
    A[idle] --> B[busy]
    B --> B

反例の末尾は実行の終了ではありません

活性の反例は，有限の前半と無限に繰り返す部分によって，無限の実行を表します．最後の状態まで応答がないというだけでなく，ループを繰り返しても応答がないことが違反の根拠です．

今回のモデルで応答を保証するには，処理を続ける選択肢をなくして必ずdoneへ進めます．現実に処理時間が可変なら，上限付きの処理段階などをモデル化する方法も考えられます．公平性の仮定を加える方法は第4回の発展内容です．仮定が現実に妥当かを確認する必要があります．

3.7 真という結果を吟味する¶

要求の前提が起こらない：空虚な成立¶

controller_vacuous.smvでは，待機の分岐をphase = idle : idle;にします．初期状態からずっと待機するため，安全性も2つの応答要求も真です．

応答要求が真なのは，処理が正常に完了することを観察できたからではありません．busyが一度も起こらず，含意の前提が常に偽だからです．このような成立を空虚な成立と呼びます．

CTLのEFで到達可能性を確認する¶

CTLSPEC EF (phase = busy);

CTL（Computation Tree Logic，計算木論理）では経路の選び方も式で表します．Eは「ある経路」，Fは「いつか」を表し，EF pは「pになる状態に至る経路がある」という意味です．現在の状態ですでにpなら，その状態も含みます．

正常モデルではEF (phase = busy)は真，待機し続けるモデルでは偽です．性質の前提が実際に起こり得るかを別の式で調べることで，この例の空虚な成立に気付けます．ただし，前提が到達可能であることだけで，モデルや要求の妥当性のすべてが保証されるわけではありません．

EFが偽の場合

今回の結果は，到達する経路が存在しないことを表します．単独の実行経路だけで「どの経路でも到達しない」を証明することはできないため，偽の結果すべてに通常の1本の反例が表示されるわけではありません．

「ある経路」と「すべての経路」を区別する¶

branching.smvは，初期状態startからdoneまたはwaitへ進み，その後は選んだ状態に留まります．

stateDiagram-v2
    [*] --> start
    start --> done
    start --> wait
    done --> done
    wait --> wait

記述	意味	結果
`CTLSPEC EF (phase = done);`	応答段階に至る経路がある	真
`LTLSPEC F (phase = done);`	すべての実行経路で，いつか応答段階になる	偽

start → wait → wait → …がLTLの反例です．「応答できる場合がある」だけでは，全経路での応答を保証しません．

発展として，CTLSPEC AG (phase != error);は，全経路で常に異常ではないことを表します．今回の公平性を使わないモデルでは，同じ条件のINVARSPECと対応します．CTLとLTLの一般的な表現力の比較は，この回では扱いません．

3.8 演習¶

演習1：要求を性質にする【基本】¶

controller_response.smvから性質の行を外したモデルを作り，次の要求を自分で追加してください．実行前に真偽を予想し，3.5節の結果と比較します．

異常状態には入らない．
処理中になったら，いつか応答段階に進む．
処理中なら，次の状態で応答段階に進む．

ヒント

1は状態の条件，2と3は経路上の順序の条件です．2と3では，「いつ処理を始めても」を外側のGで表します．

解答例と解説

INVARSPEC phase != error;
LTLSPEC G ((phase = busy) -> F (phase = done));
LTLSPEC G ((phase = busy) -> X (phase = done));

すべて真です．1では到達可能な状態を調べ，2と3では各経路の各位置を調べます．外側のGを省くと，初期状態がidleなので前提が偽となり，後の処理について調べる要求になりません．

自己確認： 式を読むとき，外側のG，含意の前提，FまたはXの順に意味を説明します．単に「応答する式」とだけ答えず，いつ・どの経路に要求するかを確認してください．

演習2：バグを修正してすべて再検証する【基本】¶

controller_error.smvを実行し，偽になった式とその理由を記録します．反例から原因の行を特定し，controller_fixed.smvとして修正します．修正後は性質を変えずにすべて再検証します．

解答例と解説

安全性と2つの応答要求は偽，処理中への到達可能性は真，応答段階への到達可能性は偽です．初期状態からidle → busy → errorと進み，errorでは留まります．

phase = busy : error;をphase = busy : done;へ変えると正常モデルに戻り，5つの性質がすべて真になります．

自己確認： 変更した行，修正後の経路，元の要求に合う理由を説明します．応答要求だけを削除する修正や，busy → busyにして異常を避ける修正では要求を満たせません．安全性だけ真になっても，応答の活性は別に確認します．

演習3：活性の反例のループを読む【基本】¶

controller_stuck.smvを実行します．応答の活性の反例を選び，次を説明してください．

処理を開始するまでの部分．
ループの開始位置と，繰り返す状態．
なぜループを繰り返しても応答しないか．
doneへ進む経路があっても，結果が偽になる理由．

解答例と解説

前半でidleからbusyに進み，ループではbusyに留まり続けます．自己ループはモデルの集合{busy, done}が許す選択です．ループ内にはdoneがないため，処理を開始した位置から先で応答しません．

ほかの選択で完了できても，全経路で成立するという要求に対しては，違反経路が1本あれば偽です．反例の具体的な前半や状態数は変わり得ます．

自己確認： 「表示された最後まで応答がない」ではなく，「無限に繰り返す部分にも応答がない」と説明します．Xの性質が偽になる理由も考えてください．1回でもbusy → busyを選べば，次の状態での応答には違反します．

演習4：空虚な成立に気付く【基本】¶

controller_vacuous.smvを実行し，応答要求が真になる理由を考えます．busyとdoneの到達可能性の結果を確認し，正常モデルとの違いを説明してください．

解答例と解説

応答要求は真ですが，到達可能性の2式は偽です．経路はidle → idle → …だけなので，処理開始後の応答要求は一度も前提が真になりません．

本来，処理を開始できるモデルを意図しているなら，待機からの分岐を{idle, busy}に戻します．すると前提が到達可能になり，応答要求も正常モデルでは成立します．

自己確認： 「応答を確認できた」と「処理が起きないので違反しなかった」を区別します．前提の到達可能性を確認しても，すべての要求を受理することまでは確認していない点も説明してください．

演習5：「いつか」と「次」を比較する【確認】¶

controller_delay.smvでは，busy → finish → doneと進みます．安全性と2つの応答要求の真偽を予想して実行し，偽の性質を真にするためにモデルと要求のどちらを変更するべきか考えます．

解答例と解説

安全性とFを使う応答要求は真，Xを使う応答要求は偽です．処理開始から2回の遷移後には応答しますが，直後はfinishなので，1回後の応答には違反します．

本来の要求が「次の状態で応答」なら，処理の遷移をdoneへ変更します．要求が単に「いつか応答」なら，その要求に対しては遅れるモデルでも成立しています．出力を真にする目的だけでXをFに変えてはいけません．自然言語の要求を先に確認します．

自己確認： 反例を「モデルが悪い」と決め付けず，モデルと性質のどちらが意図からずれているかを説明します．

演習6：到達可能性と全経路の応答【発展・任意】¶

branching.smvを実行し，EFが真でFのLTL検証が偽になる理由を図から説明します．さらに，once.smvのF (phase = done)とG F (phase = done)の結果を予想してください．このモデルはstart → busy → done → idle → idle → …と進みます．

解答例と解説

分岐モデルではstart → doneがあるのでEFは真ですが，start → wait → wait → …があるので，全経路についてのFは偽です．

1回だけ応答するモデルではF (phase = done)は真，G F (phase = done)は偽です．G F pは，どの位置から先にもpが現れることを要求します．無限の経路上では，pが無限に何度も現れることに対応します．idleになった後は再びdoneが現れないので違反します．

自己確認： 「1回以上応答する」と「繰り返し応答する」，「ある経路」と「すべての経路」の違いを，それぞれ別の観点として説明してください．

3.9 よくある誤りと見直し方¶

状況	確認すること
応答しないのに真になる	含意の前提が到達可能か，外側の`G`を省いていないか
応答できるのに偽になる	応答しない選択肢が残るか，全経路の要求になっているか
応答が少し遅れるだけで偽になる	`F`と`X`のどちらが自然言語の要求に合うか
反例の末尾で理由が分からない	ループの開始位置と，繰り返し部分の状態を復元する
結果の式を取り違える	記述順ではなく，出力された式と真偽を対応させる
構文エラーになる	`LTLSPEC`・`CTLSPEC`，括弧，セミコロン，式を置く場所を確認する

G・F・Xを使う式はLTLSPECに書きます．今回のINVARSPECには現在状態の条件を，CTLSPECにはEFなどのCTL式を書きます．LTLのXとモデルのnext(...)は記述する場所と役割が違うので，機械的に置き換えないでください．

3.10 振り返り¶

安全性と活性の違反を，それぞれ有限の違反経路と無限の繰り返しから説明できる（3.3節・3.6節）．
「処理中ならいつか応答」を，外側のGを含めて説明できる（3.4節・演習1）．
バグを直した後，安全性と応答の要求を再検証できる（演習2）．
活性の反例のループが表す無限の経路を説明できる（演習3）．
前提が起きないために真になる例を説明できる（3.7節・演習4）．
到達可能な応答と，全経路で保証される応答を区別できる（3.7節・演習6）．

最後に1つのモデルを選び，「自然言語の要求」「書いた式」「真偽」「反例または成立理由」「モデルの前提と確認できた範囲」を，解説を閉じて説明します．説明が曖昧な箇所を復習してください．

第4回では，インタラクティブ実行でモデルを調べ，環境入力とモジュールを使って構成要素を組み合わせます．

参考資料¶

nuXmv公式ドキュメント：使用バージョンの配布物内マニュアルのSpecificationsとトレース表示の説明を参照します．
NuSMV公式チュートリアル：CTL・LTL検証と反例の基礎例．古い資料のコマンドや文法の細部は，nuXmvの使用バージョンで確認してください．