model-checking - 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 相同。否则，我必须做很多组合才能只返回空闲的位置。

有人知道这是否可能吗？

Answer 1

一种可能的方法是进一步限制状态空间

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

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

来源：nuXmv：简介。