第1回：モデル検査を体験する

今回は，nuXmvを導入し，用意された小さな制御器のモデルを使って検証を体験します．

ここでの検証は，nuXmvのバッチ実行によって行います．バッチ実行では，モデルと検証したい性質を記述した.smvファイルを指定してプログラムを起動することで，読み込み，モデルの構築，性質の検証，結果の表示といった一連の処理を自動で行います．もう1つの実行方法であるインタラクティブ実行による対話的な検証は，第4回で詳しく扱います．

正常なモデルとバグのあるモデルを比較し，性質の違反に至る反例を読みます．SMV言語の文法をすべて覚える必要はありません．モデルの本格的な記述は第2回で扱います．

1.1 到達目標と授業の進め方

終了時に，次のことができれば今回の目標を達成しています．

• 状態・遷移・初期状態・実行経路を例で説明できる．
• PowerShellまたはTerminalからnuXmvを起動できる．
• .smvファイルを指定してバッチ実行できる．
• 検証結果のtrue・falseと，実行エラーを区別できる．
• 反例を状態遷移の列として読み，最初の違反を指摘できる．

内容	目安
状態遷移とモデル検査の考え方	15分
nuXmvの導入・起動確認	25〜35分
モデルの準備とバッチ実行	20分
反例の読み方	10分
演習と振り返り	20〜30分

必要なものは，WindowsまたはmacOSのPC，インターネット接続，テキストエディターです．Windowsの手順はPowerShell，macOSの手順はTerminalで行います．

途中で困った場合

コマンド，出力されたエラー，現在の作業フォルダーを記録してから，ページ後半の「トラブルシューティング」を確認してください．

1.2 状態と状態遷移を考える

状態は「今の変数の値」

システムの状態は，モデルで使う状態変数の値の組です．今回はphaseという変数を1つ使い，次の4つの値を取れることにします．

phaseの値	意味
idle	待機中
busy	処理中
done	応答する段階
error	異常状態

このモデルでは変数が1つだけなので，phase = idleが1つの状態を表します．変数が2つ以上なら，その組み合わせが状態になります．

初期状態と遷移

最初の状態を初期状態と呼びます．今回はidleから始めます．正常な制御器は，次の図のように動きます．

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

矢印は1回の遷移を表します．errorも取り得る値として定義されていますが，正常なモデルでは初期状態からerrorに進む矢印がありません．

今回の簡略化

今回は，待機状態で毎回要求が到着し，処理も1段階で完了するものとします．外部入力や処理時間は表現していません．矢印1つが現実の1秒を表すわけでもありません．環境入力は第4回で追加します．

実行経路

遷移をたどって得られる状態の列を実行経路と呼びます．正常なモデルは，次のように繰り返します．

idle → busy → done → idle → busy → done → …

初期状態から遷移をたどって行ける状態を到達可能な状態と呼びます．この例ではidle，busy，doneが到達可能です．errorは取り得る値ですが，到達できません．

確認：2回遷移した後の状態は？

初期状態を遷移回数0とすると，1回後はbusy，2回後はdoneです．状態を数える場合と遷移を数える場合を区別しましょう．

1.3 シミュレーションとモデル検査

シミュレーションでは，ある実行をたどって振る舞いを観察します．複数の選択肢があるモデルでは，観察した経路以外の経路もあり得ます．

モデル検査では，モデルに対して検証したい性質を与えます．今回の性質は，次のものです．

初期状態からどのように動いても，異常状態に入らない．

nuXmvはこの性質がモデルで成立するかを調べます．成立しない場合には，異常状態に至る具体的な経路が反例として表示されます．

要素	今回の例
モデル	idle → busy → done → idleという振る舞い
性質	異常状態に入らない
結果	性質が成立するか，反例があるか

検証する対象はモデルです

検証結果は，モデルに記述した振る舞いについての結果です．モデルに含めていない故障や入力について，実システムの安全性を保証するものではありません．

1.4 nuXmvを導入する

使用するバージョン

本教材では nuXmv 2.1.0 を使用します．公式の旧バージョン配布ページから取得してください．Windowsはx86_64版，macOSは64-bit universal版を選びます．

2026年10月8日時点で，最新バージョンの配布ページには2.2.0のWindows版が「coming soon」と掲載されているため，両OSに配布のある2.1.0を基準にします．

利用条件

nuXmvの公式配布ページでは，非商用または学術目的での利用とされています．取得時に公式の利用条件を確認してください．

配布物を展開する

=== "Windows（PowerShell）"

1. 公式配布ページの**Version 2.1.0 → Windows → x86_64**を選びます．
2. `nuXmv-2.1.0-win64.7z`を保存します．
3. `.7z`を扱える展開機能で展開します．Windowsの展開機能で扱えない場合は，[7-Zipの公式サイト](https://www.7-zip.org/)から導入した7-Zipを利用します．大学の管理PCでは担当者の案内に従ってください．
4. 展開したフォルダーを開き，`bin`内の`nuXmv.exe`を探します．
5. 配布物全体を保存しておきます．実行ファイルだけを移動する必要はありません．

エクスプローラーで拡張子を表示してください．Windows 11では「表示 → 表示 → ファイル名拡張子」，Windows 10では「表示 → ファイル名拡張子」が目安です．操作名が違う場合は，エクスプローラーの設定から拡張子の表示を探します．

**確認：** 実行ファイルの実際の場所を確認できたら次へ進みます．Windows版はx86_64向けです．ARM版Windowsを使う場合は，授業前に実行できるか担当者と確認してください．

=== "macOS（Terminal）"

1. 公式配布ページの**Version 2.1.0 → Mac OS → 64-bit universal binary**を選びます．
2. `nuXmv-2.1.0-macos-universal.tar.xz`を保存します．
3. Terminalを開き，次のコマンドで展開します．保存先がDownloads以外の場合はパスを変更します．

```bash
cd "$HOME/Downloads"
tar -xf nuXmv-2.1.0-macos-universal.tar.xz
```

展開先の`nuXmv-2.1.0-macos-universal/bin/nuXmv`を確認します．配布物全体を保存しておきます．

**確認：** 実行ファイルの実際の場所を確認できたら次へ進みます．macOSが実行を止める場合の対応は，後半のトラブルシューティングにあります．

作業フォルダーを作る

実行ファイルの場所と，演習用ファイルを保存する場所は別でも構いません．演習ではホームフォルダーの下にnuxmv-tutorial/lesson01を作ります．

=== "Windows（PowerShell）"

スタートメニューで「PowerShell」を検索して開き，次を実行します．

```powershell
New-Item -ItemType Directory -Force -Path "$HOME\nuxmv-tutorial\lesson01"
Set-Location "$HOME\nuxmv-tutorial\lesson01"
Get-Location
```

最後のコマンドで，現在の場所が`lesson01`で終わることを確認します．

=== "macOS（Terminal）"

Terminalで次を実行します．

```bash
mkdir -p "$HOME/nuxmv-tutorial/lesson01"
cd "$HOME/nuxmv-tutorial/lesson01"
pwd
```

最後のコマンドで，現在の場所が`lesson01`で終わることを確認します．

コマンドは1行ずつ実行します

コピーした後，Enterを押して実行します．PS C:\…>や%など，入力待ちを示すプロンプトはコピーしません．以降の実行用コードにはプロンプトを含めていません．

実行ファイルの場所を設定する

長いパスを毎回入力しなくてよいよう，今開いているシェルの変数nuxmvExeに実行ファイルの場所を入れます．ここでの変数はSMVモデルの変数とは別です．

=== "Windows（PowerShell）"

次の例はDownloads直下に配布フォルダーを展開した場合です．**展開先が違う場合やフォルダーが二重になっている場合は，実際の場所に書き換えてください．**

```powershell
$nuxmvExe = "$HOME\Downloads\nuXmv-2.1.0-win64\bin\nuXmv.exe"
Test-Path $nuxmvExe
```

`True`ならファイルが存在します．`False`なら先にパスを修正します．エクスプローラーで実行ファイルを右クリックして「パスのコピー」を選び，`$nuxmvExe = `に続けて貼り付けても構いません．コピーしたパスには引用符`"`が付いているので，自分で引用符を追加しないでください．

```powershell
$nuxmvExe = "C:\実際の展開先\bin\nuXmv.exe"
```

この2つ目の例は，貼り付けた後の形を示したものです．「実際の展開先」の部分が自分の場所になります．

=== "macOS（Terminal）"

```bash
nuxmvExe="$HOME/Downloads/nuXmv-2.1.0-macos-universal/bin/nuXmv"
ls -l "$nuxmvExe"
```

実行ファイルの情報が表示されることを確認します．`No such file or directory`なら，実際の展開先に合わせてパスを修正します．

起動してバージョンを確認する

=== "Windows（PowerShell）"

```powershell
& $nuxmvExe -int
```

`&`は，変数に入っているパスのプログラムを実行するための記号です．

=== "macOS（Terminal）"

```bash
"$nuxmvExe" -int
```

起動時の表示でnuXmv 2.1.0を確認します．説明文や著作権表示に続いて，nuXmv >という入力待ちが表示されます．ここでは動作確認だけを行うので，nuXmvのプロンプトに次を入力して終了してください．

quit

確認： OSのシェルに戻れば起動確認は完了です．対話的な検証の操作は第4回で詳しく扱います．

新しいシェルを開いた場合

nuxmvExeの設定は，そのシェルを閉じると失われます．新しいPowerShellやTerminalを開いたら，作業フォルダーへ移動し，実行ファイルの場所を再設定してください．

任意：このシェルだけPATHに追加する

今回はnuxmvExeを使えば十分です．PATHは，プログラム名から実行ファイルを探す場所の一覧です．このシェルだけに追加する場合は次を使います．シェルを閉じると元に戻ります．

=== "Windows（PowerShell）"

```powershell
$env:Path = "$(Split-Path -Parent $nuxmvExe);$env:Path"
nuXmv.exe -int
```

=== "macOS（Terminal）"

```bash
export PATH="$(dirname "$nuxmvExe"):$PATH"
nuXmv -int
```

起動したらquitで終了します．教材の後続コマンドは引き続きnuxmvExeを使います．

1.5 最初のSMVファイルを準備する

演習ファイルを取得する

次のリンクから2つのSMVファイルと演習メモを保存し，先ほど作ったlesson01フォルダーに置いてください．演習メモは任意です．ブラウザーが内容を表示する場合は，リンクを右クリックして「リンク先を保存」を選びます．

• 正常な制御器：controller_ok.smv
• バグのある制御器：controller_bug.smv
• 演習メモ（任意）

最初のファイルは，以下の内容をコピーして作成しても構いません．

controller_ok.smv

-- Lesson 01: a controller that never enters error.
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;

エディターで保存する

プレーンテキストを編集できるエディターを使います．Wordなどで文書ファイルとして保存しないでください．

=== "Windows（PowerShell）"

メモ帳を使う場合は，コードを貼り付けて「名前を付けて保存」します．

- 保存先：ホームフォルダー内の`nuxmv-tutorial\lesson01`
- ファイル名：`controller_ok.smv`
- ファイルの種類：すべてのファイル
- 文字コード：UTF-8（「UTF-8（BOM付き）」は選ばない）

BOM付きで保存すると，ファイル先頭に見えない文字が入り，構文エラーの原因になることがあります．保存後に拡張子を確認し，`controller_ok.smv.txt`になっていないことを確かめます．

=== "macOS（Terminal）"

テキストエディットを使う場合は，「フォーマット → 標準テキストにする」を選びます．また，テキストエディットの設定で「スマート引用符」と「スマートダッシュ」をオフにしてください．スマートダッシュが有効だと，コメントの`--`が`—`に変わり，構文エラーになります．

- 保存先：ホームフォルダー内の`nuxmv-tutorial/lesson01`
- ファイル名：`controller_ok.smv`
- 文字コード：UTF-8

`.txt`を自動追加する設定がある場合は外します．Finderの「情報を見る」でも実際の名前と拡張子を確認できます．コード用エディターを使っても構いません．

ファイルを確認する

=== "Windows（PowerShell）"

```powershell
Get-ChildItem *.smv
Get-Content .\controller_ok.smv
```

=== "macOS（Terminal）"

```bash
ls *.smv
cat controller_ok.smv
```

確認： ファイル名が表示され，内容が上のコードと一致していることを確認します．

コードの見どころ

記述	今回の役割
MODULE main	モデルの入口
VAR	状態変数の宣言
phase : {idle, busy, done, error};	4つの値を取る変数
init(phase) := idle;	初期状態はidle
next(phase) := case ... esac;	現在の状態に応じて次状態を決める
phase = busy : done;	処理中なら次は応答段階
TRUE : phase;	上の条件に当てはまらない場合は現在値を保つ
INVARSPEC phase != error;	到達可能なすべての状態で異常状態ではないことを検証

!=は「等しくない」を表します．INVARSPECはモデルを制限する命令ではなく，モデルについて確かめたい性質です．

1.6 バッチ実行して結果を読む

正常なモデルを実行する

バッチ実行なので，-intは付けません．

=== "Windows（PowerShell）"

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

=== "macOS（Terminal）"

```bash
"$nuxmvExe" controller_ok.smv
```

期待される検証結果の主要部分は次です．起動時の説明文は省略しています．

-- invariant phase != error is true

これは「初期状態から到達可能なすべての状態でphase != errorが成立する」という結果です．errorは型の値には含まれますが，到達できないので性質は成立します．

バグのあるモデルを実行する

controller_bug.smvでは，次の1行が変更されています．

phase = busy : error;

実行前に，どの順番で状態が変わり，性質の結果がどうなるかを予想してください．その後，実行します．

=== "Windows（PowerShell）"

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

=== "macOS（Terminal）"

```bash
"$nuxmvExe" controller_bug.smv
```

期待される検証結果の主要部分は次のとおりです．nuXmvのバージョンや設定によって，表記が多少異なることがあります．

-- invariant phase != error is false
-- as demonstrated by the following execution sequence
Trace Description: AG alpha Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    phase = idle
  -> State: 1.2 <-
    phase = busy
  -> State: 1.3 <-
    phase = error

まずis falseと，idle → busy → errorという状態の列を確認してください．Trace DescriptionのAG alphaはツール側の説明で，今回覚える必要はありません．

3つの結果を区別する

表示・状況	意味	次にすること
is true	検証した性質がモデルで成立した	どの性質が成立したかを確かめ，ほかに検証すべき性質を検討する
is falseと反例	性質に違反する実行がある	反例と遷移を照合し，違反の要因を特定する
構文エラー，ファイルを開けない，起動できない	検証を正常に完了していない	モデルや実行環境を修正する

falseはnuXmvの故障ではありません

バグのあるモデルでfalseが出ることは，意図した検証結果です．一方，エラーで止まった場合は，性質の真偽を判断できたことにはなりません．

出力を保存する（任意）

結果をファイルに残したい場合は次を使います．画面にも表示しながらファイルに保存します．同じ名前の記録ファイルがある場合は上書きされます．

=== "Windows（PowerShell）"

```powershell
& $nuxmvExe .\controller_bug.smv 2>&1 | ForEach-Object { "$_" } | Tee-Object -FilePath .\controller_bug-output.txt
```

`ForEach-Object { "$_" }`は，Windows PowerShell 5.1で起動時の説明文がエラー表示として記録されないようにするためのものです．

=== "macOS（Terminal）"

```bash
"$nuxmvExe" controller_bug.smv 2>&1 | tee controller_bug-output.txt
```

1.7 反例を状態遷移図と対応させる

反例は，性質を満たさない具体的な実行の例です．今回の反例を表にすると次のようになります．

状態番号	遷移回数	phase	phase != error
1.1	0	idle	真（成立）
1.2	1	busy	真（成立）
1.3	2	error	偽（不成立）

1.1の左側の1はトレース番号，右側の1はそのトレース内での順番です．初期状態の状態番号は1.1ですが，遷移回数は0です．

flowchart LR
    A["1.1: idle"] --> B["1.2: busy"]
    B -->|バグのある遷移| C["1.3: error"]
    style C fill:#ffebee,stroke:#b71c1c,color:#111

読み方は次の順序です．

1. 最初の状態が，モデルに指定した初期状態と一致するか確認する．
2. 隣り合う状態の間で，どの遷移規則が使われたか調べる．
3. 検証した性質が初めて不成立になる状態を探す．
4. その直前の遷移が，自然言語で説明した動作に合っているか考える．

今回，最初に違反するのは1.3です．直前のbusy → errorは「処理が完了したら応答する」という意図に合いません．

直前の状態から値が変わらない変数は表示されません

標準のトレース表示では，前の状態から値が変わらない変数を省略します．複数変数のモデルを読む際は，表示がない変数も直前の値を使って状態を復元してください．初期状態には最初の値が表示されます．

1.8 演習

解答例と解説は折りたたまれています．

演習の進め方

1. 解答を開く前に結果を予想し，その理由を短く書きます．
2. 実行して，出力と予想を比較します．
3. 解答例と解説を開き，違いがあれば「遷移の読み違い」「性質の意味」「操作・保存」のどこで違ったかを探します．
4. 該当する説明に戻ってから，解答を閉じて理由を説明し直します．

演習1：予想と実行を比較する【基本】

1. controller_ok.smvとcontroller_bug.smvについて，初期状態からの3回の遷移を書き下します．
2. それぞれの性質の結果を予想します．
3. 両方を実行し，予想と結果を比較します．
4. 結果が違った場合は，どの遷移の読み方を間違えたか説明します．
5. 両モデルが初めて異なる状態になるのは，何回目の遷移かを説明します．

ヒント

next(phase)のcaseは，現在のphaseに対応する行を使います．errorの場合は最後のTRUE : phase;で値が変わりません．

解答例と解説

正常なモデルはidle → busy → done → idleです．異常状態に到達しないためtrueです．

バグのあるモデルはidle → busy → error → errorです．2回の遷移後に異常状態に入るためfalseです．反例は異常状態に初めて入るところまでを示します．

遷移回数	正常なモデル	バグのあるモデル
0	idle	idle
1	busy	busy
2	done	error
3	idle	error

なぜこの結果になるか： 現在値がidleなら，両モデルとも次はbusyです．現在値がbusyになった次の遷移（2回目）で，正常モデルはdone，バグモデルはerrorを選びます．バグモデルのerrorでは先の3条件が成立しないため，TRUE : phase;が選ばれてerrorに留まります．正常モデルは3状態の周期を繰り返すので，その先も異常状態に入りません．

間違えやすい点： caseの各行を上から順に実行して，1回の遷移でidle → busy → doneと進むわけではありません．1回の遷移では，現在値に基づいて次の値を1つ決めます．また，反例が3状態で終わるのは，モデルの実行そのものが終了したからではありません．違反までの経路を示すには十分だからです．理由を説明できない場合は，1.5節の「コードの見どころ」で現在値と次の値の対応を見直してください．

演習2：反例を表にする【基本】

controller_bug.smvの出力を使い，次の項目をまとめてください．

• 状態番号
• 遷移回数（初期状態を0とする）
• 各状態のphase
• 各状態で性質が成立するか
• 最初に違反する状態と，その直前の遷移

解答例と解説

状態番号	遷移回数	phase	phase != error
1.1	0	idle	真（成立）
1.2	1	busy	真（成立）
1.3	2	error	偽（不成立）

最初の違反は状態1.3，遷移回数2のphase = errorです．直前の遷移はbusy → errorであり，phase = busy : error;が原因です．

性質の評価： idle != errorとbusy != errorは真です．error != errorは偽です．反例中のすべての状態が違反しているのではなく，今回は最後の状態で初めて違反します．

間違えやすい点： 状態1.3を「3回遷移した後」と読むと，1回ずれます．初期状態も表示上の状態数に含まれるため，3状態の反例には2本の遷移があります．取り違えた場合は，1.7節で初期状態を遷移回数0として数え直します．

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

1. controller_bug.smvをコピーし，controller_fixed.smvという名前にします．
2. 「処理中から応答する段階へ進む」という意図に合うよう，1行修正します．
3. 検証する性質は変更せず，保存します．
4. 実行前に結果を予想します．
5. 次のコマンドで再検証し，予想どおりの結果になるかを確かめます．

=== "Windows（PowerShell）"

コピーする場合：

```powershell
Copy-Item .\controller_bug.smv .\controller_fixed.smv
```

エディターで修正・保存した後：

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

=== "macOS（Terminal）"

コピーする場合：

```bash
cp controller_bug.smv controller_fixed.smv
```

エディターで修正・保存した後：

```bash
"$nuxmvExe" controller_fixed.smv
```

ヒント

INVARSPECを消したり，常に成立する式に変えたりすると，元の要求を検証できなくなります．busyの次に進む状態を直しましょう．

解答例と解説

phase = busy : error;をphase = busy : done;に変更します．保存して再実行すると-- invariant phase != error is trueになります．

修正後の全体は次です．自分のファイルと比較してください．

controller_fixed.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;

なぜ修正できたと言えるか： 修正後はidle → busy → done → idleと繰り返します．意図した「処理中から応答段階へ進む」遷移が復元され，異常状態への経路もなくなります．

不十分な修正の例： 性質を削除すると，確認したい要求を検証できません．INVARSPEC TRUE;に変えると，異常状態に入るモデルでも真になります．busy → busyに変えても今回の性質は真ですが，応答しなくなるため，元の動作の修正としては不十分です．演習5でこの違いを確認します．

検証したい要求は「異常状態に入らない」のままなので，性質を変更せず，意図と違った遷移を修正します．ただし，この1つの性質の成立だけでは応答に関するすべての要求を確認したことにはなりません．

結果がfalseのままなら，保存したか，実行したファイル名が正しいかを見直します．構文エラーが出た場合は1.9節を参照してください．

確認問題：結果を言葉で説明する

1. errorを型の値に含めているのに，正常なモデルで性質がtrueになるのはなぜですか．
2. シミュレーションで1つの経路に異常がなかった場合と，今回の不変条件のモデル検査でtrueだった場合は，何が違いますか．
3. 今回の結果がtrueなら，現実の制御器が故障しないと言えますか．

解答例と解説

1. 型は取り得る値を定めますが，到達可能性は初期状態と遷移で決まります．正常なモデルには初期状態からerrorへ至る経路がありません．
2. 1つの経路を観察しただけでは，ほかの経路の違反を除外できません．今回のモデル検査は，モデルのすべての到達可能な状態について不変条件を確認します．今回の正常な例は経路が1つですが，選択肢のあるモデルではこの違いが重要です．
3. 言えません．今回のモデルには現実の故障や外部入力の詳細を含めていません．結果は記述したモデルと性質の範囲についてのものです．

回答の観点： 解答例と同じ文章である必要はありません．次の内容を説明できていれば十分です．

問い	回答に含めたい説明	不十分な説明と見直し方
1	型の値と到達可能な状態は異なり，初期状態と遷移が到達可能性を決める	「errorを使っていないから」だけでは不十分です．初期状態からの矢印をたどって確認します
2	観察した1経路と，モデルのすべての到達可能な状態についての検証の違い	「何回も実行するから」ではありません．1.3節に戻り，検証の対象範囲を確認します
3	モデルに含めた振る舞いと，今回検証した性質の範囲に限る	「nuXmvが真と言ったから安全」と広げないよう，含めていない入力や故障を1例挙げます

演習4：初期状態を変える【発展・任意】

正常なモデルをcontroller_initial_error.smvとしてコピーし，init(phase) := error;に変更します．結果と反例の状態数を予想してから，同じ方法で実行してください．

解答例と解説

初期状態ですでに性質に違反するためfalseです．反例には初期状態のphase = errorが表示され，違反までの遷移回数は0です．性質は遷移後の状態だけでなく，初期状態についても調べます．

出力の主要部分は次です．空白や説明文が異なっても，真偽と状態の値を比較してください．

-- invariant phase != error is false
-- as demonstrated by the following execution sequence
Trace Description: AG alpha Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    phase = error

なぜ1状態で十分か： 性質に違反するまでの遷移を探す必要がありません．開始した時点でerror != errorは偽です．反例が1状態でも，モデルが遷移できないという意味ではありません．このモデルはTRUE : phase;によってerrorに留まります．

演習5：真でも応答しないモデル【発展・任意】

正常なモデルをcontroller_stuck.smvとしてコピーし，phase = busy : done;をphase = busy : busy;に変えます．実行経路と今回の性質の結果を予想し，実行して確認してください．応答できるかも考えます．最後に，この問題を見つけるために追加したい要求を自然言語で書いてください．時相論理の式はまだ書けなくても構いません．

解答例と解説

経路はidle → busy → busy → …です．errorには到達しないので，今回の性質はtrueです．しかしdoneに進まず，応答しません．「異常状態に入らない」と「いつか応答する」は別の性質です．応答に関する活性の記述は第3回で学びます．

観点	正常なモデル	処理中に留まるモデル
到達可能な状態	idle，busy，done	idle，busy
phase != error	成立	成立
応答段階doneに進むか	進む	進まない

なぜ検出されないか： 今回の式はerrorへの到達を調べるだけで，doneへの進行を要求していません．ツールは与えられた性質を正しく検証しています．応答しない問題を調べるには，応答に関する別の性質が必要です．追加したい要求の例は「処理中になったら，いつか応答段階に進む」です．

1.9 トラブルシューティング

実行ファイルが見つからない

WindowsではTest-Path $nuxmvExe，macOSではls -l "$nuxmvExe"でパスを確認します．展開してできたフォルダーが二重になっていないか，実行ファイルがbin内にあるかを確認してください．新しく開いたシェルでは変数の再設定も必要です．

入力ファイルが見つからない

現在の作業フォルダーを確認します．

=== "Windows（PowerShell）"

```powershell
Get-Location
Get-ChildItem
```

=== "macOS（Terminal）"

```bash
pwd
ls
```

lesson01にいない場合は1.4節のコマンドで移動します．ファイルがDownloadsに残っている場合は，作業フォルダーへ移動してください．

ファイル名が.smv.txtになっている

エクスプローラーまたはFinderで実際の拡張子を確認し，末尾の.txtを取り除きます．ファイルの中身がプレーンテキストであることも確認します．

パスに空白がある

パス全体を引用符で囲みます．例えば入力ファイルを絶対パスで指定する場合は次のようにします．

=== "Windows（PowerShell）"

```powershell
& $nuxmvExe "$HOME\nuxmv tutorial\controller_ok.smv"
```

=== "macOS（Terminal）"

```bash
"$nuxmvExe" "$HOME/nuxmv tutorial/controller_ok.smv"
```

これは引用符の例です．実際にその場所へファイルを保存していない場合は実行できません．

Windowsで実行が保護機能に止められる

公式サイトから取得した配布物か確認します．警告が出た場合は内容を記録し，大学の管理PCでは担当者に確認してください．OSの保護機能全体を無効にする必要はありません．

macOSで実行が止められる

公式サイトから取得したファイルであることを確認し，一度起動を試した後，「システム設定 → プライバシーとセキュリティ」で該当する実行の許可が案内されているか確認します．利用しているmacOSの手順に従ってください．詳しくはAppleのアプリを安全に開くための説明を参照します．

Permission deniedと表示され，実行権限がない場合に限り，確認済みの実行ファイルに権限を付けて再実行します．

chmod u+x "$nuxmvExe"
"$nuxmvExe" -int

構文エラーが出る

表示された行番号付近を確認し，教材のコードと比較します．

• セミコロン;，コロン:，:=が抜けていないか．
• caseに対応するesac;があるか．
• 全角の記号や，エディターが自動変換した文字を使っていないか．
• idle・busy・done・errorの綴りが一致しているか．
• コードブロックの囲み記号や，説明文までコピーしていないか．

修正したのに結果が変わらない

エディターで保存したか，実行したファイル名が合っているかを確認します．Get-Contentまたはcatで実際に実行するファイルの内容を見ると確実です．

nuXmv >のままOSのコマンドを入力してしまった

nuXmvのプロンプトにquitを入力してOSのシェルに戻ります．Get-LocationやcdなどはOSのシェルで実行します．

1.10 振り返り

この教材では成果物の提出を求めません．作成したモデルや出力は，予想と結果を比べて理解を深めるために使います．

次の各項目を，解説を見ずに説明できるか振り返ります．説明できない項目は，括弧内の節や演習で復習してください．

• [ ] 型にerrorがあっても到達しない理由を，初期状態と遷移から説明できる（1.2節・確認問題1）．
• [ ] 検証結果のfalseと構文エラーの違いを説明できる（1.6節・1.9節）．
• [ ] 3状態の反例に遷移が2回しかない理由を，状態番号と遷移回数を区別して説明できる（1.7節・演習2）．
• [ ] 違反に至る遷移をコードの行で特定し，性質を変えずに修正できる（演習3）．
• [ ] 1つの性質がtrueでも，すべての要求を満たすとは限らないことを例で説明できる（演習5・確認問題3）．

最後に通して説明する

バグのあるモデルをもう一度開き，実行せずに「初期状態」「違反までの経路」「原因の行」「修正方法」を順に説明します．その後に実行し，説明と出力を照らし合わせてください．途中で解説が必要だった箇所が，次に復習する箇所です．

第2回では，今回使ったinit・next・caseの意味を詳しく学び，状態遷移図から自分でSMVモデルを書きます．

参考資料

• nuXmv公式ドキュメント：マニュアルと基礎チュートリアル．
• nuXmv 2.1.0の公式配布ページ：本教材で使う配布物．
• nuXmvの現在の配布状況：使用するバージョンを変更する場合の確認先．

配布物に含まれる，使用するバージョンと一致するマニュアルを優先して参照してください．