NuSMV - AND model

Question

I'm trying to write the following model in NuSMV

In other words, z becomes bad only when x AND y are in the state bad too. This is the code I've written

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = good) -> next(state) = bad
    TRANS (state = bad) -> next(state) = bad

MODULE effect(cond)
    VAR state: {good, bad};
    ASSIGN
    init(state) := good;
    next(state) := case
        (state = bad) : bad;
        (state = good & cond) : bad;
        (!cond) : good;
        TRUE : state;
        esac;

MODULE main 
    VAR x : singleton;
    VAR y : singleton;
    VAR z : effect((x.state = bad) & (y.state = bad));

But I got only these reachable states

NuSMV > print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 3 (2^1.58496) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    2 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    3 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

How can I modify my code to get also

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

in the reachable states?

In addition, I'm not sure if I've to add or not that red arrow printed in the model picture: if x and y are in state bad, I want that for sure sooner or later also z becomes bad.

Thank you so much for helping!

Patrick Trentin Patrick Trentin · Accepted Answer · 2017-09-25T17:25:52

The states

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

are not reachable because each sub-module of main performs a transition at the same time of the others and because you force a deterministic transition for your state variables; that is, in your model both x and y change state from good to bad at the same time. Moreover, in contrast with your nice picture, your smv code does not allow for any self-loop except for the one on the final state.

To fix your model, you need only to state that --in case x (resp. y) is good-- you want next(x) (resp. next(y)) to be either good or bad, but not force either decision. e.g.

MODULE singleton
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      state = good : { good, bad };
      TRUE         : bad;
    esac;


MODULE effect(cond)
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      (state = bad | cond) : bad;
      TRUE                 : state;
    esac;


MODULE main
VAR
    x : singleton;
    y : singleton;
    z : effect((x.state = bad) & (y.state = bad));

note: i also simplified the rules for module effect, though this was unnecessary.

You can test the model as follows:

nuXmv > reset; read_model -i test.smv ; go; print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 5 (2^2.32193) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = bad
  z.state = good
  ------- State    2 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    3 ------
  x.state = bad
  y.state = good
  z.state = good
  ------- State    4 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    5 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

Regarding your second question, the code sample I provided you guarantees the property you want to verify:

nuXmv > check_ltlspec -p "G ((x.state = bad & y.state = bad) -> F z.state = bad)"
-- specification  G ((x.state = bad & y.state = bad) ->  F z.state = bad)  is true

This is obviously the case because the self-loop outlined by the red edge in your picture is not present. If you think about it, that transition would allow for at least one execution in which the current state remains equal to

x.state = bad
y.state = bad
z.state = good

indefinitely, and this would be a counter-example to your specification.

EDIT:

You can also fix the code by simply writing this:

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = bad) -> next(state) = bad

Removing the line TRANS (state = good) -> next(state) = bad allows x and y to change arbitrarily when state = good, which means they can non-deterministically remain good or become bad. This is completely equivalent to the code I provided you, although less clear at a first glance since it hides non-determinism under the hoods instead of making it explicit.

NuSMV - AND model

1 Answers