以语句LTl的形式表示，自旋

Question

很抱歉，我的英语，我来自乌克兰)只是开始学习自旋系统验证。我们问了以下问题：“以下面的形式表达LTL :如果我爱玛莎，我就不能爱达莎”。我不知道该怎么做。下面是我得到的:P-类Masha获得的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 } 

我知道这是胡说八道，但我请求你的帮助。

Answer 1

如果你只需要一个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! */
}

也许这会让你开始。但是，我不确定这是否完全回答了你的问题！