伝播遅延のあるuppaalにモデルの単純なNOTゲートがあります。しかし、私は 1 つのプロパティを証明することができません。オートマタのスクリーンショットを添付します。Xinp は入力、xout は出力です。ここでは伝播遅延として 3 を使用します。
P1: A[] (xinp && t>3 imply (xout==!xinp))
このプロパティは正しく機能しており、3 時間単位の後、出力は入力の否定になります。
P2: A[] (xinp && t<3 imply (xout==!xinp))
このプロパティは満足できないはずなので、not ゲートが伝搬遅延の後、3 時間単位の出力が not ゲートに従っていない前に機能していることを確認できます。しかし、この特性は満足できないものではありません。
ありがとう
