对不起我的英语,我来自乌克兰)才开始研究旋转系统验证。我们问了以下问题:“用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 }
我知道这是胡说八道,但我请求您的帮助。