問題タブ [promela]

複数のステートメントを無限に頻繁に実行する必要があるという公平性の制約があるプログラムで、LTL プロパティを検証できるかどうか疑問に思っています。

例えば：

このプログラムは、最終的にno_flipフラグが trueに flagなり、true になった場合に正しいです。

ただし、'pan -a' と 'pan -a -f' (弱い公平性) の両方を実行すると、no_flip=1ステートメントと受け入れ状態 (LTL 式から) を循環します。

進行状況ラベルは、実行が無限に頻繁に通過することを強制すると思っていましたが、そうではないようです。では、そのような公平性制約を追加することは可能ですか?

ありがとう、ヌーノ

Spin を使用してベーカリー ロックを作成しました

テストすると、次のエラーが表示されます: pan:1: アサーション違反 - 無効な配列インデックス (深さ 5)

トレイルを走ると、これが戻ってきます

この行をスキップする理由を誰か教えてください (i == n) -> break; ?

上記のコードは、「構文エラーが「チョップスティック」の近くに「識別子」を見ました」というエラーを送信します

Sublime Text で vim Syntax Highlight Definition Files を使用 (または変換) できるかどうかを知っている人はいますか?

promela 用の蛍光ペンを探していて、vim 用の蛍光ペンしか見つかりませんでしたが、デフォルトのエディターとして sublime-text を使用しています

私が見つけた定義https://github.com/vim-scripts/promela.vim/blob/master/syntax/promela.vim

私はプロメラが初めてです。私はpromelaで書かれたプログラミングを持っています:

このプログラムの遷移システムを描く方法を知っている人はいますか?

グローバル変数のデフォルト値はありますか? または、モデル チェッカーは可能なすべてのインターリービングをチェックします。つまり、この場合、 と の両方(x==0)で可能なすべての状態を使用し(x>0)ます。

次のコードでは、

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

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

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