第2回：状態遷移図からSMVモデルを書く

第1回では，用意されたモデルをバッチ実行し，反例を読みました．今回は，状態遷移図をもとに自分でモデルを書きます．初期状態と次状態の書き方を学び，変数を増やした場合の同時更新，条件分岐，非決定的な選択へと進みます．

演習では，実行前に状態の列を予想し，実行後に解答例と解説を使って理由を確かめます．性質の書き方は第3回で詳しく扱うため，今回は確認用のINVARSPECを使います．

2.1 到達目標と準備

状態遷移図から状態変数，初期状態，次状態を記述できる．
真偽値（Boolean）型，列挙型，有限範囲の整数を使い分けられる．
複数のnextが現在状態に基づいて同時に更新されることを説明できる．
caseの優先順位と，集合による非決定的な選択を説明できる．
初期値や次状態の指定を省いた場合の振る舞いを説明できる．

内容	目安
準備と，図から基本モデルを作る	25分
型・式・条件分岐	15分
同時更新と非決定性	20分
指定を省く場合の注意	10分
演習と振り返り	20〜40分

第1回の導入手順を終え，nuXmv 2.1.0を実行できることを前提とします．作業フォルダーを新しく用意します．

=== "Windows（PowerShell）"

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

実行ファイルのパスは，第1回で確認した実際の場所に合わせます．最後の結果が`True`であることを確認します．

=== "macOS（Terminal）"

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

実行ファイルのパスは，第1回で確認した実際の場所に合わせます．実行ファイルの情報が表示されることを確認します．

.smvファイルの保存方法と注意点は，第1回の1.5節と同じです．

2.2 状態遷移図をモデルに書き換える

動作を整理する

第1回と同じ制御器を使います．今回も外部入力を省き，待機後は必ず処理に進むものとします．

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

次の順序で，図からコードに必要な情報を取り出します．

状態を表す変数を決める：今回は1つの変数phaseを使う．
取り得る値を列挙する：idle，busy，done，error．
初期状態を決める：idle．
各状態間の矢印をもとに，現在の値と次の値の表を作る．

現在の`phase`	次の`phase`
`idle`	`busy`
`busy`	`done`
`done`	`idle`
`error`	`error`

モデルの入口と状態変数

MODULE main
VAR
  phase : {idle, busy, done, error};

MODULE mainはモデルの入口です．VARの後に，変数名，コロン，型，セミコロンを記述します．波括弧で並べた名前は列挙型の値です．ここでは単語が状態を表しますが，nuXmvが単語の意味から遷移を推測することはありません．

初期状態を書く

ASSIGN
  init(phase) := idle;

ASSIGNは状態の値を記述します． init(phase)への指定は，最初の状態での値を定めます．:=は値を指定する記号です．等しいかどうかを調べる=とは使い方が異なります．

次状態を書く

  next(phase) := case
    phase = idle : busy;
    phase = busy : done;
    phase = done : idle;
    TRUE : phase;
  esac;

next(phase)は次状態でのphaseの値を定めます．case〜esacは条件と，その条件が満たされたときの値の組を記述します．:の左側が現在の状態での条件，右側が条件を満たすときの値です．例えば現在のphaseの値がbusyなら，次のphaseの値はdoneになります．条件は上から順に評価されます．最後のTRUE : phase;は，いずれの条件にも当てはまらない場合に現在の値を保持する分岐です．今回はphaseがerrorのときの自己ループに対応します．

全体を完成させて実行する

次の内容をcontroller_cycle.smvとして保存します．まずは図と各行の対応を考えながら，自分で入力してください．完成例のダウンロードも用意しています．

controller_cycle.smv

MODULE main
VAR
  phase : {idle, busy, done, error};
ASSIGN
  init(phase) := idle;
  next(phase) := case
    phase = idle : busy;
    phase = busy : done;
    phase = done : idle;
    TRUE : phase;
  esac;
INVARSPEC phase != error;

=== "Windows（PowerShell）"

```powershell
& $nuxmvExe .\controller_cycle.smv
```

=== "macOS（Terminal）"

```bash
"$nuxmvExe" controller_cycle.smv
```

期待結果の主要部分は次です．

-- invariant phase != error is true

確認： この結果に加えて，初期状態からidle → busy → done → idleと進む理由をコードから説明します．式が真になるだけでは，図とコードの一致をすべて確認したことにはなりません．

2.3 型と基本的な式

今回使う3種類の型

型	宣言例	取り得る値
真偽値（Boolean）型	`alarm : boolean;`	`TRUE`，`FALSE`
列挙型	`phase : {idle, busy, done};`	指定した名前
範囲付き整数	`cnt : 0..3;`	0，1，2，3

0..3は両端を含みます．この例ではcntは4つの値を取ります．負数を含む範囲も記述できます．状態名のように名前が意味をもつ場合は列挙型，値を用いて計算を行う場合は有限範囲の整数を使います．

有限範囲の整数とinteger

cnt : 0..3;とcnt : integer;は異なります．後者は範囲を限定しない整数で，無限状態モデルとなるため，検証手法も考慮する必要があります．今回は有限状態モデルを扱います．

条件や値を表す式

記号	意味	例
`=`，`!=`	等しい，等しくない	`phase = busy`
`<`，`<=`，`>`，`>=`	数値の比較	`cnt < 3`
`!`	否定	`!alarm`
`&`	かつ	`(phase = busy) & !alarm`
`\|`	または	`(phase = idle) \| (phase = done)`
`->`	含意	`(phase = error) -> alarm`
`+`，`-`	加算，減算	`cnt + 1`

a -> bは，「aが真ならbも真である」ときに真となるという条件式です．aが偽の場合は常に成立します．演習の警報モデルで使います．複数の演算を組み合わせる場合は，括弧でまとまりを明示してください．

SMVの予約語や識別子の大文字・小文字に注意します．TRUEとFALSEは大文字，booleanは小文字です．変数名では大文字と小文字を区別するため，phaseとPhaseは同じ名前として扱いません．コメントは--から行末までです．

変数名には予約された単語や組み込み演算の名前を使いません．例えばcountは組み込み演算の名前なので，この教材ではカウンターの変数をcntとしています．

2.4 caseの優先順位と値域

最初に成立した条件を使う

caseは，条件が真になる最初の分岐の右側の値を選びます．複数の条件が真でも，下の分岐へ進み直すことはありません．

next(cnt) := case
  cnt < 3 : cnt + 1;
  cnt = 2 : 0;
  TRUE : 0;
esac;

現在値が2なら，cnt < 3とcnt = 2の両方が真です．このとき次の値がいくつになるかは，演習2で確かめます．

TRUEの分岐は最後に置きます

TRUE : phase;のような分岐は，「それより上のどの条件にも当てはまらなかった場合」に使われます．

最後に置く理由： TRUEは常に真です．先頭に置くと，現在値が何であってもこの分岐が選ばれ，その下の分岐は一度も使われません．
省略しない理由： どの条件も真にならない現在値があると，次の値が決まりません．その場合に自動で現在値を保つことはないため，最後にTRUEの分岐を置いて，必ずどれかの分岐が選ばれるようにします．

次の値を型の範囲に収める

cnt : 0..3;の変数に対して，単純にnext(cnt) := cnt + 1;と書くと，現在値3で次の値が4になります．これは指定した範囲の外です．nuXmvは範囲外の値への代入をエラーとして報告し，検証を完了しません．上限を超える場合の動作を明示します．

counter.smv

MODULE main
VAR
  cnt : 0..3;
ASSIGN
  init(cnt) := 0;
  next(cnt) := case
    cnt < 3 : cnt + 1;
    TRUE : 0;
  esac;
INVARSPEC cnt <= 2;

このモデルは0 → 1 → 2 → 3 → 0 → …と進みます．確認用の性質は「2以下のままである」なので偽になります．3は型の範囲内なので，この結果は型のエラーではありません．counter.smvを保存し，2.2節の実行コマンドのファイル名をcounter.smvに変えて確認してください．

2.5 全ての変数は同時に更新される

現在状態から次状態をまとめて計算する

次のモデルをswap.smvとして用意します．

swap.smv

MODULE main
VAR
  x : boolean;
  y : boolean;
ASSIGN
  init(x) := FALSE;
  init(y) := TRUE;
  next(x) := y;
  next(y) := x;
INVARSPEC x != y;
INVARSPEC x = FALSE;

初期状態は(x, y) = (FALSE, TRUE)です．2つのnextの右側は，どちらもこの現在状態を参照します．

遷移回数	`x`	`y`	次の`x`（現在の`y`）	次の`y`（現在の`x`）
0	`FALSE`	`TRUE`	`TRUE`	`FALSE`
1	`TRUE`	`FALSE`	`FALSE`	`TRUE`
2	`FALSE`	`TRUE`	`TRUE`	`FALSE`

各行のx・yから右の2列を求め，それを次の行のx・yとします．

したがって，値は入れ替わり続けます．next(x)を書いた後にnext(y)を書くことは，「更新後のxをyに渡す」ことではありません．これら2つの指定の順序を入れ替えても，モデルの振る舞いは同じです．

実行すると，x != yは真，x = FALSEは偽です．後者の反例には，初期状態と1回の遷移後の状態が表示されます．2つの性質をそれぞれ確認してください．

2.6 非決定的な選択を書く

次状態を集合で指定する

処理中から「処理を続ける」「完了する」のどちらにも進める場合は，次のように書きます．

phase = busy : {busy, done};

これは，次の値としてbusyまたはdoneを許す指定です．確率は付いていません．毎回交互に選ぶ指定でもありません．

controller_nondet.smvでは，待機を続ける場合と処理を続ける場合を追加します．

controller_nondet.smv

MODULE main
VAR
  phase : {idle, busy, done, error};
ASSIGN
  init(phase) := idle;
  next(phase) := case
    phase = idle : {idle, busy};
    phase = busy : {busy, done};
    phase = done : idle;
    TRUE : phase;
  esac;
INVARSPEC phase != error;
INVARSPEC phase != busy;

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

可能な経路には，idle → idle → busy → done → idle → …や，idle → busy → busy → …があります．処理を続ける自己ループを何回でも選べるので，必ず完了するとは限りません．

検証では許した選択肢を考える

phase != errorは真です．どの選択を繰り返しても，初期状態からerrorへ進めません．一方，phase != busyは偽です．idle → busyという違反経路が存在するためです．違反しない経路があっても，違反する経路が1つあれば不変条件は偽です．

nuXmvは選択肢を1つずつランダムに試すのではなく，モデルが許すすべての振る舞いについて性質を検証します．

2.7 指定を省いた場合はどうなるのか

初期値を指定しない場合

controller_cycle.smvからinit(phase) := idle;だけを省くと，初期値を制限しなくなります．列挙した4つの値のどれでも初期値になり得ます．変数が自動で最初の列挙値に初期化されるわけではありません．このモデルをcontroller_no_init.smvとして用意しています．

次状態を指定しない場合

init(phase) := idle;は残し，next(phase)への指定全体を省くと，初期状態はidleですが，次状態は4つの値のどれでも許されます．「指定しないので値を保つ」とは解釈されません．値を保つにはnext(phase) := phase;と明示します．

next(phase)の指定を省いたモデルをcontroller_no_next.smvとして用意しています．

2.8 演習

各演習では，まず結果を予想してから実行し，その後に解答例と解説を開いて予想と比べます．完成例のファイルへのリンクは，解答例と解説の中にあります．

演習1：図からモデルを完成させる【基本】

信号機を次の状態遷移図で表します．通常は青・黄・赤の順に切り替わります．offは消灯（故障）を表し，一度入ると留まります．

stateDiagram-v2
    [*] --> green
    green --> yellow
    yellow --> red
    red --> green
    off --> off

2.2節の手順で，変数，取り得る値，初期状態，現在値と次の値の表を書き出します．変数名はlightとします．
次の空欄を埋め，signal.smvとして保存します．___は説明用の空欄であり，そのままでは実行できません．
初期状態から3回遷移した状態の列を書きます．
バッチ実行し，性質の結果を予想と比べます．
図の各矢印を，コードの行と対応させて説明します．

MODULE main
VAR
  light : ___;
ASSIGN
  init(light) := ___;
  next(light) := case
    ___
  esac;
INVARSPEC light != off;

ヒント

caseの各行は，2.2節と同じく「現在値の条件 : 次の値;」の形です．offのように値を保つ状態は，最後の分岐で現在値を表す変数名を使えます．

解答例と解説

全体の完成例は次のとおりです．

MODULE main
VAR
  light : {green, yellow, red, off};
ASSIGN
  init(light) := green;
  next(light) := case
    light = green : yellow;
    light = yellow : red;
    light = red : green;
    TRUE : light;
  esac;
INVARSPEC light != off;

経路はgreen → yellow → red → green，検証結果は真です．offは型に含まれますが，初期状態から到達しません．

最後の分岐をlight = off : off;と書いても，このモデルでは残りの条件に該当する値はoffだけなので，同じ遷移になります．ただし，TRUE : light;と書く方が「現在値を保つ」という意図を直接表します．

間違えやすい点： red : greenのつもりでred : yellowと書いても，light != offは真のままです．検証結果だけでなく，各矢印とコードの行を1つずつ照合します．

演習2：条件の優先順位を直す【基本】

counter_priority.smvを用意します．2.4節の優先順位の例を全体のモデルにしたものです．

初期値0から3回遷移した後の値を求めます．
cnt <= 2の結果を予想して実行します．
「2まで数えたら0に戻る」ように分岐の順序を変更し，counter_priority_fixed.smvとして実行します．型と性質は変更しません．

ヒント

現在値2で真になる条件をすべて挙げ，先に書かれている条件を選んでください．

解答例と解説

修正前は0 → 1 → 2 → 3なので，3回後は3，性質は偽です．2では最初のcnt < 3が真となるため，下のcnt = 2は選ばれません．

修正後の指定は次です．全体の完成例も参照できます．

next(cnt) := case
  cnt = 2 : 0;
  cnt < 3 : cnt + 1;
  TRUE : 0;
esac;

修正後は0 → 1 → 2 → 0 → …となり，結果は真です．型には3を残していますが，初期値0から3へは到達しません．

間違えやすい点： 型を0..2に狭めるだけでは，元の分岐で2から3を計算する問題は解決しません．値域と，値を生成する式の両方を確認します．

演習3：同時更新を手で追う【基本】

swap.smvをコピーしてswap_not.smvとし，next(x) := y;をnext(x) := !y;に変更します．next(y) := x;と2つの性質はそのままにします．

初期状態から4回遷移するまでの(x, y)を，現在値と次の値を分けて表にします．
x != yとx = FALSEの結果と，それぞれの反例の状態数を予想して実行します．
next(x)とnext(y)の指定の順序を入れ替えると結果が変わるか考えます．

解答例と解説

遷移回数	`x`	`y`	次の`x`（`!y`）	次の`y`（`x`）
0	`FALSE`	`TRUE`	`FALSE`	`FALSE`
1	`FALSE`	`FALSE`	`TRUE`	`FALSE`
2	`TRUE`	`FALSE`	`TRUE`	`TRUE`
3	`TRUE`	`TRUE`	`FALSE`	`TRUE`
4	`FALSE`	`TRUE`

4回の遷移で初期状態に戻り，この4状態を繰り返します．全体の完成例も参照できます．

x != yは偽で，1回後の(FALSE, FALSE)が違反です．反例は2状態です．x = FALSEも偽で，2回後の(TRUE, FALSE)が最初の違反です．反例は3状態です．指定の順序を入れ替えても，両方の右側が現在状態を参照するため，結果は変わりません．

間違えやすい点： 遷移回数2を(TRUE, TRUE)と予想した場合は，更新後のx（TRUE）をyの計算に使っています．next(y)の右側のxは，現在のx（FALSE）です．

演習4：非決定的な遷移を追加する【基本】

「待機からは必ず処理に進む．処理中は継続，完了，異常のいずれかに進む．完了と異常からは待機に戻る」という説明をモデルにします．controller_retry.smvとして保存してください．

変数，型，初期状態を決めます．初期状態は待機です．
状態遷移図を描き，next(phase)を記述します．
処理が継続する経路と，異常状態に至る経路をそれぞれ書きます．
INVARSPEC phase != error;の結果を予想し，実行します．

ヒント

処理中の選択肢は集合で書きます．異常から待機への遷移は，最後の値保持の分岐より前に置きます．

解答例と解説

phase : {idle, busy, done, error};，init(phase) := idle;を使い，次状態を次のように指定します．全体の完成例で確認できます．

next(phase) := case
  phase = idle : busy;
  phase = busy : {busy, done, error};
  phase = done : idle;
  phase = error : idle;
  TRUE : phase;
esac;

継続する経路はidle → busy → busy → …，異常に至る経路はidle → busy → errorです．異常に至る経路が存在するので結果は偽です．error → idleで回復できても，一度異常状態に入った時点で今回の性質に違反します．

間違えやすい点： {busy, done, error}は，3つの値をその順に実行する指定ではありません．異常に進む確率が1/3という意味でもありません．

演習5：警報が遅れる理由を考える【発展・任意】

controller_alarm.smvでは，状態変数alarmを加えます．idle → busy → errorと進むモデルで，警報は次のように書かれています．

init(alarm) := FALSE;
next(alarm) := (phase = error);

確認する性質はINVARSPEC (phase = error) -> alarm;です．これは「異常状態なら警報が真である」という意味です．

初期状態から3回遷移するまでの(phase, alarm)を求めます．
性質の結果を予想して実行します．
next(alarm)をnext(phase)より後に書けば解決するか説明します．
このモデルについて，異常に入る遷移と同時に警報が真になるようにnext(alarm)の右側を修正します．

ヒント

異常に入る直前の現在状態はbusyです．現在状態がerrorになってから警報を更新すると，1回遅れます．

解答例と解説

遷移回数	`phase`	`alarm`
0	`idle`	`FALSE`
1	`busy`	`FALSE`
2	`error`	`FALSE`
3	`error`	`TRUE`

結果は偽です．2回目の遷移では，現在のphaseはbusyです．next(phase)はerrorを選びますが，next(alarm)の右側のphase = errorは偽なので，警報は偽のままです．3回目で初めて真になります．記述順序を変えても，同時更新の意味は変わりません．

このモデルに限れば，次の指定で修正できます．

next(alarm) := (phase = busy) | (phase = error);

busyから異常に入るときに警報を真にし，errorに留まるときも真を保ちます．後半のphase = errorを省くと，異常状態に留まった次の遷移で警報が偽になるので不十分です．修正後の性質は真です．

適用範囲： この修正は，busyの次は必ずerrorであり，errorでは留まるという今回の遷移に基づきます．非決定的に完了や継続も選ぶモデルに，そのまま適用できるとは限りません．

演習6：指定を省いたモデルを比較する【基本】

2.7節のcontroller_no_init.smvとcontroller_no_next.smvについて，phase != errorの結果と反例の状態数を予想してから実行します．反例の状態数が異なる理由を説明し，どちらの指定を戻せば元の周期モデルになるか考えてください．

解答例と解説

どちらの結果も偽です．初期値を省いたモデルは，errorを初期値として許すため，1状態の反例になります．次状態を省いたモデルは，初期値はidleですが，次にerrorを選べるため，idle → errorという2状態の反例になります．「書かない」ことは「現在値を保つ」ことではありません．

前者にはinit(phase) := idle;，後者には2.2節のnext(phase)全体を戻します．次状態を省いたモデルにnext(phase) := phase;だけを追加すると，idleに留まるので今回の性質は真になりますが，処理も応答も起こらず，元の周期モデルにはなりません．

2.9 よくある誤り

初めてモデルを書くときに起こりやすい誤りを，nuXmvがエラーで止まるものと，エラーなく実行されるものに分けて示します．後者は検証結果が出るため，気付きにくい誤りです．

エラーで止まる誤り

誤った書き方	正しい書き方	原因
`phase == idle`，`a && b`，`a \|\| b`	`phase = idle`，`a & b`，`a \| b`	C言語やPythonの記号を使った．SMVの等号は`=`が1つ，論理演算は`&`・`\|`です
`init(phase) = idle;`	`init(phase) := idle;`	値の指定には`:=`を使う
`phase = idle := busy;`	`phase = idle : busy;`	`case`の分岐は「条件`:`値`;`」の形
`esac`（`;`なし），分岐末尾の`;`忘れ	`esac;`，`phase = idle : busy;`	エラーの行番号は，`;`を忘れた行の次の行を指すことがある
`alarm := true;`，`phase = Idle`	`alarm := TRUE;`，`phase = idle`	大文字・小文字が宣言と違う．`TRUE`・`FALSE`は大文字
`next(phase)`を状態ごとに分けて2回書く	1つの`case`にまとめる	同じ変数の`next`は1か所でしか指定できない
`cnt : 0..3;`で`next(cnt) := cnt + 1;`	上限で`0`に戻す分岐を加える（2.4節）	現在値3のとき次の値が4になり，型の範囲を超える

エラーにならない誤り

誤った考え方	実際の振る舞い	戻る節
`cnt < 3 : cnt + 1;`の下に`cnt = 2 : 0;`を書けば，2で0に戻る	先に真になった`cnt < 3`が選ばれ，3へ進む	2.4節・演習2
`next(x) := y;`の後に`next(y) := x;`と書けば，`y`には更新後の`x`が入る	右側の`x`は現在値．指定の順序は関係ない	2.5節・演習3
`{busy, done}`は「`busy`の次に`done`」の意味	どちらか一方を選べる指定．順番も確率もない	2.6節・演習4
変数`alarm`を追加したが，`init(alarm)`を書かなくても`FALSE`から始まる	初期値は`TRUE`・`FALSE`のどちらでもよくなり，想定外の初期状態から反例が出る	2.7節
`next`を書かなかった変数は値を保つ	次の値は型のどの値にもなり得る	2.7節・演習6
性質が真なので，図どおりのモデルになっている	性質に関係しない遷移の誤りは検出されない	演習1

起動，保存，ファイル指定の問題は第1回のトラブルシューティングも参照してください．

2.10 振り返り

次の各項目を，解説を見ずに説明できるか確かめます．

[ ] 図の状態と矢印を，VAR・init・nextに対応させられる（2.2節・演習1）．
[ ] 型に含まれる値と，実際に到達する値を区別できる（2.3節・演習2）．
[ ] caseで複数の条件が真になった場合の値を求められる（2.4節・演習2）．
[ ] 複数の変数の次状態を，現在状態からまとめて求められる（2.5節・演習3）．
[ ] 非決定的な選択は，順番や確率の指定ではないと説明できる（2.6節・演習4）．
[ ] 指定を省いた変数が自動で値を保つわけではないと説明できる（2.7節・演習6）．

最後に，自分で書いたモデルから1つ選び，「何を状態として記録したか」「どこから始まるか」「各状態からどこへ進めるか」「何を検証したか」を順に説明してください．

第3回では，検証したい要求を自分で性質として記述し，安全性と活性，反例に基づく修正を学びます．

参考資料

nuXmv公式ドキュメント：使用するバージョンの配布物内のマニュアルでは，Input Languageの型，Case Expressions，ASSIGNの説明を参照します．
NuSMV公式チュートリアル：基礎となる有限状態モデルの例．古い資料のため，コマンドや文法の細部はnuXmvの使用バージョンで確認してください．