- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* Interactive mode とは [#f1c53d5e]
- 通常の処理系Hyroseは, 入力に対してそのシミュレーションの結果を返すのみである
- Interactive modeでは, シミュレーションの様子を見ながら対話的に実行をおこなう
-- モデルの理解を促進
-- モデルに操作を加えることが可能
-- デバッグ等に有用
* 利用法 [#l5c4ae5d]
- シミュレーション開始時にオプション"--in"でInteractive modeを有効にする
- <ENTER>を押す毎に1フェイズずつ実行を進める("j 1"とおなじ動作を行う)
- 離散変化を行うPointPhase(PP)と, 連続変化の計算を行うIntervalPhase(IP)のそれぞれで入力を受け付ける
- 各時点でコマンドを入力し, それぞれの機能を有効にする
>
h : Help
Helpを表示する
<
>
j [arg] : Jump
現在の状況から, 与えられた数のフェイズだけジャンプする
positive number : forward (通常のシミュレーションと同じ)
negative number : backward
<
>
q : Quit this simulation
現在のシミュレーションを終了する
<
>
c : Change a value of a variable
変数値の変更を行う
<
>
p : Display the information of the current phase
現在の状態をプリントする
<
>
a : approx a value of a variable as interval
変数の値を区間値に変更して近似する
<
>
u : Find unsat core constraints and paint them
デバッグ情報としてのunsat coreを導出する
<
>
breakpoints : Making program stop at certain points
ブレークポイントを設定する
<
>
run : simulate program until the breakpoint is reached
設定したブレークポイントまでシミュレーションを進める
<
>
s : Save state to file
現在のシミュレーション状況をファイルに保存する
<
* Unsat Core [#q743138b]
- インタラクティブモードでは, unsat coreを利用した柔軟なシミュレーションを容易に行うことができる
- また, インタラクティブモードでなくてもunsat core利用したシミュレーションは可能である
** Unsat Coreとは [#d7071a1f]
- ある充足不可能となる制約集合の部分集合で, 極小矛盾集合のこと
- 次の条件を満たすψをUnsat Coreという
φ : 充足不可能となる制約集合
1. φ = ψ ^ ψ'
2. ψは充足不可能
3. ψ中の各制約{c}についてψ\{c}は充足可能
** HydLaにおけるバグ [#paac1e9a]
- Hyroseでは各時刻において変数が満たすべき制約を求める
- 制約には優先順位をつけることができる
- HydLaプログラムの制約に関して, 望んだ動作でない場合がある
-- 満たすべき制約集合が充足不可能となる
-- 採用されてほしい制約が採用されない
** Unsat Coreを用いたバグの特定 [#x0fc019b]
- シミュレーション中に意図しない動作が現れた時点で解析を行う
- unsat coreがバグの原因の場合, 問題となるプログラムの修正が容易になる
>
~ INIT <=> y＝9 & y'=0.
~ FALL <=> [](y''=-10).
~ BOUNCE <=> [](y-=0 => y'=-(4/5)*y'-).
~ INIT, FALL, BOUNCE.
<
-採用されている制約(c)
>
~ PP1
~ c1 : t=0
~ c2 : y=9
~ c3 : y'=0
~ c4 : y''=-10
~ IP2
~ c1 : t=(0, 3*5^( ( -1 )/2))
~ c2 : y=9+t^2*(-5)
~ c3 : y'=t*(-10)
~ PP3
~ c1 : t=3*5^((-1)/2)
~ c2 : y=0
~ c3 : y'=24*5^((-1)/2)
~ c4 : y''=-10
~ c5 : y'=-6*5^(1/2)
~ ここでエラー(execution stack)
<
- Unsat Coreの存在する場所
-- c3 : y'=24*5^((-1)/2)
--- c3 : BOUNCEのガード条件の後件
-- c5 : y'=-6*5^(1/2)
--- c5 : FALLでy''について述べられているためy'に連続性が生じる
- 次のように表示される
~ -----unsat core-------------------------------------------------------------
~ BOUNCE -> constraint : y'=(-4)/5*y'-
~ FALL -> constraint : y"=-10 -> continulty : y"
~ --------------------------------------------------------------------------------
- このようにして, HydLaプログラム中でバグの原因となる制約について発見できる
