model-checkingnusmv

NuSMV - AND model


I'm trying to write the following model in NuSMV

enter image description here

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!


Solution

  • 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.