2

我正在尝试使用 Spin Model Checker 对两个对象（A 和 B）之间的游戏进行模型检查。对象在板上移动，每个位置由其 (x,y) 坐标定义。这两个物体应该不会碰撞。我有三个进程：init，A Model，B Model。我正在检查一个 ltl 属性的模型：（用于检查两个对象是否曾经占据相同位置的 liveness 属性）

ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) }

我得到的错误线索是：init -> A Model -> B Model -> init

但是，根据显示的数据，我不应该得到错误线索（反例）：x_a=2，x_b=1，y_a=1，y_b=1。

同样，第一个 init 确实经过了 init 进程的所有行，但第二个只显示到它的最后一行。

此外，我的 A 模型和 B 模型仅由“do”块中的警卫和动作组成，如下所示。但是它们更复杂，并且在“->”右侧有 if 块

active proctype AModel(){
do
:: someValue == 1 -> go North
:: someValue == 2 -> go South
:: someValue == 3 -> go East
:: someValue == 4 -> go West
:: else -> skip;
od
}

我需要在原子块中放入任何东西吗？我问的原因是错误跟踪显示的行甚至没有进入“do”块，它只是两个模型的第一行。

编辑： LTL 属性是错误的。我将其更改为：

ltl prop1 { [] (!((x_a == x_b) && (y_a == y_b))) }

但是，我仍然得到完全相同的错误线索。

4

1 回答 1

2

您的 LTL 属性执行错误。本质上，SPIN 发现的反例是上述 LTL 的真正反例。

[] ( !(x_a == x_b) && !(y_z == y_b) )   =>
[] ( !(2 == 1) && !(1 == 1) )  =>
[] ( !0 && !1) =>
[] ( 1 && 0)   =>
[] 0  =>
false

LTL 应该是：

always not (same location) =>
[] (! ((x_a == x_b) && (y_a == y_b))) =>
[] (! ((2 == 1) && (1 == 1))) =>
[] (! (0 && 1) =>
[] (! 0) =>
[] 1 =>
true

关于你的初始化和任务。启动任务时，您希望确保在任务运行之前初始化已完成。我将使用以下两种方法之一：

init { ... atomic { run taskA(); run taskB() } where tasks are spawned once all initialization is complete`

或者

bool init_complete = false;
init { ...;  init_complete = true }
proctype taskA () { /* init local stuff */ ...; init-complete -> /* begin real works */ ... }

您的 LTL 可能在初始化期间失败。

并且根据您的问题，如果您更改 x 或 y，您最好在 atomic{} 中同时更改两者。

于 2012-04-15T03:57:24.533 回答