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