問題タブ [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.

0 投票する
1 に答える
153 参照

java - ispin ヘルプ (LTL 式の到達不能状態)

ispin でシステムをモデル化しましたが、LTL 式を使用してシステムを検証しようとすると、次のような到達不能エラーが見つかりました

私のLTL式は

0 投票する
2 に答える
6903 参照

android - imageviewを常に回転させるには?

アクティビティの途中で画像ビューがあります。360 度無限に回転するようにするにはどうすればよいですか?

0 投票する
1 に答える
174 参照

automata - 2 つの LTL を比較する方法

2 つの LTL を比較して、一方が互いに矛盾する可能性があるかどうかを確認するにはどうすればよいですか? 階層的なステート マシンと、各ステートの動作を説明する LTL があるためです。ローカル LTL がグローバル LTL と矛盾する可能性があるかどうかを知る必要があります。「機能仕様と自動競合検出」という記事で、L(f) の交差 L(g) が空である場合、2 つの LTL プロパティ f と g が矛盾することを見ました。そして、これはまさに、プログラムとして f とプロパティとして ¬g を使用したモデル チェックの問題です。誰でもこれで私を助けることができますか?LTL f を SPIN/Promela のプログラムに変換するにはどうすればよいですか??

ありがとう。

0 投票する
2 に答える
449 参照

model-checking - SPIN で状態空間を表示する方法

iSpin (v. 1.1.4) の "Automata View" は、正確には何を示していますか? 1つのプロセスの制御フローの単なるグラフのようです。

システムの完全な状態空間を取得するにはどうすればよいですか?

たとえば、Ben-Ari: Spin Model Checker の原理では、図 4.1 が必要です。または概要では、図1が必要です。

0 投票する
1 に答える
776 参照

spin - 組み込みモデリングの promela/spin と uppaal の長所と短所

組み込みシステムをモデリングするための uppaal と spin/promela の長所と短所は何ですか?

私は少し混乱しています - ありがとう

0 投票する
2 に答える
616 参照

verification - Promela - 非決定論ではなく非決定論?

次のスニペットを検討してください。

これは、カウンターが 0 を下回るまで値 0..3 をかなり恣意的に出力し、その時点で別の数値を出力するか終了することを期待するでしょう。

しかし、そうではないようです。

返される値は、0、次に 1、次に 0、次に 1、次に 0、次に 1 だけです。

if/fi ステートメントの「非決定論」を誤解したのでしょうか?

(問題がある場合は、ubuntuでispinを使用してください)。

0 投票する
2 に答える
746 参照

verification - プロメラモデルで動作しないと主張しない

次の単純な PROMELA モデルを検討してください。

私は、spin -f を使用して生成された次の単純な主張で、このモデルを検証したかったのです。

ただし、これを使用した検証は

結果が出ません。-a オプションを試しても結果は得られません。任意のランダム シミュレーションは、ある時点で明らかに p が false であることを示しています。

基本的な何かが欠けていますか?