nusmv

Digicode in Nusmv


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


Solution

  • 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:

    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.