- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
* Interactive mode とは [#f1c53d5e]
- 通常の処理系Hyroseは, 入力に対してそのシミュレーションの結果を返すのみである
- Interactive modeでは, シミュレーションの様子を見ながら対話的に実行をおこなう
-- モデルの理解を促進
-- モデルに操作を加えることが可能
-- デバッグ等に有用
* 利用法 [#l5c4ae5d]
- シミュレーション開始時にオプション"--in"でInteractive modeを有効にする
- <ENTER>を押す毎に1フェイズずつ実行を進める
- <ENTER>を押す毎に1フェイズずつ実行を進める("j 1"とおなじ動作を行う)
- 離散変化を行うPointPhase(PP)と, 連続変化の計算を行うIntervalPhase(IP)のそれぞれで入力を受け付ける
- 各時点でコマンドを入力し, それぞれの機能を有効にする
>
b [arg] : Break Point
ブレークポイントを設定する
h : Help
Helpを表示する
<
>
c [arg] : Change
変数値の変更を行う
j [arg] : Jump
現在の状況から, 与えられた数のフェイズだけジャンプする
positive number : forward (通常のシミュレーションと同じ)
negative number : backward
<
>
fu : Find unsat core
デバッグ情報としてのunsat coreを導出する
q : Quit this simulation
現在のシミュレーションを終了する
<
>
j [arg] : Jump
特定のフェイズにジャンプする
c : Change a value of a variable
変数値の変更を行う
<
>
p : Print
p : Display the information of the current phase
現在の状態をプリントする
<
>
q : Quit
シミュレーションを終了する
a : approx a value of a variable as interval
変数の値を区間値に変更して近似する
<
>
r : Run
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.
~ INIT <=> y=9 & y'=0.
~ FALL <=> [](y''=-10).
~ BOUNCE <=> [](y-=0 => y'=-(4/5)*y'-).
~ INIT, FALL, BOUNCE.
<
実行される動作
-採用されている制約(c)
>
PP0
c1 : t=0
c2 : y=9
c3 : y'=0
c4 : y''=-10
IP1
c1 : t=(0, 3*5^((-1)/2))
c2 : y=9+t^2*(-5)
c3 : y'=t*(-10)
PP1
c1 : t=3*5^((-1)/2)
c2 : y=0
c3 : y'=24*5^((-1)/2)
c4 : y''=-10
c5 : y'=-6*5^(1/2)
ここでエラー
~ 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''
---------
<
>
別の利用例
意図した制約が採用されない
-- その制約を含むunsat coreを求めることで原因を特定することができる
<
>
入出力例 プリント文
INIT <=> x=1.
EQ <=> [](x’=-1).
PRINT <=> [](x=0 =>
PRINTPP("Example PrintPP time=%d",TIME)
& PRINTIP("Example PrintIP%d",TIME)).
INIT, EQ.
<
- 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"
~ --------------------------------------------------------------------------------