model checking - Check CTL specification in SMV -

when try check "eg (!s11included & !s10included)" in smv, reported false , gives counter example follows, think on contrary support ctl specification. there wrong ctl specification?

-- specification eg (!s11included & !s10included)  false -- demonstrated following execution sequence trace description: ctl counterexample  trace type: counterexample    -> state: 9.1 <-     s00included = true     s01included = true     s10included = false     s11included = false 

short answer:

no, there isn't wrong ctl specification: observe normal , entirely depends on model specification.

the tool prints counter-example first state (included) violating given property. although appears bit arbitrary human operator since reason property violation can hidden execution trace itself, design choice makes perfect sense point of view of ctl model checking. the important thing note result can trusted and, more importantly, double-checked running simulation.

---

example:

i invite @ following example.

module main var : boolean; var b : boolean;  assign next(a) := case     = false : { true };     true      : { true, false };   esac;  next(b) := case     b = false : { true };     true      : { true, false };   esac;  ctlspec eg (!a & !b); 

in model, whenever a (resp. b) false deterministically set true, otherwise allow change arbitrarily.

if check ctl property, same yours, obtain following counter-example:

nusmv > reset; read_model -i test.smv ; go; check_property -- specification eg (!a & !b)  false -- demonstrated following execution sequence trace description: ctl counterexample  trace type: counterexample  -> state: 1.1 <-   = false   b = false 

as can see, counter-example matches yours 100%. going on?

well, nusmv conservatively prints fewest number of states necessary in order reach state in property violated. in case, initial-state of execution trace violates property, because next, deterministic, transition leads state in either a or b true (in specific case, both):

nusmv > pick_state -s 1.1 nusmv > simulate -iv -k 2 ********  simulation starting state 3.1   ********  ***************  available states  *************  ================= state ================= 0) -------------------------   = true   b = true   there's 1 available state. press return proceed.  chosen state is: 0  ***************  available states  *************  ================= state ================= 0) -------------------------   = true   b = true   ================= state ================= 1) -------------------------   b = false   ================= state ================= 2) -------------------------   = false   b = true   ================= state ================= 3) -------------------------   b = false   choose state above (0-3): ^c 

my conjecture model has similar behaviour, , reason why obtain same result.