spin

1熱

1答えて

私はかなり簡単なプロメラモデルで作業しています。 2つの異なるモジュールを使用して、横断歩道/交通信号機として機能します。最初のモジュールは、現在の信号（緑色、赤色、黄色、保留中）を出力する信号灯です。このモジュールはまた、「歩行者」と呼ばれる信号を入力として受け取り、これは交差する歩行者があることを示す指標となる。第2のモジュールは横断歩道として機能する。信号機モジュールからの出力信号（緑、黄、

1熱

1答えて

SPINモデルチェッカーでは最大探索深度を小さくするには小さすぎますか？考えられる理由は何でしょうか？

私のモデル検証をしながら私は、コンパイル文字列が tesTdma.pml -aスピン最大検索深さが小さすぎる、奥行= 9999の状態で、このエラーを取得していますこのエラーの原因を理解していない。誰かが1.1.4とSPIN 6.4.7

2熱

1答えて

PromelaのNプロセス間でロックする

私はモデル検査のためにプロメラでプロジェクトをモデル化しようとしています。その中で、私はN個のノードをネットワークに持っています。したがって、各ノードに対して、私はプロセスを作ります。 init { byte proc; atomic { proc = 0; do :: proc < N -> run node (q[proc],proc);

1熱

1答えて

プロメラのキューをモデル化する方法は？

これでPromelaでCLH-RW lockをモデル化しようとしています。ロックの仕組みはシンプルです、本当に：キューは、リーダーとライターの両方が、新しいノードとCAS-INGを作成することによって、彼らがそうする単一bool succ_must_waitを含むノードをエンキューするtail、で構成されていそれはtailです。これにより、テールがノードの先行ノードpredになります。次に

2熱

1答えて

Jspinでmtypeを使用するときの宣言されていない変数エラー

JspinとPromelaを初めて使用しています。、家庭用警報システムは、個人のIDキーまたはパスワードを使用して活性化し、無効にすることができ、システムは約30秒の待機期間に入る活性化した後、ユーザーが避難することを可能にする時間を：私は、次のシステムを実装してみました警報が発令された後の安全区域、侵入が検知されたときにも警報器には待機時間または15秒の遅延があり、侵入者がパスワードを入力す

1熱

1答えて

PromelaのSPINがproctypeのエラーに達していません

私はSPINとPromelaには新しく、私のモデルではライブネスのプロパティを検証しようとしています。エラーコード： unreached in proctype P (0 of 29 states) unreached in proctype monitor mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"

1熱

1答えて

スピンの「深さに達した」とはどのような状態と遷移が考えられますか？主張したことがない使用（IsPinを持つ）検証のために

は、私は例えば、状態の数や遷移の数よりも多いdepth reachedで出力を得る： Full statespace search for: never claim + (REQ5) assertion violations + (if within scope of claim) cycle checks - (disabled by -DSAFETY)

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

1熱

1答えて

複数のLTL式をSPINでテストする

同じ.pmlファイルでテストしようとしている多くのLTL式があります。私の問題は、単一のltl式でエラーが見つかった場合、トレイルファイルは同じトレイルファイル名に書き込まれる（または上書きされる）ことです。私は私の選択のトレイルファイル名に書き込む方法を見つけることができませんでした。このオプションが存在するか知っていますか？そうでない場合は、毎回同じトレイルファイルを上書きせずに同じ.pml

1熱

1答えて

Spinで初期化されていない変数を作成する方法は？

Promelaは各変数を初期設定（0または宣言で与えられた値）するようです。未知の値で初期化される変数を宣言するにはどうすればよいですか？ドキュメントはif :: p = 0 :: p = 1 fi示唆が、私はそれが動作とは思わない：スピンはまだこの主張 bit p init { if :: p = 0 :: p = 1 fi } ltl { ! p } を検証（およびp偽造）だか