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