問題タブ [spin]
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.
java - ispin ヘルプ (LTL 式の到達不能状態)
ispin でシステムをモデル化しましたが、LTL 式を使用してシステムを検証しようとすると、次のような到達不能エラーが見つかりました
私のLTL式は
android - imageviewを常に回転させるには?
アクティビティの途中で画像ビューがあります。360 度無限に回転するようにするにはどうすればよいですか?
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が必要です。
spin - 組み込みモデリングの promela/spin と uppaal の長所と短所
組み込みシステムをモデリングするための uppaal と spin/promela の長所と短所は何ですか?
私は少し混乱しています - ありがとう
verification - Promela - 非決定論ではなく非決定論?
次のスニペットを検討してください。
これは、カウンターが 0 を下回るまで値 0..3 をかなり恣意的に出力し、その時点で別の数値を出力するか終了することを期待するでしょう。
しかし、そうではないようです。
返される値は、0、次に 1、次に 0、次に 1、次に 0、次に 1 だけです。
if/fi ステートメントの「非決定論」を誤解したのでしょうか?
（問題がある場合は、ubuntuでispinを使用してください）。
verification - プロメラモデルで動作しないと主張しない
次の単純な PROMELA モデルを検討してください。
私は、spin -f を使用して生成された次の単純な主張で、このモデルを検証したかったのです。
ただし、これを使用した検証は
結果が出ません。-a オプションを試しても結果は得られません。任意のランダム シミュレーションは、ある時点で明らかに p が false であることを示しています。
基本的な何かが欠けていますか？