* 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 [#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.
<
実行される動作
>
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)
ここでエラー
<
>
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.
<
