第5回：状態爆発を理解する――モデルを小さくする工夫¶
第4回では，複数の構成要素を接続しました．変数や構成要素を増やすと，取り得る状態の組み合わせは急速に増えます．今回は，状態数を見積もり，実際の到達可能な状態数と比較しながら，モデルを簡略化します．
小さくした後は，性質の真偽に加えて，必要な振る舞いを保っているかを確認します．演習では予想，実行，解答・解説との比較を行い，自分で変更の妥当性を説明します．成果物の提出は求めません．
5.1 到達目標と準備¶
- 変数の値域から，状態数の上限を計算できる．
- 取り得る状態の総数と，到達可能な状態数を区別できる．
- 値域の見直し，
DEFINE，不要な変数の削除を使い分けられる． - 抽象化で増えた振る舞いと，元のモデルの振る舞いを比較できる．
- 状態空間を小さくすることと，BDDによる表現や検証を効率化することを区別できる．
| 内容 | 目安 |
|---|---|
| 準備と状態数の見積もり | 15分 |
| 到達可能な状態数の確認 | 15分 |
| 値域・導出値・不要な変数の見直し | 25分 |
| 抽象化と検証の効率化 | 20分 |
| 演習と振り返り | 25〜40分 |
nuXmv 2.1.0を使用します．作業フォルダーを用意し，実行ファイルのパスを自分の展開先に合わせて設定します．
New-Item -ItemType Directory -Force -Path "$HOME\nuxmv-tutorial\lesson05"
Set-Location "$HOME\nuxmv-tutorial\lesson05"
$nuxmvExe = "$HOME\Downloads\nuXmv-2.1.0-win64\bin\nuXmv.exe"
Test-Path $nuxmvExe
最後の結果がTrueであることを確認します．
mkdir -p "$HOME/nuxmv-tutorial/lesson05"
cd "$HOME/nuxmv-tutorial/lesson05"
nuxmvExe="$HOME/Downloads/nuXmv-2.1.0-macos-universal/bin/nuXmv"
ls -l "$nuxmvExe"
実行ファイルの情報が表示されることを確認します．
ファイルはプレーンテキスト，UTF-8（BOMなし）で保存します．ファイルの保存方法は第1回，インタラクティブ実行は第4回と同じです．
5.2 状態数を見積もる¶
状態変数の値域の積¶
状態は，状態変数の値の組です．他の制約を考える前の組み合わせの数は，各変数の取り得る値の数を掛け合わせて計算します．
| 宣言 | 値の数 |
|---|---|
phase : {idle, busy, done, error}; |
4 |
alarm : boolean; |
2 |
ticks : 0..15; |
16 |
この3変数なら4 × 2 × 16 = 128通りです．Boolean変数をさらに1つ追加すると256通りになります．独立したBoolean変数がn個なら2^n通りです．構成要素を増やす場合も，内部状態の組み合わせを考えます．
入力と導出値は別に数えます
今回数えるのは状態変数の値の組です．IVARは遷移時の入力で，そのまま状態変数の積には含めません．ただし入力の種類は遷移の選択肢に影響します．DEFINEも独立した状態変数ではないため，積に含めません．
取り得る状態と到達可能な状態¶
第1回の制御器は4つの状態名を持ちますが，idle → busy → done → idleと繰り返すので，初期状態から到達可能なのは3状態です．型から得られる総数と，到達可能な状態数は一致するとは限りません．
この資料では，型の値域の積を状態数の上限と呼びます．INVARなどで状態を制約している場合は，実際の有効な状態の総数もそれより小さくなり得ます．今回の数値比較用モデルでは，そのような状態制約や公平性を使いません．
5.3 nuXmvで到達可能な状態数を調べる¶
状態数を確認する手順¶
controller_core.smvを作業フォルダーへ保存し，OSのシェルで起動します．
& $nuxmvExe -int
"$nuxmvExe" -int
nuXmv >に次を入力します．
read_model -i controller_core.smv
go
print_reachable_states
check_invar
check_ltlspec
このモデルは，4つの状態名を持つ周期的な制御器です．出力の主要部分は次です．
reachable states: 3 (2^1.58496) out of 4 (2^2)
reachable states: 3が到達可能な状態数です．out of 4はこのモデルの取り得る状態の総数です．括弧内は同じ数を2のべきで表したものなので，小数が含まれていても状態数が小数という意味ではありません．
小さなモデルでは，次で具体的な状態も表示できます．
print_reachable_states -v
idle，busy，doneが表示され，errorが含まれないことを確認します．大きなモデルで-vを使うと大量に表示されるため，まず数だけを調べます．
比較するたびに読み込み直す¶
別のファイルを調べる場合は，次のようにします．
reset
read_model -i controller_log.smv
go
print_reachable_states
check_invar
check_ltlspec
上の例を実行する前に，controller_log.smvも保存します．ほかの比較でも，read_modelのファイル名を対象に置き換えます．保存したモデルを編集した場合も，resetからやり直します．
到達可能な状態の計算にも費用がかかります
print_reachable_statesは，必要なら到達可能な状態を計算します．単に宣言の数を表示するだけのコマンドではありません．今回の小さな例で操作を覚え，大きなモデルで無条件に実行することは避けます．
5.4 使っていない値域を見直す¶
大きく宣言しすぎたカウンター¶
timer_wide.smvは，3に達したら値を保つタイマーです．
MODULE main
VAR
ticks : 0..15;
ASSIGN
init(ticks) := 0;
next(ticks) := case
ticks < 3 : ticks + 1;
TRUE : ticks;
esac;
INVARSPEC ticks <= 3;
LTLSPEC F (ticks = 3);
取り得る値は16個ですが，到達するのは0 → 1 → 2 → 3 → 3 → …の4個です．初期値が0で，3より小さいときだけ1増やすので，4以上にはなりません．
timer_narrow.smvでは，宣言だけをticks : 0..3;に変えます．この初期値と遷移なら，初期状態からの振る舞いを保ったまま値域を狭められます．
| モデル | 状態数の上限 | 到達可能な状態数 | 2つの性質 |
|---|---|---|---|
timer_wide.smv |
16 | 4 | 両方真 |
timer_narrow.smv |
4 | 4 | 両方真 |
重要な違い： この変更では，上限は減りますが，到達可能な状態数は減りません．符号化に必要なビット数を減らせる可能性がありますが，実行時間が必ず短くなるとは限りません．
根拠なく値域を狭めない¶
初期値や遷移が4以上を使うなら，今回の変更はそのまま適用できません．例えばnext(ticks) := ticks + 1;に対して宣言だけを狭めても，上限で範囲外の値を作る問題は解決しません．
また，10回後に起きるバグを，カウンターを3までにして探しても，元のシステムを確認したことにはなりません．値域を狭める前に，その値が本当に到達しないのか，検証したい振る舞いを除いていないかを説明します．
5.5 導出できる値をDEFINEにする¶
状態として保持している応答フラグ¶
controller_stored.smvは，周期モデルのphaseに加え，応答フラグackをBooleanの状態変数として持ちます．重要な部分は次です．
VAR
phase : {idle, busy, done, error};
ack : boolean;
ASSIGN
init(ack) := FALSE;
-- phaseの初期値と遷移は周期モデルと同じ
next(ack) := phase = busy;
INVARSPEC ack = (phase = done);
この断片だけでは実行できないため，全体は配布ファイルを使います．現在のphaseがbusyなら，次のphaseはdoneとなり，次のackも真になります．初期状態からは，常にack = (phase = done)が成立します．
現在状態の式として表す¶
controller_define.smvでは，ackの状態変数宣言と初期値・次状態の指定を取り除き，次を使います．
DEFINE
ack := phase = done;
この例では，保持していた値と現在のphaseから計算した値が到達可能な状態で一致するため，検証していた応答の意味を保てます．
| モデル | 状態数の上限 | 到達可能な状態数 |
|---|---|---|
controller_stored.smv |
4 × 2 = 8 |
3 |
controller_define.smv |
4 | 3 |
到達可能な状態数はどちらも3です．元のモデルでもackとphaseの組に相関があり，8通りすべてには到達しないためです．状態として保持する情報は減りますが，到達可能な状態数が半分になるわけではありません．
過去の情報を持つ変数は単純にDEFINEへ置き換えられません
「過去に異常が1回でも起きた」など，現在のほかの変数だけから決まらない履歴には記憶が必要です．現在の異常状態の式に置き換えると，異常から回復した後に意味が変わります．今回のように一致する根拠を確認してから変更します．
5.6 検証に不要な状態変数を除く¶
controller_log.smvでは，制御器にlog_tick : 0..3;を追加します．初期値0から，毎回(log_tick + 1) mod 4に更新します．log_tickは制御器の遷移にも，今回の安全性・応答の性質にも使いません．
元の制御器は3段階の周期，記録用カウンターは4段階の周期なので，組は12回の遷移で初期状態に戻ります．
| 遷移回数 | phase |
log_tick |
|---|---|---|
| 0 | idle |
0 |
| 1 | busy |
1 |
| 2 | done |
2 |
| 3 | idle |
3 |
| 4 | busy |
0 |
| 5 | done |
1 |
log_tickを除いたcontroller_core.smvと比較します．
| モデル | 状態数の上限 | 到達可能な状態数 | 安全性と応答 |
|---|---|---|---|
| 記録変数あり | 4 × 4 = 16 |
12 | 両方真 |
| 記録変数なし | 4 | 3 | 両方真 |
今回は到達可能な状態数も減ります．記録値を無視してphaseだけを見ると同じ周期となり，残した変数の遷移にlog_tickが影響しないためです．
ただし，記録間隔やログの欠落を検証したい場合は不要ではありません．また，検証式で直接使わなくても，他の変数の更新条件に使う変数は影響します．削除する前に，性質と遷移の両方からの依存関係を確認してください．
5.7 抽象化で細部をまとめる¶
具体値をカテゴリに置き換える¶
data_concrete.smvは，3から0まで値を減らし，0に留まるモデルです．
MODULE main
VAR
value : 0..3;
ASSIGN
init(value) := 3;
next(value) := case
value > 0 : value - 1;
TRUE : 0;
esac;
LTLSPEC G ((value = 0) -> X (value = 0));
LTLSPEC F (value = 0);
値を正確に区別せず，0をzero，1・2・3をpositiveにまとめます．data_abstract.smvは次です．
MODULE main
VAR
category : {zero, positive};
ASSIGN
init(category) := positive;
next(category) := case
category = positive : {positive, zero};
TRUE : zero;
esac;
LTLSPEC G ((category = zero) -> X (category = zero));
LTLSPEC F (category = zero);
具体モデルの3 → 2と2 → 1は，抽象モデルではpositive → positiveです．1 → 0はpositive → zeroになります．具体モデルの各遷移を対応させるため，抽象モデルでは両方を許します．
flowchart LR
A["具体: 3 → 2 → 1 → 0 → 0 …"] -->|値をカテゴリに対応させる| B["抽象: positive → positive → positive → zero → zero …"]状態をまとめると，余分な振る舞いを許すことがある¶
| 性質 | 具体モデル | 抽象モデル |
|---|---|---|
| 0になったら次も0 | 真 | 真 |
| いつか0になる | 真 | 偽 |
抽象モデルには，positive → positive → positive → …という経路があります．元のモデルは毎回値が減るので，この無限の経路はありません．減少に関する情報をまとめたため，抽象モデルに余分な経路が加わっています．
この余分な経路による反例は，元のモデルに対応しない見かけの反例です．抽象モデルが偽でも，すぐに元のモデルのバグとは結論できません．具体値や遷移と照合し，必要なら情報を戻して抽象化を細かくします．
今回は，各具体状態を対応するカテゴリに写すと，初期状態も各1回の遷移も抽象モデルで表せます．この対応と，検証する式の対応を確認することが重要です．任意のモデル変更について，同じ保存関係が自動的に得られるわけではありません．
削除，値域の縮小，抽象化は同じ操作ではありません
使わない値を除く例では初期状態からの振る舞いを保ちました．今回の抽象化では具体的な区別を失い，余分な振る舞いを許します．単に値を小さくした場合に，どちらの関係が得られるかは別途確認が必要です．
5.8 状態数の削減と検証の効率化を区別する¶
BDDのサイズは状態数そのものではない¶
nuXmvは，今回の手順ではBDDという論理関数の表現を使って，状態集合や遷移関係を扱います．すべての状態を1つずつ列挙して保存するとは限りません．
したがって，到達可能な状態数が多くてもコンパクトに表せる場合があり，逆に同じ状態数でも表現が大きくなる場合があります．BDDの変数順序を変えると表現の大きさが変わることがありますが，それ自体でモデルの意味上の状態数が減るわけではありません．
次は，モデル構築後に確認できる情報の例です．
print_fsm_stats
usage
print_fsm_statsは遷移関係の分割などの情報とBDDノード数を含む統計を表示します．usageはプロセスの資源利用に関する情報で，表示内容はOSによって異なります．どちらも到達可能な状態数とは別の指標です．
発展として，次はBDDの変数順序を明示的に見直す操作です．
dynamic_var_ordering -f sift
実行時間を使って表現を改善する処理なので，小さなモデルで速くなるとは限りません．今回の演習では状態数の比較を優先し，この操作は任意とします．
性質に関係する部分への絞り込み¶
検証する式から，その値に影響する変数や遷移をたどり，関連部分に絞る考え方をcone of influence（COI）と呼びます．検証のための絞り込みと，元のモデル全体の状態数は区別します．性質に現れない変数でも，関連する変数の更新に使うなら無関係ではありません．
今回の状態数比較では，COIなどの追加の絞り込みを有効にせず，同じread_modelとgoの手順でモデル全体を比べます．ツール側で関係のない変数を除く設定を使う場合は，何を対象に数えたかも記録してください．
測定条件をそろえる¶
比較するときは，nuXmvのバージョン，PC，検証する式，コマンド，設定をそろえます．新しいnuXmvプロセスで同じ手順を実行すると，前の計算結果や資源統計の累積の影響を分けやすくなります．
print_reachable_statesを先に行う場合と，行わずに検証する場合は，同じ測定として扱いません．今回の小さな例では起動などの費用も大きいため，時間差が見えなくても失敗ではありません．状態数がどう変わり，性質と振る舞いがどう対応するかを説明することを優先します．
5.9 演習¶
演習1：組み合わせの増え方を確認する【基本】¶
flags4.smvとflags8.smvを保存します．それぞれ4個と8個のBoolean状態変数を持ち，初期値と次状態を制限していません．状態数の上限と到達可能な状態数を予想して，print_reachable_statesで確認します．
解答例と解説
4個なら2^4 = 16，8個なら2^8 = 256です．初期状態で全組み合わせを許すので，どちらも上限と到達可能な状態数が一致します．変数が2倍になると状態数も2倍，ではありません．この例では16倍です．
確認用のINVARSPEC flag0 | !flag0;は常に成立する式です．実用的な安全性の要求ではなく，実行できる性質を添えたものです．ほかのフラグに関する振る舞いを保証する式ではありません．
自己確認： 第2回で学んだ「初期値を省く」と「次状態を省く」の意味から，なぜ全組み合わせを許すか説明します．数が多くてもBDDが同じ比率で大きくなるとは限らない点も区別します．
演習2：値域を見直す【基本】¶
timer_wide.smvの到達可能な値を予想し，検証します．次に宣言だけを0..3に変更し，timer_narrow.smvとして保存します．変更前後の状態数の上限，到達可能な状態数，性質の結果を比較してください．
ヒント
3になった後にどの分岐が選ばれるか確認します．宣言した範囲の値をすべて通るわけではありません．
解答例と解説
上限は16から4へ減りますが，到達可能な状態数は両方4です．不変条件と完了のLTL式は両方真です．初期値0から3まで増え，その後は現在値を保つため，4以上を除いても到達する振る舞いは変わりません．
自己確認： 結果の真偽が一致しただけでなく，変更前の到達状態が新しい型に収まり，初期値と遷移も同じであることを説明します．上限と到達数を混同した場合は5.2〜5.3節へ戻ります．
演習3：保持する値と導出値を比較する【基本】¶
controller_stored.smvとcontroller_define.smvで，到達可能な状態数と3つの性質を比較します．ackを現在状態の式に置き換えてよい理由を説明してください．
解答例と解説
状態数の上限は8から4へ減り，到達可能な状態数は両方3です．安全性，ack = (phase = done)，応答のLTL式はすべて真です．
保持するモデルでは，到達する組は(idle, FALSE)，(busy, FALSE)，(done, TRUE)です．DEFINEで計算する値も同じです．置き換え後の一致条件は定義から真になりますが，置き換える前にも一致することが重要です．
自己確認： 「すべてのBoolean変数はDEFINEで消せる」と一般化しないでください．過去の異常を記憶する場合に，現在のphaseだけでは足りない例を考えます．
演習4：不要な記録変数を除く【基本】¶
controller_log.smvとcontroller_core.smvを比較します．記録変数ありのモデルで初期状態に戻るまでの組を考え，状態数を確認します．この削除で保てることと，確認できなくなることを説明してください．
解答例と解説
上限は16から4，到達可能な状態数は12から3です．制御器は3段階，記録値は4段階の周期なので，両方が初期値に戻るのは12回後です．
今回の安全性と応答は両方真で，phaseだけを見た経路も同じです．log_tickを削除しても残りの更新条件が変わらないからです．ただし，記録値自体や記録タイミングに関する要求は，削除したモデルでは検証できません．
自己確認： 変数を「性質に名前が出ていないから」だけで削除せず，遷移にも影響しないことを確認します．
演習5：抽象モデルの反例を吟味する【確認】¶
data_concrete.smvとdata_abstract.smvを実行します．2つの性質の結果を比較し，抽象モデルの活性の反例が具体モデルで実行できるか考えます．
解答例と解説
具体モデルの2式は真，抽象モデルでは0を保つ性質は真，いつか0になる性質は偽です．状態数は4から2に減っています．
抽象モデルの反例はpositiveに留まる無限の経路です．具体モデルは3から始まり，3回の遷移で0になります．無限に正の値に留まることはできないため，この反例は元のモデルのバグではありません．
自己確認： 減少の回数を区別する情報を落としたことが原因だと説明します．活性を確認するためなら，具体値を戻す，残り段階を区別するなど，完了までの進行を表す情報が必要です．根拠なく公平性を付けて反例を消すことは，元のモデルとの対応の説明にはなりません．
演習6：比較結果を自分で評価する【発展・任意】¶
今回の比較から1組を選び，同じ手順で状態数とprint_fsm_statsの情報を確認します．実行時間も観察する場合は条件をそろえます．次の4点をまとめて説明してください．
- 何を変更したか．
- 上限と到達可能な状態数がそれぞれどう変わったか．
- 性質の結果と，その結果を比較できる根拠．
- 性能について言えることと，この小さな例だけでは言えないこと．
解答例と解説
例えば記録変数を除く比較では，制御器に影響しないカウンターを削除し，上限16から4，到達数12から3になります．残した状態の経路が同じなので，今回の安全性と応答を同じ意味で比較できます．
到達数が減ったことは確認できますが，必ず実行時間が4分の1になるとは言えません．BDDの表現，前処理，起動，測定のばらつきなども影響します．特定のBDDノード数や時間の一致を正解の条件にはしません．
自己確認： 状態数，BDDノード数，時間を別の指標として説明できれば，今回の目的を達成しています．
5.10 よくある誤りと振り返り¶
| 状況 | 見直すこと |
|---|---|
| 上限と到達数が違う | 初期状態と遷移をたどり，型の全値に到達するか調べる |
| DEFINEに変えたらタイミングが変わる | 元の変数が現在値から導けるのか，履歴を記憶していたかを確認する |
| 値域を狭めたら構文・範囲のエラー | 初期値と遷移先が新しい型に収まるか確認する |
| 小さくしたら活性が偽になる | 余分な経路を許したか，必要な進行情報を落としたか調べる |
| 性質を真にするために制約を加えた | 元のモデルの反例を根拠なく除外していないか確認する |
| 状態数が減っても速くならない | BDDの表現や測定条件を区別し，状態数だけで時間を予想しない |
- 状態変数の値域の積を計算できる（5.2節・演習1）．
- 出力の到達数と総数を読み分けられる（5.3節・演習2）．
- 値域や導出値の変更で，到達数が変わらない理由を説明できる（5.4〜5.5節・演習2〜3）．
- 削除してよい変数を，性質と遷移の依存関係から考えられる（5.6節・演習4）．
- 抽象モデルの反例を具体モデルと照合できる（5.7節・演習5）．
- 状態数の削減と，検証表現・処理の効率化を区別できる（5.8節・演習6）．
最後に，比較した2モデルについて，結果の表だけでなく「なぜその変更で，どの振る舞いと性質を保てるか」を解説を閉じて説明します．説明できない箇所を復習してください．
第6回では，有界モデル検査（BMC）で探索の上限を指定し，反例が見つかった場合と見つからなかった場合の意味を学びます．
参考資料¶
- nuXmv公式ドキュメント：使用バージョンのマニュアルのDEFINE，BDD関連コマンド，到達可能性の表示を参照します．
- 使用中のnuXmvでは，
help -p print_reachable_states，help -p print_fsm_stats，help -p dynamic_var_orderingで詳細を確認できます．