I try to use NuSMV to check my model and here is the code.
However, when I input NuSMV kernel.smv
in the shell, it occur an error
file kernel.smv: line 16: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(tx.fired) at line 16
I'm a newbie in NuSMV model checker, so I could not fix this syntax error. Please help, thanks!
I was able to create a MVCE out of your image:
MODULE trans(cond)
VAR
fired : boolean;
ASSIGN
init(fired) := FALSE;
next(fired) := case
!next(cond) : TRUE;
TRUE : FALSE;
esac;
MODULE main
VAR
_b : boolean;
t : trans(_cond);
DEFINE
_cond := (_b != next(_b));
Here the design problem is exactly what the model checker tells you in the error message:
NuSMV > reset; read_model -i t.smv ; go
file t.smv: line 6: nested NEXT operators: next(_b)
in definition of next(_cond)
in definition of next(t.fired) at line 6
There is a double nesting of the next()
operator within itself, and this isn't supported as it would require the execution horizon to be increased beyond the current_state + chosen_transition pair, and know which transition is taken from a future state that is still under construction.
Workaround.
Let's take the following model, which has the same problem as yours:
MODULE main()
VAR
frst : 0 .. 1;
scnd : boolean;
ASSIGN
init(frst) := 0;
init(scnd) := FALSE;
next(scnd) := case
next(middle) : TRUE;
TRUE : FALSE;
esac;
DEFINE
middle := (frst != next(frst));
we want scnd
to be true
iff the value of frst
is going to change amidst the next()
and the next(next())
state.
To do so, we can delay the beginning of the execution trace, so that we can predict the future value of frst
with sufficient advantage.
Let's see it with an example:
MODULE main()
VAR
hidden : 0 .. 1;
frst : 0 .. 1;
scnd : boolean;
ASSIGN
init(hidden) := 0;
init(frst) := 0;
init(scnd) := FALSE;
next(frst) := hidden; -- frst does not start "changing" arbitrarily
-- in the second state, but in the third state
next(scnd) := case
predicted : TRUE; -- true iff frst changes value 2 states from now
TRUE : FALSE;
esac;
DEFINE
middle := (frst != next(frst)); -- true iff frst changes value
-- from the current state to the
-- next() state
predicted := (hidden != next(hidden)); -- true iff frst changes value
-- from the next state to the
-- next(next()) state