model-checkingnusmvnuxmv

syntax error nested NEXT operator in NuSMV


I try to use NuSMV to check my model and here is the code.

enter image description here

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!


Solution

  • 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