logictemporalctlnusmv

NuSMV passes wrong specification

I am new to NuSMV and CTL and was trying simple Examples. I have 3 states A, B, and C and there is a transition from A-> B

I modeled it in NuSMV and want to check if there is any execution path from B to A. Eventhough I have not defined such transition, The Specification gives me counter example.

Module main
VAR
state:{a,b};
ASSIGN
init(state):=a;
next(state):=b;
SPEC !EF(state=a -> state=c)
SPEC !EF(state=b -> state=a)

Can anyone tell whats wrong in this?

how do i write specification for "is A reachable from B?" - this should return false as there is no transition defined

Solution

  • Note: your code example was not working on my machine, it reported some syntactic errors, so I have actually changed it to look like this:

    MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state):=b;

    Comments on your approach. The property SPEC !EF(state=a -> state=c) can be read as:

    it is not true that there exists a path starting from the initial state such that sooner or later the logic condition state=a -> state=c is true.

    The condition state = a -> state = c is true for all states such that state != a only, because there exists no state in which the conditions state = a and state = c can hold at the same time.

    If you run NuSMV, you are given the following counter-example:

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

    In state 1.2 the variable state is equal to b, therefore state = a -> state = c is true and !EF(state = a -> state = c) is violated.

    Similar considerations hold for the property SPEC !EF(state=b -> state=a).

    One-Step Reachability. If you want to check that there exists no one-step transition from a state in which state = a holds to a state in which state = c holds, then you can use the following property:

    SPEC AG (state = a -> AX state != c)

    This reads:

    for all states, that can be reached following all execution paths starting from all initial states, the CTL property state = a -> AX state != c is always verified. Such property says that, if in the current state state = a, then it is necessarily the case that in all possible immediate next states the value of state is different from c.

    If we check such property with NuSMV, we find out that it is verified:

    NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true

    A similar example holds for the other property that you want to encode.

    Path Reachability. If you want to check that there exists no path, formed by an arbitrary and variable number of intermediate transitions, that reaches a state in which state = c holds, starting from a state in which state = a holds, then the encoding is slightly different:

    SPEC AG (state = a -> AX AG state != c)

    This reads:

    for all states, that can be reached following all executions paths starting from all initial states, the CTL property state = a -> AX AG state != c is always verified. Such property is true for all states s' s.t.

    • state != a in s'

    or

    • state = a in s', and state != c for all reachable states s'' on all the outgoing paths that start at s'

    If we check such property with NuSMV, we find that it is verified:

    NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX (AG state != c))  is true

    To better outline the difference among the two encodings, I'll drop here a model example on which the first property is false but the second one is true:

    MODULE main ()
VAR
  state : {a,b,c};

ASSIGN
  init(state):=a;
  next(state) := case
     state = a : b;
     state = b : c;
     TRUE : state;
    esac;

SPEC AG (state = a -> AX state != c)
SPEC AG (state = a -> AX AG state != c)

    If you run NuSMV over this example, the output is the following one:

    NuSMV > reset; read_model -i test.smv; go; check_property
-- specification AG (state = a -> AX state != c)  is true
-- specification AG (state = a -> AX (AG state != c))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  state = a
-> State: 1.2 <-
  state = b
-> State: 1.3 <-
  state = c

    Obviosly, if the first property is found to be false, then the second property must necessarily be false as well.

    K-Steps Reachability. The one-step reachability encoding can be generalised to reachability in exact k steps by increasing the number of AX in the formula:

    SPEC AG (state = a -> AX state != c)       -- state != c after 1 transition
SPEC AG (state = a -> AX AX state != c)    -- state != c after 2 transitions
SPEC AG (state = a -> AX AX AX state != c) -- state != c after 3 transitions
SPEC AG (state = a -> AX ... state != c)   -- state != c after 1 + |...| transitions

    ETA:

    In this use-case scenario, the property

    SPEC AG (state = a -> AX AG state != c)

    could be simplified to 

    SPEC AG (state = a -> AG state != c)

    and, apparently, it would still work.

    However, there is a reason why I did not do it: there is a subtle semantic difference among the two encodings, and even though the latter can be used to verify a reachability property in some cases, the former encoding is more robust since it more closely matches the actual semantics of the reachability problem. e.g. the template B_COND_1 -> AG B_COND_2 fails miserably whenever B_COND_2 := !B_COND_1, because for any state s' that verifies the premise B_COND_1 the conclusion AG B_COND_2 --which can be rewritten as AG !B_COND_1-- cannot possibly hold; prepending AXto the conclusion adds one level of indirection, and it is more correct because the conclusion should only be required to hold starting from the next states in the execution tree.

    ETA #2:

    You write:

    how do i write specification for "is A reachable from B?" - this should return false as there is no transition defined

    A property that returns false when there is no path from state = b to state = a, is the following:

    SPEC AG (state = b -> EF state = a)

    If you want to verify that it is never the case that state = a is reachable from state = b, then this is actually a bad idea for two reasons:

    For these reasons I actually encoded the reachability problem the other way around, returning true when state = a is not reachable from state = b and false + single counter-example otherwise.