holCheck : model -> model
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.