Uppaal（http://www.uppaal.com/）の使い方を忘れそうなので、メモメモ
■編集
（１）立ち上げる
→Templateという名前のテンプレートが開く
（２）左側のナビゲーションツリーのDeclarations（日本語化してある場合「宣言」）をクリック
→右側の描画ペインが大域情報編集ペインにかわる
（３）大域情報を大域情報編集ペインに記入する
大域クロック変数
大域変数
大域通信チャネル
（４）左側のナビゲーションペインで、「Template」をクリック
→描画ペインが表示される
（５）テンプレートの「名前」を変えて、テンプレート名をいれ、
右にパラメータを設定する
（６）ナビゲーション側にある（５）で書き換えた名前をクリック、
すると、下にDeclarations（日本語化してある場合「宣言」）が
でてくるので、それをクリック
→編集画面になるので、局所変数などを宣言する
（７）ナビゲーション側にある（５）で書き換えた名前をクリック
描画ペインに戻るので、ロケーション（上の○に下に星？のやつ）を
クリックして、ロケーションを置く（描画ペインでクリックすると置ける）
（８）続けて、→をクリック、ロケーションの始点をクリックして、終点をクリック
すると、エッジが引ける
（９）太い→で選択できる。それをクリック後、ロケーション（○）をダブルクリックすると
ロケーション編集というダイアログが出る。
ここで、名前や不変条件、初期、アージェント、コミットの指定ができる
（１０）太い→で選択できる。それをクリック後、エッジ（→）をダブルクリックすると、
エッジの編集というダイアログが出る。
そこで、ガードに繊維可能条件、同期に同期通信イベント、更新に変数の更新（代入）を設定する
（１１）全部のロケーションとエッジを書いたら、ナビゲーションペインから「システム宣言」を
クリック、プロセス割り当て編集を行う
P1＝P(1) のように、プロセス＝テンプレート（引数）を何個か書き、
最後に
System P1,P2, のように、System プロセス,・・・という具合に書く
■シュミレーション
（１２）上記で編集が終わったので、シュミレーションを行う。
シュミレータータブをクリックする。
（１３）左上が、実行可能なものを表示するので、そこを適当にクリックすると、
右上のオートマトンの状態や、右下のシーケンス図が動く
■検証
（１４）べりファイアタブをクリックする
（１５）検証式を「クエリ」に入れると（２番目のボックス）、「概要」（１番目のボックス）に入ってくる
（１６）追加ボタンをクリックすると、次のの検証式を入れられる。
（１６）検査したい検証式をクリックして、一番上の「検査」ボタンをクリックすると、一番下のボックスに結果がでる
（１７）反例トレースを出す場合は、検証のメニューで
オプション→診断トレース→いくらか
を選択して「検査」、その後、「はい」をクリックして、シミュレーションタブをクリックして
シュミレーションを表示させると、判例とレースが見れる。
アクセス
トータル
ランキング
