問題タブ [uppaal]

UPPAAL モデル チェッカーを使用してゲート レベルで同期回路をモデル化しています。クロックをモデル化する方法について混乱しています。私の目標は、セットアップ タイムとホールド タイムに違反していないことを確認することです。appal モデル チェッカーでクロックをテスト ベクトルとして指定するモデルをいくつか見つけました。たとえば、at=10 は立ち上がりエッジに相当し、at=20 は立ち下がりエッジであり、テスト ベクトルのように見えます。UPAAL で同期回路をモデル化する方法に関する基本的な例を誰かが提案できますか?

ありがとうございました

UPPAAL を使用してモデルをセットアップし、ベリファイアを使用してデッドロックをチェックしました。答えは: プロパティが満たされていない. したがって、デッドロックが存在します。

特定の状況におけるすべての変数の状態や現在の値など、デッドロックに関するより詳細な情報を UPPAAL で報告する方法はありますか?

時々 UPPAAL で、int x:=1-0 のような 2 つの値を取る整数変数の例を見つけましたが、これは正確にはどういう意味ですか? xが最初に「1」を取り、次に「0」をとるように、またはXは2つの値の単なる配列ですか?

ありがとうございました

伝播遅延のあるuppaalにモデルの単純なNOTゲートがあります。しかし、私は 1 つのプロパティを証明することができません。オートマタのスクリーンショットを添付します。Xinp は入力、xout は出力です。ここでは伝播遅延として 3 を使用します。

このプロパティは正しく機能しており、3 時間単位の後、出力は入力の否定になります。

このプロパティは満足できないはずなので、not ゲートが伝搬遅延の後、3 時間単位の出力が not ゲートに従っていない前に機能していることを確認できます。しかし、この特性は満足できないものではありません。

ありがとう

テンプレート セクション内でチャネルを宣言するときに、UPPAAL コンパイラがエラーをスローしないのはなぜですか? うまくいけば、他のテンプレートはこれらのチャネルにアクセスできないため、チャネル宣言は宣言セクション全体でのみ意味があるように見えます。それとも私は何かを見落としていますか？

ありがとう！

PS同期チャネルを介した「内部」テンプレート通信をモデル化したいのですが、テンプレート内でチャネルを宣言することが解決策になることを願っています。上の質問は、提起して答えるのが簡単なようです:)