holCheckLib.holCheck

We choose a mod-8 counter as our example, which starts at 0 and counts up to 7, and then loops from 0 again. We wish to show that the most significant bit eventually goes high.

1. Load the HolCheck library:

- load "holCheckLib"; open holCheckLib; (* we don't show the output from the "open" here *)
> val it = () : unit

2. Specify the labelled transition system as a list of (string, term) pairs, where each string is a transition label and each term represents a transition relation (three booleans required to encode numbers 0-7; next-state variable values indicated by priming; note we expand the xor, since HolCheck requires purely propositional terms) :

- val xor_def = Define `xor x y = (x \/ y) /\ ~(x=y)`;
  val TS = List.map (I ## (rhs o concl o (fn tm => REWRITE_CONV [xor_def] tm handle ex => REFL tm))) 
				  [("v0",``(v0'=~v0)``),("v1",``v1' = xor v0 v1``),("v2",``v2' = xor (v0 /\ v1) v2``)]
Definition has been stored under "xor_def".
> val xor_def = |- !x y. xor x y = (x \/ y) /\ ~(x = y) : thm
> val TS =
    [("v0", ``v0' = ~v0``), ("v1", ``v1' = (v0 \/ v1) /\ ~(v0 = v1)``),
     ("v2", ``v2' = (v0 /\ v1 \/ v2) /\ ~(v0 /\ v1 = v2)``)] :
  (string * term) list

3. Specify the initial states (counter starts at 0):

- val S0 = ``~v0 /\ ~v1 /\ ~v2``; 
> val S0 = ``~v0 /\ ~v1 /\ ~v2`` : term

4. Specify whether the transitions happen synchronously (it does):

- val ric = true;
> val ric = true : bool

5. Set up the state tuple:

- val state = mk_state S0 TS;
> val state = ``(v0,v1,v2)`` : term

6. Specify a property (there exists a future in which the most significant bit will go high) :

- val ctlf = ("ef_msb_high",``C_EF (C_BOOL (B_PROP ^(pairSyntax.mk_pabs(state,``v2:bool``))))``);
> val ctlf = ("ef_msb_high",``C_EF (C_BOOL (B_PROP (\(v0,v1,v2). v2))``) : string * term

Note how atomic propositions are represented as functions on the state.

7. Create the model:

- val m = ((set_init S0) o (set_trans TS) o (set_flag_ric ric) o (set_state state) o  (set_props [ctlf])) empty_model;
> val m = <model> : model

8. Call the model checker:

- val m2 = holCheck m;
> val m2 = model : <model>

9. Examine the results:

- get_results m2; 
> val it =
    SOME [(<term_bdd>,
           SOME [............................]
               |- CTL_MODEL_SAT ctlKS (C_EF (C_BOOL (B_PROP (\(v0,v1,v2). v2)))),
           SOME [``(~v0,~v1,~v2)``, ``(v0,~v1,~v2)``, ``(~v0,v1,~v2)``,
                 ``(v0,v1,~v2)``, ``(~v0,~v1,v2)``])] :
  (term_bdd * thm option * term list option) list option

The result is a list of triples, one triple per property checked. The first component contains the BDD representation of the set of states satisfying the property. The second component contains a theorem certifying that the property holds in the model i.e. it holds in the initial states. The third contains a witness trace that counts up to 4, at which point v2 goes high.

Note that since we did not supply a name for the model (via holCheckLib.set_name), the system has chosen the default name ctlKS, which stands for "CTL Kripke structure", since models are internally represented formally as Kripke structures.

10. Verify the proof:

- val m3 = prove_model m2; (* we don't show the prove_model "chatting" messages here *)
> val m3 = <model> : model

11. Examine the verified results:

- get_results m3;
> val it =
    SOME [(<term_bdd>,
           SOME|- CTL_MODEL_SAT ctlKS (C_EF (C_BOOL (B_PROP (\(v0,v1,v2). v2)))),
           SOME [``(~v0,~v1,~v2)``, ``(v0,~v1,~v2)``, ``(~v0,v1,~v2)``,
                 ``(v0,v1,~v2)``, ``(~v0,~v1,v2)``])] :
  (term_bdd * thm option * term list option) list option

Note that the theorem component now has no assumptions. Any assumptions to the term_bdd would also have been discharged.