問題タブ [nusmv]

NuSMV を Java のモデル チェッカーとして使用しようとしています。ただし、関連する JAR ライブラリをオンラインで見つけることができません。

私が見つけた唯一のものはここで提供されており、ダウンロード リンクはもう機能しません。どうやら、ライブラリは存在しますが、アクセス リンクが機能していません。

NuSMV Java API ライブラリにアクセスする方法を知っている人、または別の方法を知っている人はいますか?

AG(~q ∨ Fp)以下のモデルで LTL 式は満たされていますか? なぜ、またはなぜではないのですか？

モデル？

LTL を使用して、オープン インタラクション プロトコルのルールを定義しています。次に、特定のインタラクションが仕様に従っているかどうか、またはルールに違反していないかどうかを確認したいと思います。私の当面のアプローチは NuSMV を使用することでしたが、問題は、確認したい相互作用のモデルがなく、特定の有限トレース (すべての状態のすべての変数の値) が 1 つしかないことです。

NuSMV でこれを指定する方法はありますか? 基本的に、NuSMV が反例として出力するモデルの 1 つを入力したいと思います。

そして、それを確認してください。それとも、NuSMV はこのための間違ったツールですか?

ありがとう！

NuSMV を使用しており、リアルタイム CTL プロパティを書き込もうとしています。
次のように、状態からステップを設定する方法があるかどうかを知りたいです。
((s.state = on) ABG (0..5 s.state = off))

として読み取られます: if (s.state=on) is true、この状態から、および他の 5 つのステップでは、プロパティ(s.state= off) is true.
このようなことを書き込もうとしましたが、うまくいきません。手伝って頂けますか？

そうでなければ、最初ではない状態から同じプロパティをチェックすることは可能ですか?

教育のためにモデルチェックと NuSMV を学んでいます。私は NuSMV コードを編集して実行することができ、UART とは何か、何をするのかについてかなり理解しています。

私の仕事は、NuSMV で UART を正式にモデル化することですが、現時点ではその方法がわかりません。UART が 1 バイトを 8 つの連続ビットとして送信することは理解していますが、それをどのようにモデル化できますか?

出発点としてミューテックスコードがあります：

コード

Eclipse の nuseen 更新サイトが機能していません。