1

英語で申し訳ありません、ウクライナ出身です) スピンシステムの検証を勉強し始めたばかりです。次の問題を出題しました: 「LTL 式の下の形式で提示: マーシャを愛しているなら、ダーシャを愛することはできません」。私はそれを行う方法を理解できません。これが私が得たものです: p - マーシャが取得した Gp のように、[] p コードの形式で表されます (ただし、書き方はわかりません):

int m = 4;
int d = 5;

proctype lab1(byte a; byte b){
    if
    :: (a > b) -> printf("%e\n",a)
    :: (a < b) -> printf("%e\n",b)
    fi
}

init {
    run lab1(m, d)
}

ltl la { []m }

これがナンセンスであることは理解していますが、あなたの助けを求めます。

4

1 に答える 1

1

「If I love Masha, I can't love Dasha」の LTL 表現が必要な場合は、これで十分かもしれません。

bool i_love_masha;
bool i_love_dasha;

ltl la { i_love_masha -> !i_love_dasha }

問題は、モデルの動作が何であるかです。私は次のようなものを推測します：

init {
  i_love_masha = true;
  i_love_dasha = true;   /* should be a violation! */
}

多分それはあなたを始めるでしょう。しかし、これがあなたの質問に正確に答えるかどうかはわかりません!

于 2014-03-05T15:46:41.087 に答える