nusmv

1熱

1答えて

私は教育のためにモデル検査とNuSMVを学んでいます。私はNuSMVコードを編集して実行することができ、私はUARTが何であるかを公正に理解しています。私の仕事は、正式にUARTをNuSMVでモデル化することですが、現時点ではどのように行うのかよくわかりません。私は、UARTが8バイトの連続ビットとして1バイトを送信することを理解していますが、どうすればそれをモデル化できますか？私は出発点とし

0熱

1答えて

NuSMV Realtime CTL

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

0熱

2答えて

NuSMVがインストールされていません

Windows 10 OSにNuSMV-2.6.0-win64をインストールすることはできません。これは正常にダウンロードされましたが、抽出された 'bin'folderからはインストールできません。

-2熱

1答えて

NuSMVを学ぶ最も良い方法は何ですか？

基本的に、NuSMVを使って複雑なSimulinkモデルを構築することができます。私は公式のNuSMVガイドを試してみましたが、それは自分のような初心者にとっては複雑すぎます。また、NuSMVのSimulinkモデルのモデリングに焦点を当てた書籍はありません。

-1熱

1答えて

WindowsでNuSMV 2.6を実行しています

NuSMV Webサイトからファイルをダウンロードしましたが、実際にはシステム上でアプリケーションを実行できません。どんなリードも高く評価されます。ファイルは、フォルダ含まれています - ビン、libに、シェアを、あなたはコマンドライン上でそれを実行する必要があります

0熱

1答えて

NuSMVでグローバル定数を定義するにはどうすればよいですか？

私はCで #define n 5 に類似した方法で、NuSMVでグローバル定数を宣言するのか分かりません。 NuSMVでどうすればいいですか？

-2熱

1答えて

UPPAALまたはNuSMVを使用したエレベーター制御

NuSMVおよびUPPAALを初めて使用しています。この問題の解決に取り組んでいます。誰でも次の質問に対する解決策を提供できますか？モデル及び（5 4言うか）と LIXSの数の（例えば2または3）と数とフロアの数にサービスを提供あなた独自設計のエレベータシステムの制御系を解析ユーザーが個々のフロアにあり、別のものにgelngするための個別の希望がありますフロア。システムがあります。• 、

1熱

1答えて

モデルチェッカーを使用して特定のトレースを確認してください

私はオープン相互作用プロトコルのルールを定義するためにLTLを使用しています。私は、特定の対話が仕様に従っているかどうか、または何らかのルールが壊れていないかどうかを確認したい。私の直接のアプローチはNuSMVを使うことでしたが、問題は私がチェックしたい相互作用のモデルではなく、ただ一つの特定の有限のトレース（すべての状態のすべての変数の値）です。これをNuSMVで指定できる方法はありますか？

2熱

1答えて

XSAPエラー

私はXSAP（バージョン1.2.0）SMVモデルに渡すしようとしていたが、私はモデルがNuSMV（バージョン2.6.0で正常に動作します。このエラー [email protected]:~/Desktop$ python /home/panda/Desktop/xSAP/scripts/extend_model.py -v /home/panda/Desktop/brca.smv /home/pa