i hame fsm like this 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
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;