# 第1回 演習メモ（任意）

提出は不要です．予想と結果，理解したことを書き留めるために使います．

- OS：
- nuXmvのバージョン：

## 演習1：予想と実行

| ファイル | 3回の遷移（予想） | 実行前の予想 | 実行結果 | 理由 |
| --- | --- | --- | --- | --- |
| controller_ok.smv | | | | |
| controller_bug.smv | | | | |

両モデルが初めて異なる状態になる遷移：

## 演習2：反例

| 状態番号 | 遷移回数 | phase | 性質を満たすか |
| --- | --- | --- | --- |
| | | | |
| | | | |
| | | | |

最初に違反する状態と，その直前の遷移：

## 演習3：修正

- 修正した行（変更前・変更後）：
- 実行前の予想：
- 実行結果：
- 性質を変えずに修正した理由：

## 確認問題

1. errorを型の値に含めても性質がtrueになる理由：
2. シミュレーションとモデル検査の違い：
3. trueという結果から言えることと言えないこと：

## 発展演習（任意）

- 変更内容：
- 実行前の予想：
- 観察と説明：
- 演習5で追加したい要求：

## 振り返り

- 予想と結果が違った点と，その原因（遷移の読み方／性質の意味／操作・保存）：
- 解説を見ずに説明できなかったこと：
- 疑問・困ったこと：