NuSMV: how to exclude a possible next state

Question

I want to exclude a possible next case under specific conditions. For example, I have:

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;
...

The same for all the values 1..6. Otherwise, I have to do a lot of combinations to return only the position that are free.

Has anyone an idea if this is possible?

Answer 1

A possible approach is to further constraint the space of states with

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

Please beware that an inadvertent use of TRANS can result in a Finite State Machine which has no initial state or it contains some state s_i which does not have any future state:

source: nuXmv: Introduction.