syntax error nested NEXT operator in NuSMV

Question

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!

Answer 1

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