第4回：対話的に調べる――環境入力と複数の構成要素¶

第3回までは，モデルをバッチ実行して性質を検証しました．今回は，nuXmvを起動したままコマンドを入力するインタラクティブ実行を使います．モデルの読み込み，個別の性質の検証，シミュレーションを順に体験します．

その後，外部からの要求を入力として記述し，制御器をモジュールに分け，環境モデルと接続します．操作した結果とその理由を解答・解説で確かめます．成果物の提出は求めません．

4.1 到達目標と準備¶

OSのシェルとnuXmvのプロンプトを区別して操作できる．
モデルを読み込み，性質の一覧，個別検証，トレースを確認できる．
シミュレーションで入力を選び，状態遷移との関係を説明できる．
IVAR，DEFINE，MODULEと引数を使ってモデルを構成できる．
同期的に接続した環境と制御器の更新を説明できる．
制約や公平性の仮定が，検証する振る舞いに及ぼす影響を説明できる．

内容	目安
準備と入力モデル	15分
対話的な検証とシミュレーション	25分
モジュールと環境の接続	25分
制約とデッドロック	10分
演習と振り返り	25〜40分

公平性は発展内容です．時間に応じて後から取り組んでください．nuXmv 2.1.0を使用し，作業フォルダーと実行ファイルの場所を設定します．パスは自分の展開先に合わせます．

Windows（PowerShell）macOS（Terminal）

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

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

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

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

ファイルはプレーンテキスト，UTF-8（BOMなし）で保存します．保存や起動に困ったら第1回を参照してください．

4.2 環境からの入力を加える¶

入力と内部状態¶

これまでは，待機から処理へ進むかを遷移の集合で表しました．今回は，外部入力requestが真なら待機から処理へ進みます．要求は待機中だけ受理し，処理中や応答段階で来た要求は記憶しない簡単な制御器とします．

種類	宣言	役割
状態変数	`VAR phase : ...;`	制御器が現在の段階を保持する
入力変数	`IVAR request : boolean;`	遷移時に環境から与えられる値

IVARには今回は制約を加えません．各遷移で真・偽のどちらの入力も許します．init(request)やnext(request)への代入は書きません．入力を一定の手順で生成したい場合は，後の4.6節のように環境の状態変数として表す方法があります．

入力を持つモデル¶

controller_input.smvを作業フォルダーに保存してください．

controller_input.smv

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

待機中に要求がなければ最後の分岐でidleに留まります．処理中の次は，要求の値にかかわらずdoneです．初期状態から要求を1回受け付けた後は，次のように進みます．

flowchart LR
    A[idle] -->|request = FALSE| A
    A -->|request = TRUE| B[busy]
    B --> C[done]
    C --> A

予想： 今回の3つの性質はすべて真です．ただし，任意の時点の要求をすべて受理するという性質ではありません．処理開始後の応答と，処理を開始できることを確認します．

4.3 対話的にモデルを検証する¶

起動とプロンプト¶

次はOSのシェルで実行します．

Windows（PowerShell）macOS（Terminal）

& $nuxmvExe -int

"$nuxmvExe" -int

起動するとnuXmv >が表示されます．以下のコマンドはこのプロンプトに入力します．プロンプト自体は入力しません．

入力する場所	使うコマンドの例
PowerShell／Terminal	nuXmvの起動，フォルダーの移動
`nuXmv >`	`read_model`，`go`，検証，シミュレーション，`quit`

読み込みとモデルの構築¶

read_model -i controller_input.smv
go
show_property

read_modelはファイルを読み込み，goは今回使うBDDによる検証に必要なモデル構築を行います．show_propertyは性質の一覧と検証状態を表示します．この段階ではUncheckedと表示されます．

nuXmv 2.1.0での一覧の例は次です．説明のため一部を省略しています．

000 :EF phase = busy
  [CTL            Unchecked      N/A    N/A]
001 : G (phase = busy -> F phase = done)
  [LTL            Unchecked      N/A    N/A]
002 :phase != error
  [Invar          Unchecked      N/A    N/A]

性質の番号は，ファイルに記述した順とは限りません．モデルを変更したら一覧を見直します．

性質を種類ごとに検証する¶

check_invar
check_ltlspec
check_ctlspec
show_property

それぞれ，不変条件，LTL，CTLの性質を検証します．このモデルではすべて真となり，一覧の状態も更新されます．ある性質だけを番号で指定することもできます．上の一覧で番号001が応答のLTL式であることを確認した場合は，次でその式だけを検証します．

check_ltlspec -n 1

番号が違う場合は，一覧に表示されたLTL式の番号を指定してください．

ヘルプとモデルの再読み込み¶

help -p simulate

help -pは，外部のページャーを使わずヘルプを表示します．macOS版などで通常のhelpがページャーのエラーになる場合にも使えます．

ファイルを編集したら，保存した後に次を実行します．

reset
read_model -i controller_input.smv
go
show_property

resetは読み込んだモデルや検証・トレースの情報を初期化します．ディスク上のファイルは削除しません．保存しただけでは，すでに構築したモデルは更新されません．

終了するときは次を入力し，OSのシェルへ戻ります．

quit

4.4 シミュレーションとトレース¶

初期状態を選ぶ¶

4.3節のモデルを読み込んでgoを実行した状態で，次を入力します．

pick_state -v

今回は初期状態がphase = idleの1つなので，その状態が選ばれます．pick_state -iなら，複数の初期状態から対話的に選ぶこともできます．

遷移と入力を選ぶ¶

simulate -i -k 1

1回の遷移について候補が表示されます．候補には，到達する状態と，その遷移で使う入力が表示されます．

phase = busyへ進む候補には，request = TRUEが対応する．
phase = idleへ留まる候補には，request = FALSEが対応する．

Choose a state ...という選択待ちになったら，画面の候補の番号を入力し，Enterを押します．候補番号は固定だと考えず，表示された状態と入力を見て選んでください．まずbusyへ進む候補を選びます．

選択待ちではnuXmvコマンドを入力しません

simulateの候補を選んでいる間は，選択番号を入力します．show_tracesなどのコマンドは，nuXmv >に戻ってから入力してください．

トレースを表示する¶

show_traces -v

初期状態と1回の遷移後の例は次です．

Trace Description: Simulation Trace
Trace Type: Simulation
  -> State: 1.1 <-
    phase = idle
  -> Input: 1.2 <-
    request = TRUE
  -> State: 1.2 <-
    phase = busy

Input: 1.2は，状態1.1から1.2への遷移に使った入力です．初期状態の変数の値と，遷移時の入力を区別します．

続けてsimulate -i -k 1を実行し，done，idleまで進みます．処理中ではどちらの入力でも次状態はdoneです．同じ次状態に到達する入力が複数候補になることがあります．

決定的・ランダムな実行¶

新しく初期状態から始め直すにはpick_state -vを再実行します．次は決定的な選び方で4回の遷移を進めます．

pick_state -v
simulate -v -k 4

ランダムに選ぶ場合はsimulate -r -v -k 4を使います．どちらも，観察するのはモデルの実行の一例です．観察した経路が安全でも，全経路の性質を確認したことにはなりません．また，シミュレーションで要求を出す候補だけを選んでも，検証用モデルが「必ず要求が来る」モデルに変わるわけではありません．

4.5 制御器をモジュールに分ける¶

MODULEと引数¶

controller_modules.smvは，制御器をcontrollerというモジュールに分けたものです．

controller_modules.smv

MODULE main
IVAR
  request : boolean;
VAR
  ctrl : controller(request);
INVARSPEC ctrl.phase != error;
LTLSPEC G (ctrl.active -> F ctrl.ack);
CTLSPEC EF ctrl.active;

MODULE controller(req)
VAR
  phase : {idle, busy, done, error};
DEFINE
  accepting := phase = idle;
  active := phase = busy;
  ack := phase = done;
ASSIGN
  init(phase) := idle;
  next(phase) := case
    (phase = idle) & req : busy;
    phase = busy : done;
    phase = done : idle;
    TRUE : phase;
  esac;

controller(req)のreqは仮引数です．ctrl : controller(request);でインスタンスを作ると，reqを通じてmainのrequestを参照します．起動時に値を1回コピーする仕組みではなく，各状態・遷移で接続先の式の値を参照します．今回は引数を読み取りだけに使います．

ctrl.phaseはインスタンスctrlの内部の状態変数です．ドットでモジュールの内側を参照します．controllerという定義そのものと，ctrlというインスタンスを区別してください．

DEFINEは導出値¶

activeとackは，現在のphaseから計算できる式です．DEFINEで名前を付けると，性質を読みやすくできます．

定義	意味
`accepting := phase = idle;`	今，要求を受理できる状態
`active := phase = busy;`	今，処理中である
`ack := phase = done;`	今，応答段階である

これらは新しい状態変数ではなく，独立した初期値や次状態を持ちません．init(ack)やnext(ack)への代入を追加しません．phaseから導ける値を別の状態変数にすると，更新のずれにも注意が必要になります．状態数との関係は第5回で扱います．

確認： 4.3節と同じ手順でこのファイルを読み込み，3つの性質が真であることを確かめます．フラットなモデルとの違いは構造と名前であり，この例の遷移の意味は同じです．

4.6 環境をモデルとして接続する¶

任意の入力と，特定の環境¶

controller_environment.smvでは，要求を交互に出す環境を接続します．controllerの定義は4.5節と同じで，mainと環境の定義は次です．これだけではファイル全体ではないので，下にMODULE controller(req)以降も残してください．

MODULE main
VAR
  env : environment;
  ctrl : controller(env.request);
INVARSPEC ctrl.phase != error;
LTLSPEC G (ctrl.active -> F ctrl.ack);
CTLSPEC EF ctrl.active;

MODULE environment
VAR
  request : boolean;
ASSIGN
  init(request) := FALSE;
  next(request) := !request;

ここではrequestは環境の状態変数です．FALSE → TRUE → FALSE → …と変化します．任意の入力を表したIVAR版とは，許す入力列の範囲が異なります．

flowchart LR
    E[環境 environment] -->|env.request| C[制御器 controller]
    C -->|ctrl.ack| A[応答の観察]

接続しても更新は同期的¶

環境が次の要求を計算し，その更新済みの値を使って制御器が動くという逐次実行ではありません．両方とも現在状態を参照して，次状態を同時に決めます．

遷移回数	`env.request`	`ctrl.phase`	次の遷移で制御器が参照する要求
0	`FALSE`	`idle`	`FALSE`なので待機を続ける
1	`TRUE`	`idle`	`TRUE`なので処理へ進む
2	`FALSE`	`busy`	要求に関係なく応答へ進む
3	`TRUE`	`done`	要求に関係なく待機へ戻る
4	`FALSE`	`idle`	`FALSE`なので待機を続ける

pick_state -vとsimulate -v -k 4で照合します．環境の要求は状態なので，トレースでもStateの値として表示されます．前のIVAR版のInput表示との違いも確認します．

同じモジュールを複数使う¶

controllers_shared.smvは，a : controller(request);とb : controller(request);で2つの制御器を作ります．内部状態はそれぞれ別ですが，同じ初期値・同じ要求・同じ決定的な遷移を使うので，同時に処理中になります．

INVARSPEC !(a.active & b.active);は偽です．複数のモジュールに分けただけで共有資源の相互排他が実現するわけではありません．必要なら，どちらに許可を出すかを決める調停器などを別にモデル化します．

4.7 制約とデッドロックを確認する¶

INIT・INVAR・TRANSの役割¶

記述	制約する対象	例の意味
`INIT phase = idle;`	初期状態	初期値を待機に限る
`INVAR phase != error;`	各状態	異常状態をモデルから除外する
`TRANS next(phase) != error;`	現在状態と次状態の関係	次が異常になる遷移を除外する

これらはASSIGNなど，ほかの記述と合わせて制約を課します．後ろに書いた制約が前の指定を上書きするわけではありません．今回は意味の区別を学び，基本モデルの記述は引き続きASSIGNを中心にします．

INVARSPECは性質を調べ，INVARはモデルを制限します．要求を真にする目的だけで違反状態をINVARで除外すると，確認するべき振る舞いを隠すことになります．環境の仮定を加える場合も，なぜその振る舞いを除外できるかを説明します．

遷移できない状態を作ってしまう例¶

controller_deadlock.smvは，4.2節のモデルの末尾に次を追加したものです．

TRANS phase != busy;

ここにnextはありません．現在状態がbusyである遷移をすべて除外します．idleからbusyには入れますが，入った後には次状態が存在しません．これが今回のデッドロックです．

reset，read_model -i controller_deadlock.smv，goの後に，次を実行します．

check_fsm

出力にはThe transition relation is not totalと，phase = busyのデッドロック状態が表示されます．正常な入力モデルではThe transition relation is total: No deadlock state existsと表示されます．

デッドロックがある場合は先にモデルを見直します

無限の実行を前提とした時相論理の結果を解釈する前に，意図せず次状態をなくしていないかを確認します．制約を追加した後はcheck_fsmも実行してください．今回の修正は，不適切に加えたTRANSを取り除いて元の遷移を復元することです．

4.8 公平性という仮定【発展・任意】¶

controller_wait.smvでは，処理中を{busy, done}にします．第3回と同じく，処理を続ける経路があるので応答の活性は偽です．

controller_fair.smvでは，さらに次の公平性を指定します．

FAIRNESS phase != busy;

これは検証対象とする公平な経路上で，phase != busyが無限に何度も成立することを求めます．busyに永遠に留まる経路が対象から外れるため，このモデルの応答のLTL式は真になります．有限の回数だけ処理を続けてから完了する経路は許されます．

公平性は「何回以内に完了する」という上限でも，完了を確率で保証する指定でもありません．シミュレーションで完了の候補を選ぶ操作とも異なります．また，この公平性は待機し続ける経路を除外しないため，要求や処理開始が必ず起きる保証ではありません．

確認： この結果は「公平性の仮定を満たす経路では応答する」という意味です．現実の処理にその仮定を置ける根拠がなければ，モデルの問題を解決したとは言えません．公平性と各検証手法の関係にも注意が必要です．この回では応答のLTL式について比較します．

4.9 演習¶

演習1：読み込みから個別検証まで【基本】¶

controller_input.smvを読み込み，構築，一覧表示，種類ごとの検証を行います．一覧のLTL式の番号を確認して，その式だけを再検証してください．

解答例と解説

次の順で操作します．

read_model -i controller_input.smv
go
show_property
check_invar
check_ltlspec
check_ctlspec
show_property

すべて真です．LTL式が番号001であればcheck_ltlspec -n 1で指定できます．種類の違う式の番号を渡さないよう，一覧を確認します．

自己確認： read_modelとgoの役割，未検証と真の違いを説明します．ファイルを編集した後は，保存だけでなくresetから再構築する必要があることも確かめます．

演習2：要求の有無を自分で選ぶ【基本】¶

初期状態から，要求を出さずに1回待機し，次に要求を出して処理，応答，待機へ進みます．各遷移でsimulate -i -k 1を使い，最後にトレースを表示します．

ヒント

最初はidleへ留まる候補を，次はbusyへ進む候補を選びます．番号ではなく，表示された状態と入力を確認します．

解答例と解説

pick_state -vから始め，4回の遷移を選ぶと，状態列はidle → idle → busy → done → idleです．最初の入力はFALSE，次はTRUEです．処理中と応答段階での入力はどちらでも，この状態列になります．show_traces -vで照合します．

自己確認： Input: 1.2が初期状態そのものの値ではなく，次の状態へ進む遷移の入力であることを説明します．この経路を選んでも，ほかの入力列が検証対象から除外されない点も確認してください．

演習3：導出値とモジュールを読む【基本】¶

controller_modules.smvについて，ctrl.phaseとctrl.ackの関係を説明します．性質を検証し，ctrl.activeをctrl.phase = busyに展開した場合の意味も考えます．

解答例と解説

ctrl.ackはctrl.phase = doneの略記であり，独立した状態変数ではありません．同じくctrl.activeはctrl.phase = busyです．したがって応答の式は，フラットなモデルの応答要求と対応し，結果は真です．

間違えやすい点： ackを前の状態の値を記憶する変数だと読むと，応答のタイミングがずれます．DEFINEは現在の式を表し，別の更新を待ちません．

自己確認： モジュールの定義名controller，インスタンス名ctrl，仮引数req，接続先requestをそれぞれ説明します．

演習4：環境と制御器の同時更新【基本】¶

controller_environment.smvを読み込み，初期状態から4回シミュレーションします．実行前にenv.requestとctrl.phaseを表にし，4.6節の表と比較してください．

解答例と解説

0〜4回後の組は，(FALSE, idle)，(TRUE, idle)，(FALSE, busy)，(TRUE, done)，(FALSE, idle)です．最初の遷移では現在の要求が偽なので，制御器は待機します．環境が次に真へ変わることを先取りしません．

自己確認： 1回後を(TRUE, busy)と予想した場合は，更新後の環境の値を使っていないか確認します．現在状態の組を固定してから両方の次状態を計算します．この環境で性質が真でも，任意の入力列を検証したことにはなりません．

演習5：複数の制御器を調べる【確認】¶

controllers_shared.smvの不変条件を検証し，反例で同時に処理中になる理由を説明します．モジュールに分けるだけで相互排他になるかを考えます．

解答例と解説

結果は偽です．初期状態では両方idleで，共通のrequest = TRUEを使う遷移で両方busyになります．トレースにa.phase = busyとb.phase = busyが現れます．

別々のインスタンスは内部状態をそれぞれ持ちますが，排他的な実行の許可は自動では作られません．共有資源へのアクセスを制限するには，どちらかだけに許可する仕組みを記述する必要があります．

自己確認： 「別の変数を持つ」ことと「同時に動かない」ことの違いを説明します．性質を削除することは，相互排他の実現にはなりません．

演習6：制約と公平性の結果を吟味する【発展・任意】¶

controller_deadlock.smvを読み込み，check_fsmで問題を確認します．原因の制約を取り除き，再確認します．
controller_wait.smvとcontroller_fair.smvの応答のLTL式を比較します．何が変わったために結果が変わるか説明します．

解答例と解説

busyから次へ進めない状態が検出されます．TRANS phase != busy;を除くと，遷移関係は全域的となり，デッドロックはなくなります．これは異常状態への到達とは別の問題です．
公平性なしでは応答は偽，ありでは真です．処理を永遠に続ける経路を公平性が検証対象から外すためです．分岐そのものをdoneだけに変えたわけではありません．

自己確認： 公平性を「必ず数回以内で終わる」と説明しないようにします．また，仮定を現実に置ける根拠を考えます．根拠がなければ，公平性なしでの反例が示す問題は未解決です．

4.10 よくある誤りと振り返り¶

状況	見直すこと
OSのコマンドがnuXmvでエラーになる	`quit`でOSに戻ってから実行する
入力ファイルを開けない	OSの作業フォルダーと保存先を確認する
構築前だというエラー	`read_model`の後に`go`を実行する
修正が反映されない	保存してから`reset`と再読み込みを行う
ヘルプ表示でページャーのエラー	`help -p`を使う
シミュレーションで番号を受け付けない	候補選択待ちか，`nuXmv >`かを確認する
モジュール内の名前を参照できない	インスタンス名とドット，定義の名前を確認する
モデルを制約したら結果が不自然	制約の意味，初期状態の存在，`check_fsm`の結果を確認する

読み込み・構築・検証・再読み込みを区別して実行できる（4.3節・演習1）．
入力を選んだトレースと，全経路の検証の違いを説明できる（4.4節・演習2）．
DEFINEと状態変数を区別できる（4.5節・演習3）．
環境と制御器を現在状態から同時更新できる（4.6節・演習4）．
モジュール化だけでは相互排他が保証されないと説明できる（演習5）．
制約や公平性を追加したとき，何を対象から除外したか説明できる（4.7〜4.8節・演習6）．

最後に，入力が任意のモデルと，交互に要求する環境を接続したモデルを比較し，「どの入力列を許したか」「何を観察したか」「どの性質を検証したか」を解説を見ずに説明します．

第5回では，変数や値域が状態空間の大きさに与える影響を調べ，検証したい性質を意識してモデルを簡略化します．

参考資料¶

nuXmv公式ドキュメント：使用バージョンの配布物内マニュアルのRunning interactively，Simulation，MODULE，DEFINE，IVAR，FAIRNESSの説明を参照します．
使用中のnuXmvでは，help -p read_model，help -p simulateなどでコマンドのオプションを確認できます．