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: Введение.