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

如果您只需要“如果我爱玛莎,我就不能爱达莎”的 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 回答