Digicode in Nusmv

Question

i am new with NUSMV i am trying to modelise a digicode for reconize 41708 but user can't do more 3 error. if you enter more 3 error the system go to state bloked to wait when you enter special code to be unblocked. it is my code if you cant help me with idea and suggest code to finish .

MODULE main
VAR
val1 : {0,1,2,3,4,5,6,7,8};
location : {E1,E2,E3,E4,E5,succes,blocked,unblocked,verified};
cpt : 0..3;
block : boolean;
NumberEnter : 0..5 ;


ASSIGN
init(cpt):=0;
init(block):=FALSE;
init(location):=E1;


next(location):= case 
        (location=E1) &(cpt!=3)  & (block!=TRUE) :E2 ;
        (location=E2) & (cpt!=3) & (block!=TRUE) :{E3,E1,blocked};

        (location=E3) & (cpt!=3) & (block!=TRUE) :{E2,E1,blocked} ;
        (location=E4) & (cpt!=3) & (block!=TRUE) :{E1,E5,blocked} ;
        (location=E5) & (cpt!=3) & (block!=TRUE) :{E1,blocked} ;
        TRUE:blocked;
        esac;


next(pas):= case 
            NumberEnter<5 :NumberEnter+ 1 ;

        TRUE:0;
        esac;

Image of Model

Answer 1

One possible solution is:

MODULE main()
VAR
    in_digit  : 0 .. 9;
    in_signal : boolean;
    dc : digicode(in_digit, in_signal);


MODULE digicode(in_digit, in_signal)
VAR
    state   : { RUN, OK, ERROR };
    idx     : 0 .. 4;
    counter : 0 .. 3;

DEFINE
    pwd := [4, 1, 7, 0, 8];

INIT state = RUN & idx = 0 & counter = 0;

ASSIGN
    next(state) := case
        state = RUN   & pwd[idx]  = in_digit & idx < 4     : RUN;
        state = RUN   & pwd[idx]  = in_digit               : OK;
        state = RUN   & pwd[idx] != in_digit & counter < 3 : RUN;
        state = RUN   & pwd[idx] != in_digit               : ERROR;
        state = ERROR & in_signal                          : RUN;
        TRUE                                               : state;
    esac;

    next(counter) := case
        state = RUN & pwd[idx] != in_digit & counter < 3 : counter + 1;
        state = RUN & pwd[idx]  = in_digit               : counter;
        TRUE                                             : 0;
    esac;

    next(idx) := case
        state = RUN & pwd[idx]  = in_digit & idx < 4 : idx + 1;
        state = RUN & pwd[idx] != in_digit           : 0;
        TRUE                                         : 0;
    esac;

--
-- the following invariants nicely restrict the set of viable
-- transitions when inputs can be ignored
--
INVAR
    in_signal     -> state = ERROR;

INVAR
    state = ERROR -> in_digit = 0;

INVAR
    state = OK    -> in_digit = 0;

The solutions assumes that one can only enter one digit at a time, through input in_digit, and that there is a separate control signal in_signal to reset the device.

The device has three possible states:

• RUN: the device reads an input digit from in_digit, and compares it with a fixed password sequence
• OK: the device recognized the input sequence some time in the past, and it is now ignoring any further input
• ERROR: the user made too many incorrect input attempts, and the device is ignoring any input digit until in_signal is true.

At the end of the model, I added three INVAR constraints which prune the transition space from edges that are not relevant to us because of some inputs being ignored at certain moments. Ignoring those inputs makes it much easier to simulate the system by hand.

The run the example, use NuSMV:

~$ NuSMV -int
~$ reset; read_model -i digicode.smv; go; pick_state -iv; simulate -iv -k 30
~$ quit

---

An alternative, and much simpler approach, would be to provide digicode with 5 input digits all at once. In this way, one can remove idx and pwd from the model, making it much simpler.