* Interactive mode とは [#f1c53d5e]
- 通常の処理系Hyroseは, 入力に対してそのシミュレーションの結果を返すのみである
- Interactive modeでは, シミュレーションの様子を見ながら対話的に実行をおこなう
-- モデルの理解を促進
-- モデルに操作を加えることが可能
-- デバッグ等に有用
* 利用法 [#l5c4ae5d]
- シミュレーション開始時にオプション"--in"でInteractive modeを有効にする
- <ENTER>を押す毎に1フェイズずつ実行を進める
- 離散変化を行うPointPhase(PP)と, 連続変化の計算を行うIntervalPhase(IP)のそれぞれで入力を受け付ける
- 各時点でコマンドを入力し, それぞれの機能を有効にする
>
b [arg] : Break Point
ブレークポイントを設定する
<
>
c [arg] : Change
変数値の変更を行う
<
>
fu : Find unsat core
デバッグ情報としてのunsat coreを導出する
<
>
j [arg] : Jump
特定のフェイズにジャンプする
<
>
p : Print
現在の状態をプリントする
<
>
q : Quit
シミュレーションを終了する
<
>
r : Run
設定したブレークポイントまでシミュレーションを進める
<
* Unsat Core [#d7071a1f]
- ある充足不可能となる制約集合の部分集合で, 極小矛盾集合のこと
- 次の条件を満たすψをUnsat Coreという
φ : 充足不可能となる制約集合
1. φ = ψ ^ ψ'
2. ψは充足不可能
3. ψ中の各制約{c}についてψ\{c}は充足可能
