NuSMV：如何排除可能的下一个状态

Question

我想在特定条件下排除下一个可能的案例。例如，我有：

token : array 1..2 of {0, 1, 2, 3, 4, 5, 6};
next(token[1]) := case
                 x : {1, 2, 3, 4, 5, 6};
                 TRUE : 0;
               esac;
next(token[2]) := case
                 x : {1, 2, 3, 4, 5, 6};
                 TRUE : 0;
               esac;
-- exclude state value 1 if !position1free
...

DEFINE position1free := token[1] != 1 & token[2] != 1;
...

所有值 1..6 都相同。否则，我必须做很多组合才能return只有空闲的位置。

有人知道这是否可行吗？

Answer 1

一种可能的方法是进一步限制 space 个具有

的状态

TRANS (!position1free) -> (next(token) != 1) ;

请注意，无意中使用 TRANS 可能会导致 有限状态机 没有初始状态或包含某些状态 s_i没有任何未来状态：

来源：nuXmv: Introduction.

NuSMV：如何排除可能的下一个状态

NuSMV: how to exclude a possible next state

model-checking

nusmv