promela

2熱

1答えて

エラー：VECTORSZが小さすぎます

私はPromela、特にSPINを使用するのが初めてです。私は検証しようとしているモデルを持っており、問題を解決するためにSPINの出力を理解できません。ここで は私がやったことで次のように spin -a untitled.pml gcc -o pan pan.c ./pan 出力されました： pan:1: VECTORSZ is too small, edit pan.h (at de

concurrency formal-verification model-checking promela spin 2017-11-22

---

5熱

1答えて

vim構文定義をsublime-text2で使用する

vim構文ハイライト定義ファイルを崇高なテキストで使用（または変換）できるかどうか知りませんか？ 私はPROMELAのためのハイライトを検索し、唯一のvimのための1つを見つけましたが、私のデフォルトのエディタ として、私はhttps://github.com/vim-scripts/promela.vim/blob/master/syntax/promela.vim

sublimetext2 syntax-highlighting promela 2013-12-19

---

5熱

1答えて

スピンとプロメラの構文を使用したLTLモデルのチェック

私はDijkstraによって書かれたALGOL 60コードを「Cooperating sequential processes」という論文に再現しようとしています。このコードはmutexの問題を解決するための最初の試みです。 begin integer turn; turn:= 1; parbegin process 1: begin Ll: if turn = 2 the

model-checking spin promela 2013-03-05

---