問題タブ [model-checking]

グラフ文法モデリング (モデル チェック)に関する研究論文を勉強していました。理解を深めるために、私は研究者が行った実験を調査し始めました。

ドット表記を使用してグラフ構造を指定し、 や などの属性を使用labelangle=-35しました。type = "rt|re|node"

インターネット上でドット言語の適切なリファレンスを見つけることができません。初心者の観点から始めたものはありません。私がstackoverflowを検索したとき、いくつかの表記法が時代遅れになったが文献にはまだ存在しているため、ドットで物事を指定する標準的な方法はないと感じました.

type誰かが属性の目的、またはlabelangle少なくともこのコンテキストで何を説明してくれますか。

注: どちらtypeもlabelangle、graphviz によって生成されたグラフに違いがあるようには見えません。

たとえば、58 ページのトポロジ形成の詳細な説明で悪いパターンとして引用されている次のグラフを考えてみましょう (悪いパターンとは何かについて心配する必要はありません。研究者が論文で定義したものです)。このドット ファイルを使用して作成されます。 :

私がこれまでに開発した理解から、エッジとノードのマッピングがドットファイルと出力グラフで指定されたものと同じではないため、このグラフが上記のドットファイルの出力であるべきかどうかさえわかりません。

助けてください。

次のコードでは、

次のエラーが表示されます。

どうしてこんなことに？Promela は cond1 のすべての値 (cond1 == 0 と cond1 != 0 の両方) に対して実行すべきではありません。少なくともこれはここに書かれているものです。

このモードでは、実際にはすべての動作オプションが一度に 1 つずつ探索されるため、検証中にそのような呼び出しは行われません。

現在、UPPAAL シミュレーターを実行しています。私のシミュレーターは、特定の時点でコードの実行を停止します。この点は、私が提供する宣言によって異なります。しかし、私は一般的にいつ時計が停止するのか知りたいですか? これを引き起こす何かがありますか？

モデルチェッカーであるnusmv-tools( https://code.google.com/a/eclipselabs.org/p/nusmv-tools/ )をダウンロードします。それとその依存関係（xtextなど）をEclipseに正常にインストールし、Eclipseを再起動しました。

ここで、Eclipse が nusmv ファイル (拡張子は「.smv」) を認識することを期待していますが、認識できません。

私の質問は、Eclipse で nusmv ファイルを解析して、Eclipse が nusmv ファイル (.smv) を認識して強調表示するようにするにはどうすればよいかということです。

(xtext プロジェクト、Java プロジェクト、または一般的なプロジェクトを作成する必要がありますか? プロジェクトに追加するライブラリまたは外部 jar はどれですか?)

何か助けはありますか？ありがとう

A[] not deadlockモデルの検証ツールでクエリを実行すると、検証がエラーで停止します。

エラーのため、検証は中止されました。ほとんどの場合、これは範囲外の割り当てまたは範囲外の配列ルックアップが原因です。

これは、「範囲外の割り当てまたは範囲外の配列ルックアップ」が発生するまで、私のモデルがデッドロックフリーであることを暗黙のうちに意味しますか?