問題タブ [uppaal]

現在、UPPAAL シミュレーターを実行しています。私のシミュレーターは、特定の時点でコードの実行を停止します。この点は、私が提供する宣言によって異なります。しかし、私は一般的にいつ時計が停止するのか知りたいですか? これを引き起こす何かがありますか？

sプロセスがセットからランダムに要素を選択する必要があるモデルがありますS。選択部分は単一の操作です。UPPAAL で私が知っている唯一の同様のデータ構造は配列です。

UPPAAL には一定のデータ構造が存在しますか? そうでない場合は、どうすれば作成できますか?

私のトポロジには次のような接続があります。

https://courses.cs.ttu.ee/w/images/e/e5/ITI0130_Lab3_IEEE1394.pdf

私は uppaal でシミュレーションを実行する宣言を書きました:

配列は、インデックスを持つノードの接続を指定します。たとえば、ノード「0」はどのノードとも接続されていないため、すべてのインデックスで 0 になります。ただし、ノード「1」はノード「2、4、5」に接続されています。したがって、そのインデックスには 1 があります。

シミュレーションを実行すると、2 つの引出線が表示されるようになりました。

シミュレーションを実行するときに、ノード「0」をトポロジに接続して、リーダーを 1 つ取得する必要があります。

ノード「0」をいくつかのノードに接続しようとしましたが、うまくいきませんでした。

これは私のモデルです：

どうすればこれを行うことができますか？

私の質問は Uppaal で乱数を生成できますか?

値の範囲から数値を生成したいと思います。さらに、整数だけでなく double 値も生成したいと考えています。

例: double [7.25,18.3]

同じことを話しているこの質問を見つけました。私はそれを試してみました。ただし、次のエラーが発生しました: 予期しない T_SELECT 構文エラーです。

うまくいきません。私は Uppaal の世界ではかなり新しいものです。あなたが私に提供できる助けをいただければ幸いです。

よろしく、

リアルタイム システムを検証するために、Timed Automata について詳しく知りたいです。現在、私は UPPAAL というツールに慣れようとしています。

簡単なグラフをいくつか描き、さまざまなプロパティを追加しました。モデル全体は、異なる機械ユニットがブロックを相互に受け渡す生産セル システムを表すと想定されています。

ブロック ( BlockCycle )、2 つの機械ユニット ( Feeder、FeederBelt )、およびブロックの到着を感知する 2 つのセンサーをモデル化しました。

私のシステムは理にかなっていると思っていましたが、行き詰まりました。

この遷移のターゲット状態は、不変条件に違反しています。モデルがこのように動作することを意図している限り、これは問題ではありません。

（いいえ、しませんでした。;P）

しかし、デッドロックの理由を見つけることができないようです。このツールはBlockCycleモデルを示していますが、そこで不変条件を指定していません。実際、すべての移行要件が満たされているため、移行 ( Pos7 からPos8へ)は確実に実行する必要があります。

以下に、システムがどのように進化し、最終的にスタックするかを示します (エラー メッセージが表示されます)。

ラベル:

• 緑 : プロパティ チェック (例: FB_RunningはFB_Running == trueを意味します)
• 濃い青: プロパティの更新/割り当て
• 濃い赤: ロケーション (例: Pos7またはPos8 )

問題のそれぞれの遷移を含む BlockCycleモデル:

私の質問: 実行できるトランザクションがまだあるのに、システムがデッドロックするのはなぜですか。

Edit1: Sensor7 の位置Active ( BlockAtPos[7]と呼ばれる) の不変プロパティを削除すると、デッドロックが解決されます。したがって、デッドロックする前の最後の遷移でSensor7とBlockCycleの間に同期がないため、矛盾が発生すると思います ( BlockAtPos[7]が false になる一方で、センサーはInActive遷移を行う機会がまだありません)。不変条件に違反しています。

注: 私の UPPAAL コード/ファイルはpcs.xmlにあります。

クラスに uppaal を使用していますが、select ステートメントを使用して範囲内の整数の配列を作成したいと考えています。

背景として、私は 3 人のプレイヤーと 3 つのヒープを持つ修正された nim のゲームをモデル化しています。プレイヤーは 1 つのヒープから最大 3 つのマッチを選択するか、すべてのヒープから同じ数のマッチを選択できます (十分な数があると仮定します)。それらのすべてにマッチが残っています。)

これまでのところ、（ベリファイアのいくつかの基本的なクエリによると）単一のヒープから試合を取り、3人のプレイヤーとのnimゲームを実行しているようですが、すべてのヒープから取得できるようにプレイヤーを拡張する必要があり、そうしないことをお勧めしますheap1Taken、heap1TakenAmount、heap2Taken、heap2TakenAmount などの変数をハードコーディングする:-)

組み込みシステムをモデリングするための uppaal と spin/promela の長所と短所は何ですか?

私は少し混乱しています - ありがとう

オートマトンを実行し、eps ファイルをエクスポートしました。しかし、eps ファイルから情報をさらに分析して取得するにはどうすればよいでしょうか。変数値を外部ログ ファイルに書き込むことはできますか? 前もって感謝します