Check CTL specification in SMV

Question

When I try to check "EG (!s11included & !s10included)" in SMV, it is reported false and gives a counter example as follows, which I think on the contrary it support this CTL specification. Is there something wrong with my CTL specification?

-- specification EG (!s11included & !s10included)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 9.1 <-
    s00included = TRUE
    s01included = TRUE
    s10included = FALSE
    s11included = FALSE

Answer 1

SHORT ANSWER:

No, there isn't anything wrong with your CTL specification: what you observe is normal and entirely depends on your model specification.

The tool prints a counter-example up to the first state (included) violating a given property. Although it appears a bit arbitrary to a human operator since the reason for a property violation can get sometimes hidden from the execution trace itself, this design choice makes perfect sense from the point of view of CTL model checking. The important thing to note is that the result can be trusted and, more importantly, double-checked by running a simulation.

---

EXAMPLE:

I invite you to look at the following example.

MODULE main
VAR a : boolean;
VAR b : boolean;

ASSIGN
next(a) := case
    a = FALSE : { TRUE };
    TRUE      : { TRUE, FALSE };
  esac;

next(b) := case
    b = FALSE : { TRUE };
    TRUE      : { TRUE, FALSE };
  esac;

CTLSPEC EG (!a & !b);

In this model, whenever a (resp. b) is FALSE we deterministically set it to TRUE, otherwise we allow it to change arbitrarily.

If we check the CTL property, which is exactly the same as yours, we obtain the following counter-example:

NuSMV > reset; read_model -i test.smv ; go; check_property
-- specification EG (!a & !b)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  a = FALSE
  b = FALSE

As you can see, the counter-example matches yours 100%. What is going on?

Well, basically NuSMV conservatively prints the fewest number of states necessary in order to reach a state in which the property is violated. In this case, the initial-state of the execution trace already violates the property, because the next, deterministic, transition leads to a state in which either a or b are TRUE (in this specific case, both):

NuSMV > pick_state -s 1.1
NuSMV > simulate -iv -k 2
********  Simulation Starting From State 3.1   ********

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  a = TRUE
  b = TRUE


There's only one available state. Press Return to Proceed.

Chosen state is: 0

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
  a = TRUE
  b = TRUE


================= State =================
1) -------------------------
  b = FALSE


================= State =================
2) -------------------------
  a = FALSE
  b = TRUE


================= State =================
3) -------------------------
  b = FALSE


Choose a state from the above (0-3): ^C

My conjecture is that your model has a similar behaviour, and that is the reason why you obtain the same result.