Search code examples
fsmmodel-checkingnusmv

Convert FSM to NuSMV model

i hame fsm like this FSM

my FSM

and i wrote piece of code to check LTL property on FSM this is my LTL property 

G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))

my NuSMV code is 

MODULE main
VAR
    state : 0 .. 2;
    r1 : boolean;
    r2 : boolean;
    g1 : boolean;
    g2 : boolean;
ASSIGN
    init (state) := 0;
    init(r1) := FALSE;
    init(r2) := FALSE;
    init(g1) := FALSE;
    init(g2) := FALSE;
    next(state) :=
        case
            (state = 0) & (g1) & (r1) & (!r2) & (!g2)  : 1;
            (state = 1) & (g1) & (!r1) & (r2) & (g2)  : 0;
            (state = 0) & (!g1) & (!r1) & (!r2) & (!g2)  : 0;
            (state = 0) & (!g1) & (!r1) & (r2) & (g2)  : 0;
            (state = 0) & (g1) & (r1) & (r2) & (!g2)  : 0;
            (state = 1) & (g1) & (!r1) & (!r2) & (g2)  : 1;
            (state = 1) & (g1) & (r1) & (r2) & (!g2)  : 1;
            (state = 1) & (!g1) & (r1) & (!r2) & (!g2)  : 1;
            TRUE : state;
        esac;
    next(g1) :=
        case
            (state = 1) & (!r1) & (r2) & (g2)  : TRUE;
            (state = 0) & (!r1) & (!r2) & (!g2)  : FALSE;
            (state = 0) & (r1) & (!r2) & (!g2)  : TRUE;
            (state = 1) & (!r1) & (!r2) & (g2)  : TRUE;
            (state = 1) & (r1) & (!r2) & (!g2)  : FALSE;
            (state = 0) & (r1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (r1) & (r2) & (!g2)  : TRUE;
            (state = 0) & (!r1) & (r2) & (g2)  : FALSE;
            TRUE : g1;
        esac;
    next(r1) :=
        case
            (state = 0) & (g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (r2) & (g2)  : FALSE;
            (state = 1) & (!g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (!r2) & (g2)  : FALSE;
            (state = 0) & (!g1) & (!r2) & (!g2)  : FALSE;
            (state = 1) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (r2) & (g2)  : FALSE;
            TRUE : r1;
        esac;
    next(r2) :=
        case
            (state = 0) & (g1) & (r1) & (!g2)  : {TRUE, FALSE};
            (state = 1) & (!g1) & (r1) & (!g2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (g2)  : TRUE;
            (state = 1) & (g1) & (!r1) & (g2)  : {TRUE, FALSE};
            (state = 1) & (g1) & (r1) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (!r1) & (!g2)  : FALSE;
            TRUE : r2;
        esac;
    next(g2) :=
        case
            (state = 1) & (g1) & (r1) & (r2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (!r2)  : FALSE;
            (state = 1) & (g1) & (!r1) & (!r2)  : TRUE;
            (state = 0) & (g1) & (r1) & (!r2)  : FALSE;
            (state = 1) & (g1) & (!r1) & (r2)  : TRUE;
            (state = 1) & (!g1) & (r1) & (!r2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (r2)  : TRUE;
            (state = 0) & (g1) & (r1) & (r2)  : FALSE;
            TRUE : g2;
        esac;

After model checking with following command i wonder when i see NuSMV return True 

NuSMV -int
read_model -i test2.smv
flatten_hierarchy
encode_variables
build_model
pick_state -i

check_ltlspec -p "G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))"

NuSMV result is :

-- specification ( G !(r1 & r2) -> (( G (!g1 | !g2) &  G (r1 ->  F g1)) &  G (r2 ->  F g2)))  is true

but i can find CE manually after read NuSMV 2.6 User Manual i could not find which part of NuSMV code is wrong

Solution

  • i found problem something goes wrong in my model in this piece of code inputs modelled but it's not necessary because we just model system not environment

    next(r1) :=
        case
            (state = 0) & (g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (r2) & (g2)  : FALSE;
            (state = 1) & (!g1) & (!r2) & (!g2)  : TRUE;
            (state = 0) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (!r2) & (g2)  : FALSE;
            (state = 0) & (!g1) & (!r2) & (!g2)  : FALSE;
            (state = 1) & (g1) & (r2) & (!g2)  : TRUE;
            (state = 1) & (g1) & (r2) & (g2)  : FALSE;
            TRUE : r1;
        esac;
    next(r2) :=
        case
            (state = 0) & (g1) & (r1) & (!g2)  : {TRUE, FALSE};
            (state = 1) & (!g1) & (r1) & (!g2)  : FALSE;
            (state = 0) & (!g1) & (!r1) & (g2)  : TRUE;
            (state = 1) & (g1) & (!r1) & (g2)  : {TRUE, FALSE};
            (state = 1) & (g1) & (r1) & (!g2)  : TRUE;
            (state = 0) & (!g1) & (!r1) & (!g2)  : FALSE;
            TRUE : r2;
        esac;