Model checking of invariants

The key question now is: how can we automatically verify that an invariant I holds? The answer is very simple. Assuming that $\mathcal{R} = (\Sigma,E,\phi,R)$ satisfies reasonable executability conditions, namely, that $E$ and $R$ are finite sets, $(\Sigma, E)$ is ground Church-Rosser and terminating,^9.1 and the rules $R$ are ground coherent with $E$, and assuming, further, that all the conditions for rules in $R$ are purely equational, then $I$ holds if and only if the search command

  search init =>* x:k such that I(x:k) =/= true .

has no solutions. Indeed, having no solutions exactly means that on init, and on all states reachable from it, the predicate I evaluates to true, that is, that I is an invariant. Assuming that I has been fully defined in all cases (which is always easy with the owise feature, described in Section 4.5.4), so that it always evaluates to either true or false, we could instead give the command

  search init =>* x:k such that not I(x:k) .

Consider, for example, a simple clock that marks the hours of the day. Such a clock can be specified with the system module

  mod SIMPLE-CLOCK is 
    protecting INT .
    sort Clock .
    op clock : Int -> Clock [ctor] .
    var T : Int .
    rl clock(T) => clock((T + 1) rem 24) .
  endm

A natural initial state is the state clock(0). Note that, in principle, the clock could be in an infinite number of states, such as clock(7633157) or clock(-33457129). The point, however, is that if our initial state is clock(0), then only states clock(T) with times T such that 0 <= T < 24 can be reached. This suggests making the predicate 0 <= T < 24 an invariant of our clock system.

Using simple linear arithmetic reasoning, we can express the negation of such an invariant as the predicate (T < 0) or (T >= 24); thus, we can automatically verify that our simple clock satisfies the invariant by giving the command:

  Maude> search in SIMPLE-CLOCK : clock(0) =>* clock(T)
           such that T < 0 or T >= 24 .

  No solution.
  states: 24  rewrites: 216 in 0ms cpu (2ms real) (~ rews/sec)

If, as it is the case in this clock example, the number of states reachable from the initial state is finite, then search commands of this kind provide a decision procedure for the satisfaction of invariants. That is, in finite time Maude will either find no solutions to a search for a state violating the invariant, or will find a state violating the invariant together with a sequence of rewrites from the initial state to it, that is, a counterexample.

But what if the number of states reachable from the initial state is infinite? In such a case, if the invariant I is violated, the search command will terminate in finite time yielding a counterexample. Termination is guaranteed by the breadth-first nature of the search. The point is that such a counterexample is a reachable state; therefore, there is a finite sequence of rewrites from the initial state to such a violating state. Since there is only a finite number of rules $R$, and therefore a finite number of ways that each state can be rewritten, even though the number of reachable states is infinite, the number of states reachable from the initial state by a sequence of rewrites of length less than a given bound is always finite. This bounded subset is always explored in finite time by the search command. This means that, for systems where the set of reachable states is infinite, search becomes a semi-decision procedure for detecting the violation of an invariant. That is, if the invariant is violated, we are guaranteed to get a counterexample; but, if it is not violated, we will search forever, never finding it.

We can illustrate the semi-decision procedure nature of search for the verification of invariant failures with a simple infinite-state example of processes and resources. This example has some similarities with the classical dining philosophers problem, but it is on the one hand simpler (processes and resources have no identities or topology), and on the other hand more complex, since the number of processes and resources can grow dynamically in an unbounded manner.

  mod PROCS-RESOURCES is 
    sorts State Resources Process .
    subsorts Process Resources < State .
    ops res null : -> Resources [ctor] .
    op p : Resources -> Process [ctor] .
    op __ : Resources Resources -> Resources 
         [ctor assoc comm id: null] .
    op __ : State State -> State [ctor ditto] .
        
    rl [acq1] : p(null) res => p(res) .
    rl [acq2] : p(res) res => p(res res) .
    rl [rel] : p(res res) => p(null) res res .
    rl [dupl] : p(null) res => p(null) res p(null) res .
  endm

The state is a soup (multiset) of processes and resources. Each process needs to acquire two resources. Originally, each process p contains the null state; but if a resource res is available, it can acquire it (rule [acq1]). If a second resource becomes available, it can also acquire it (rule [acq2]). After acquiring both resources and using them, the process can release them (rule [rel]). Furthermore, the number of processes and resources can grow in an unbounded manner by the duplication of each process-resource pair (rule [dupl]).

One invariant we might like to verify about this system is deadlock freedom. There are two ways to model check this property: one completely straightforward, and another requiring some extra work. The straightforward manner is to give the search command

  Maude> search in PROCS-RESOURCES : res p(null) =>! X:State .

  Solution 1 (state 1)
  states: 3  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  X:State --> p(res)

  Solution 2 (state 5)
  states: 9  rewrites: 9 in 0ms cpu (1ms real) (~ rews/sec)
  X:State --> p(res) p(res)

  Solution 3 (state 13)
  states: 19  rewrites: 26 in 0ms cpu (3ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res)

  Solution 4 (state 25)
  states: 34  rewrites: 56 in 0ms cpu (4ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res) p(res)

  Solution 5 (state 43)
  states: 55  rewrites: 104 in 0ms cpu (23ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res) p(res) p(res)  
  
  ......
  
  Solution 20 (state 1649)
  states: 1770  rewrites: 5640 in 20ms cpu (67ms real) 
    (282000 rews/sec)
  X:State --> p(res) p(res) p(res) p(res) p(res) p(res) p(res) p(res) 
              p(res) p(res) p(res) p(res) p(res) p(res) p(res) p(res) 
              p(res) p(res) p(res) p(res)
  ......

Maude will indeed continue printing all the solutions it finds. But since there is an infinite number of deadlock states, it may be preferable to specify in advance a bound on the number of solutions, giving, for example, a command like the following, that looks for at most 5 solutions.

  Maude> search [5] in PROCS-RESOURCES : res p(null) =>! X:State .

The nice thing about model checking deadlock freedom this way is that there is no need to explicitly specify the invariant as a Boolean predicate. This is because the negation of the invariant is by definition the set of deadlock states, which is what the search command with the =>! qualification precisely looks for.

If one wishes, one can, with a little more work, perform an equivalent model checking of the same property by using an explicit enabledness predicate. Of course, this cannot be done in the original module, because such a predicate has not been defined, but this is easy enough to do:

  mod PROCS-RESOURCES-ENABLED is
    protecting PROCS-RESOURCES .
    protecting BOOL .
    op enabled : State -> Bool .
    eq enabled(p(null) res X:State) = true .
    eq enabled(p(res) res X:State) = true .
    eq enabled(p(res res) X:State) = true .
    eq enabled(X:State) = false [owise] .
  endm

One can then give the command

  Maude> search [5] in PROCS-RESOURCES-ENABLED : res p(null) 
           =>* X:State such that enabled(X:State) =/= true .

getting the following 5 solutions:

  Solution 1 (state 1)
  states: 2  rewrites: 4 in 0ms cpu (0ms real) (~ rews/sec)
  X:State --> p(res)

  Solution 2 (state 5)
  states: 6  rewrites: 15 in 0ms cpu (0ms real) (~ rews/sec)
  X:State --> p(res) p(res)

  Solution 3 (state 13)
  states: 14  rewrites: 41 in 0ms cpu (0ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res)

  Solution 4 (state 25)
  states: 26  rewrites: 87 in 0ms cpu (1ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res) p(res)

  Solution 5 (state 43)
  states: 44  rewrites: 160 in 0ms cpu (1ms real) (~ rews/sec)
  X:State --> p(res) p(res) p(res) p(res) p(res)