Uppaalの使い方

Uppaal（http://www.uppaal.com/）の使い方を忘れそうなので、メモメモ

---

■編集

（１）立ち上げる
　　→Templateという名前のテンプレートが開く

（２）左側のナビゲーションツリーのDeclarations（日本語化してある場合「宣言」）をクリック
　　→右側の描画ペインが大域情報編集ペインにかわる

（３）大域情報を大域情報編集ペインに記入する
　　　大域クロック変数
　　　大域変数
　　　大域通信チャネル

（４）左側のナビゲーションペインで、「Template」をクリック
　　→描画ペインが表示される

（５）テンプレートの「名前」を変えて、テンプレート名をいれ、
　　　右にパラメータを設定する

（６）ナビゲーション側にある（５）で書き換えた名前をクリック、
　　　すると、下にDeclarations（日本語化してある場合「宣言」）が
　　　でてくるので、それをクリック
　　　→編集画面になるので、局所変数などを宣言する

（７）ナビゲーション側にある（５）で書き換えた名前をクリック
　　　描画ペインに戻るので、ロケーション（上の○に下に星？のやつ）を
　　　クリックして、ロケーションを置く（描画ペインでクリックすると置ける）

（８）続けて、→をクリック、ロケーションの始点をクリックして、終点をクリック
　　　すると、エッジが引ける

（９）太い→で選択できる。それをクリック後、ロケーション（○）をダブルクリックすると
　　　ロケーション編集というダイアログが出る。
　　　ここで、名前や不変条件、初期、アージェント、コミットの指定ができる

（１０）太い→で選択できる。それをクリック後、エッジ（→）をダブルクリックすると、
　　　エッジの編集というダイアログが出る。
　　　そこで、ガードに繊維可能条件、同期に同期通信イベント、更新に変数の更新（代入）を設定する

（１１）全部のロケーションとエッジを書いたら、ナビゲーションペインから「システム宣言」を
　　　クリック、プロセス割り当て編集を行う

　　　P1＝P(1)　のように、プロセス＝テンプレート（引数）を何個か書き、
　　　最後に
　　　System P1,P2,　　のように、System　プロセス,・・・という具合に書く

---

■シュミレーション

（１２）上記で編集が終わったので、シュミレーションを行う。
　シュミレータータブをクリックする。

（１３）左上が、実行可能なものを表示するので、そこを適当にクリックすると、
　　　　右上のオートマトンの状態や、右下のシーケンス図が動く

---

■検証
（１４）べりファイアタブをクリックする
（１５）検証式を「クエリ」に入れると（２番目のボックス）、「概要」（１番目のボックス）に入ってくる
（１６）追加ボタンをクリックすると、次のの検証式を入れられる。
（１６）検査したい検証式をクリックして、一番上の「検査」ボタンをクリックすると、一番下のボックスに結果がでる
（１７）反例トレースを出す場合は、検証のメニューで
　　　　　オプション→診断トレース→いくらか
　　　　を選択して「検査」、その後、「はい」をクリックして、シミュレーションタブをクリックして
　　　　シュミレーションを表示させると、判例とレースが見れる。