Interactive mode

Interactive mode とは †

  • 通常の処理系Hyroseは, 入力に対してそのシミュレーションの結果を返すのみである
  • Interactive modeでは, シミュレーションの様子を見ながら対話的に実行をおこなう
    • モデルの理解を促進
    • モデルに操作を加えることが可能
    • デバッグ等に有用
↑

利用法 †

  • シミュレーション開始時にオプション"--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 †

  • インタラクティブモードでは, unsat coreを利用した柔軟なシミュレーションを容易に行うことができる
  • また, インタラクティブモードでなくてもunsat core利用したシミュレーションは可能である
↑

Unsat Coreとは †

  • ある充足不可能となる制約集合の部分集合で, 極小矛盾集合のこと
  • 次の条件を満たすψをUnsat Coreという 
     φ : 充足不可能となる制約集合
 1. φ = ψ ^ ψ'
 2. ψは充足不可能
 3. ψ中の各制約{c}についてψ\{c}は充足可能
↑

HydLaにおけるバグ †

  • Hyroseでは各時刻において変数が満たすべき制約を求める
  • 制約には優先順位をつけることができる
  • HydLaプログラムの制約に関して, 望んだ動作でない場合がある
    • 満たすべき制約集合が充足不可能となる
    • 採用されてほしい制約が採用されない
↑

Unsat Coreを用いたバグの特定 †

  • シミュレーション中に意図しない動作が現れた時点で解析を行う
  • 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プログラム中でバグの原因となる制約について発見できる
Last-modified: 2017-03-02 (Thu) 03:21:30 (2605d)