spin

    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

    2熱

    2答えて

    PROMELA/SPINの 'any'チャンネルからメッセージを受け取る方法

    私はSpinでアルゴリズムをモデリングしています。 私はいくつかのチャンネルを持っているプロセスを持っています。そしてある時点で、メッセージが来るが、どのチャンネルからメッセージが来るのか分からないことを知っています。したがって、メッセージがいずれかのチャネルから来るまでプロセスを待機（ブロック）したい。どうやってやるの？
    spin 2012-03-28

    2熱

    1答えて

    Promelaで配列要素の非決定的な値を選択することはできませんか？

    私が書いているPromelaコードは以下の通りです。 491 byte api1[5]; 492 byte api2[5]; 493 byte api3[5]; 494 byte reftask1[5] 495 byte reftask2[5]; 496 byte reftask3[5]; 497 byte rid1[5]; 498 byte rid2[5]; 49
    spin promela 2016-09-26

    1熱

    1答えて

    スピンで複数の（またはすべての）違反トレースを求める

    スピンを使用してプロパティに対して複数の（またはすべての）違反トレースを取得することは可能ですか？ 例として、私は以下のPromelaモデルモデルを作成： byte mutex = 0; active proctype A() { A1: mutex==0; /* Is free? */ A2: mutex++; /* Get mutex */ A3: /* A's critical s
    model-checking spin promela 2016-08-30
最新の質問