問題タブ [promela]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
spin - iSpin LTL プロパティの評価は、アクティブ化された「アサーション違反」のみですか?
iSpin/Promela に慣れようとしています。私は使っている：
Spin バージョン 6.4.3 -- 2014 年 12 月 16 日、iSpin バージョン 1.1.4 -- 2014 年 11 月 27 日、TclTk バージョン 8.6/8.6、Windows 8.1。
これは、LTL を使用しようとする例です。for ループの 2 つのステップがアトミックでない場合、LTL プロパティの検証でエラーが発生するはずです。
検証タップでは、LTL プロパティをテストしたいだけなので、すべての安全プロパティを無効にして、「使用クレーム」を有効にします。クレーム名は「alwaysten」です。
しかし、「アサーション違反」をアクティブにすると、LTL プロパティが評価されるだけのようです。なんで？同僚が iSpin v1.1.0 を使用していますが、これを有効にする必要はありませんか? 私は何を間違っていますか？アサーションと LTL プロパティを独立して証明したい...
トレースは次のとおりです。
deadlock - 飢餓を避ける方法は？
コードを修正しようとしています。デッドロックと相互排除の問題を解決しましたが、promela (PML) にはモニターがないため、飢餓を回避する方法がわかりません。誰かが私を助けることができますか？前もって感謝します
automata - 2 つの LTL を比較する方法
2 つの LTL を比較して、一方が互いに矛盾する可能性があるかどうかを確認するにはどうすればよいですか? 階層的なステート マシンと、各ステートの動作を説明する LTL があるためです。ローカル LTL がグローバル LTL と矛盾する可能性があるかどうかを知る必要があります。「機能仕様と自動競合検出」という記事で、L(f) の交差 L(g) が空である場合、2 つの LTL プロパティ f と g が矛盾することを見ました。そして、これはまさに、プログラムとして f とプロパティとして ¬g を使用したモデル チェックの問題です。誰でもこれで私を助けることができますか？LTL f を SPIN/Promela のプログラムに変換するにはどうすればよいですか??
ありがとう。
model-checking - SPIN で状態空間を表示する方法
iSpin (v. 1.1.4) の "Automata View" は、正確には何を示していますか? 1つのプロセスの制御フローの単なるグラフのようです。
システムの完全な状態空間を取得するにはどうすればよいですか?
たとえば、Ben-Ari: Spin Model Checker の原理では、図 4.1 が必要です。または概要では、図1が必要です。
promela - Promela でブーリアン AND 評価を非アトミックにモデル化するにはどうすればよいですか?
Promela でブーリアン AND 評価を非アトミックにモデル化するにはどうすればよいですか?
while (flag[j] == true && victim == i)AND 評価を非アトミックに行うステートメントをモデル化したいと考えています。
これはどのように可能ですか？
spin - 組み込みモデリングの promela/spin と uppaal の長所と短所
組み込みシステムをモデリングするための uppaal と spin/promela の長所と短所は何ですか?
私は少し混乱しています - ありがとう