1
2(*****************************************************************************)
3(* This file first defines a small transistion system                        *)
4(* (HexSolitaire, which I had lying around).                                 *)
5(*                                                                           *)
6(* Next two versions of a mini temporal logic are defined.                   *)
7(*                                                                           *)
8(* Finally there are some rudimentary model checking examples.               *)
9(*****************************************************************************)
10
11(*****************************************************************************)
12(* Simplified game of Solitaire                                              *)
13(*****************************************************************************)
14
15(*****************************************************************************)
16(* State variables                                                           *)
17(*                                                                           *)
18(*               01  02  03                                                  *)
19(*             04  05  06  07                                                *)
20(*           08  09  10  11  12                                              *)
21(*             13  14  15  16                                                *)
22(*               17  18  19                                                  *)
23(*                                                                           *)
24(*****************************************************************************)
25
26(* Comment out for compilation
27load "HolBddLib";
28load "PrimitiveBddRules";
29load "ListPair";
30load "stringLib";
31*)
32
33(* Needed for compilation *)
34open HolKernel Parse boolLib;
35infixr 3 -->;
36infix 9 by;
37infix ++;
38infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;
39
40open bossLib;
41open HolBddLib;
42open bdd;
43open stringLib;
44open pairSyntax;
45open pairTools;
46open pairTheory;
47
48val _ = new_theory "MiniTLHexSolitaire";
49
50(*****************************************************************************)
51(* List of board positions                                                   *)
52(*****************************************************************************)
53
54val vl = [01,02,03,04,05,06,07,08,09,10,11,12,13,14,15,16,17,18,19];
55
56(*****************************************************************************)
57(* Make an unprimed varibale for a board position                            *)
58(*****************************************************************************)
59
60fun mk_v n =
61 if n<10 then mk_var("v0"^(int_to_string n),bool)
62         else mk_var("v"^(int_to_string n),bool);
63
64(*****************************************************************************)
65(* Make a primed varibale for a board position                               *)
66(*****************************************************************************)
67
68fun mk_v' n =
69 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool)
70         else mk_var("v"^(int_to_string n)^"'",bool);
71
72(*****************************************************************************)
73(* Make state vector and primed state vector                                 *)
74(*****************************************************************************)
75
76val s  = list_mk_pair (map mk_v vl)
77and s' = list_mk_pair (map mk_v' vl);
78
79(*****************************************************************************)
80(* Funtion to shuffle unprimed and primed state variables                    *)
81(*****************************************************************************)
82
83fun shuffle (l1,l2) =
84 ListPair.foldr (fn(x1,x2,l) => x1 :: x2 :: l) [] (l1,l2);
85
86(*****************************************************************************)
87(* Varmap (i.e. variable ordering) for later use                             *)
88(*****************************************************************************)
89
90val hexsolitaire_varmap =
91 extendVarmap
92  (map
93    (fn s => mk_var(s,bool))
94    (shuffle(map (fst o dest_var o mk_v) vl, map (fst o dest_var o mk_v') vl)))
95  empty;
96
97(*****************************************************************************)
98(* Make a transition relation term for a single move in which n1 jumps       *)
99(* over (and so removes) n2 into n3                                          *)
100(*****************************************************************************)
101
102fun make_move (n1,n2,n3) =
103 let val (_,unchanged) = List.partition (fn n => mem n [n1,n2,n3]) vl
104 in
105 list_mk_conj
106  ([mk_v n1,mk_v n2,mk_neg(mk_v n3),
107    mk_neg(mk_v' n1),mk_neg(mk_v' n2),mk_v' n3]
108   @
109   (map (fn n => mk_eq(mk_v' n,mk_v n)) unchanged))
110 end;
111
112(*****************************************************************************)
113(* List of posible moves                                                     *)
114(*****************************************************************************)
115
116val moves =
117 [(01,02,03),(01,05,10),(01,04,08),
118  (02,06,11),(02,05,09),
119  (03,07,12),(03,06,10),(03,02,01),
120  (04,05,06),(04,09,14),
121  (05,06,07),(05,10,15),(05,09,13),
122  (06,11,16),(06,10,14),(06,05,04),
123  (07,11,15),(07,06,05),
124  (08,04,01),(08,09,10),(08,13,17),
125  (09,05,02),(09,10,11),(09,14,18),
126  (10,09,08),(10,05,01),(10,06,03),(10,11,12),(10,15,19),(10,14,17),
127  (11,10,09),(11,06,02),(11,15,18),
128  (12,11,10),(12,07,03),(12,16,19),
129  (13,09,05),(13,14,15),
130  (14,09,04),(14,10,06),(14,15,16),
131  (15,14,13),(15,10,05),(15,11,07),
132  (16,15,14),(16,11,06),
133  (17,13,08),(17,14,10),(17,18,19),
134  (18,14,09),(18,15,11),
135  (19,18,17),(19,15,10),(19,16,12)];
136
137(*****************************************************************************)
138(* Make the disjunction of all possible moves (i.e. the transition relation) *)
139(*****************************************************************************)
140
141val HexSolitaireTrans_def =
142  bossLib.Define `HexSolitaireTrans(^s,^s') =
143   ^(list_mk_disj(map make_move moves))`;
144
145(*****************************************************************************)
146(* Final goal state: only positions 10 and 18 filled                         *)
147(*****************************************************************************)
148
149val HexSolitaireFinal_def =
150 bossLib.Define
151  `HexSolitaireFinal ^s =
152     ^(list_mk_conj
153        (map (fn n => if (n=10 orelse n=18)
154                       then mk_v n
155                       else mk_neg(mk_v n)) vl))`;
156
157(*****************************************************************************)
158(* Compute term_bdd of set of states reachable from initial state            *)
159(*                                                                           *)
160(*  (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)                                  *)
161(*                                                                           *)
162(* First compute iteration theorems by_th0 and by_thsuc                      *)
163(*                                                                           *)
164(* Then iterate to a fixed point                                             *)
165(*                                                                           *)
166(* Finally, use ReachBy_fixedpoint to compute ReachTb, the term_bdd of       *)
167(*                                                                           *)
168(*  ``Reachable HexSolitaireTrans                                            *)
169(*     (Eq (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T))                          *)
170(*     (v01,v02,v03,v04,v05,v06,v07,v08,v09,v10,v11,                         *)
171(*      v12,v13,v14,v15,v16,v17,v18,v19)``                                   *)
172(*                                                                           *)
173(*****************************************************************************)
174
175val (by_th0,by_thsuc) =
176 time
177  (REWRITE_RULE[Eq_def,pairTheory.PAIR_EQ] ## REWRITE_RULE[HexSolitaireTrans_def])
178  (MkIterThms
179    MachineTransitionTheory.ReachBy_rec
180    (lhs(concl(SPEC_ALL HexSolitaireTrans_def)))
181    (lhs(concl(ISPECL[``(T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)``,s]Eq_def))));
182
183val (FinalTb,FinalTb') =
184 computeFixedpoint
185  (fn n => fn tb => print ".")
186  hexsolitaire_varmap
187  (by_th0,by_thsuc);
188
189val ReachTb =
190 BddEqMp
191  (SYM
192    (AP_THM
193     (MATCH_MP
194       ReachBy_fixedpoint
195       (EXT
196         (PGEN
197           (mk_var("s",type_of s))
198           s
199           (BddThmOracle(BddOp(Biimp,FinalTb,FinalTb'))))))
200     s))
201  FinalTb;
202
203(*****************************************************************************)
204(* A Mini Temporal Logic                                                     *)
205(*****************************************************************************)
206
207val _ =
208 Hol_datatype
209  `wff = ATOM     of ('state -> bool)
210       | NOT      of wff
211       | AND      of wff => wff
212       | OR       of wff => wff
213       | SOMETIME of wff
214       | ALWAYS   of wff`;
215
216val Eval_def =
217 Define
218  `(Eval (ATOM p)     R s = p s)                                        /\
219   (Eval (NOT f)      R s = ~(Eval f R s))                              /\
220   (Eval (AND f1 f2)  R s = (Eval f1 R s /\ Eval f2 R s))               /\
221   (Eval (OR f1 f2)   R s = (Eval f1 R s \/ Eval f2 R s))               /\
222   (Eval (SOMETIME f) R s = ?s'. Reachable R (Eq s) s' /\  Eval f R s') /\
223   (Eval (ALWAYS f)   R s = !s'. Reachable R (Eq s) s' ==> Eval f R s')`;
224
225(*****************************************************************************)
226(* Compute the term_bdd of                                                   *)
227(*                                                                           *)
228(* ``Eval                                                                    *)
229(*    ^wff                                                                   *)
230(*    HexSolitaireTrans                                                      *)
231(*    (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)``                              *)
232(*****************************************************************************)
233
234fun Check wff =
235 let val th = simpLib.SIMP_CONV
236               std_ss
237               [Eval_def,EXISTS_PROD,FORALL_PROD,HexSolitaireFinal_def]
238               ``Eval
239                  ^wff
240                  HexSolitaireTrans
241                  (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)``
242      val (t1,t2) = dest_eq(concl th)
243      val tb = GenTermToTermBdd (BddApRestrict ReachTb) hexsolitaire_varmap t2
244  in
245   BddEqMp (SYM th) tb
246  end;
247
248(*****************************************************************************)
249(* Some examples                                                             *)
250(*****************************************************************************)
251
252val EvalTb = Check ``(SOMETIME (ATOM HexSolitaireFinal))``;
253
254val wff1 =
255 ``\(v01,v02,v03,v04,v05,v06,v07,v08,v09,v10,v11,v12,v13,v14,v15,v16,v17,v18,v19).
256    ~v01 /\ ~v02 /\ ~v03 /\ ~v04 /\ ~v05 /\ ~v06 /\ ~v07 /\ ~v08 /\
257    ~v09 /\ v10 /\ ~v11 /\ ~v12 /\ ~v13 /\ ~v14 /\ ~v15 /\ ~v16 /\ ~v17 /\ v18 /\ ~v19``;
258
259val EvalTb1 = Check ``(SOMETIME (ATOM ^wff1))``;
260
261val wff2 =
262 ``\(v01,v02,v03,v04,v05,v06,v07,v08,v09,v10,v11,v12,v13,v14,v15,v16,v17,v18,v19).
263    v01 /\ v02 /\ v03 /\ ~v04 /\ ~v05 /\ ~v06 /\ ~v07 /\ ~v08 /\
264    ~v09 /\ ~v10 /\ ~v11 /\ ~v12 /\ ~v13 /\ ~v14 /\ ~v15 /\ ~v16 /\ ~v17 /\ ~v18 /\ ~v19``;
265
266val EvalTb2 = Check ``(SOMETIME (ATOM ^wff2))``;
267
268val wff3 =
269 ``\(v01,v02,v03,v04,v05,v06,v07,v08,v09,v10,v11,v12,v13,v14,v15,v16,v17,v18,v19).
270    ~v01 /\ ~v02 /\ ~v03 /\ ~v04 /\ ~v05 /\ ~v06 /\ ~v07 /\ ~v08 /\
271    ~v09 /\ v10 /\ ~v11 /\ ~v12 /\ ~v13 /\ ~v14 /\ ~v15 /\ ~v16 /\ ~v17 /\ ~v18 /\ ~v19``;
272
273val EvalTb3 = Check ``(SOMETIME (ATOM ^wff3))``;
274
275(*****************************************************************************)
276(* Convert to a HOL theorem                                                  *)
277(*****************************************************************************)
278
279val ModelCheckTh = BddThmOracle EvalTb;
280
281val ModelCheckTh1 = BddThmOracle EvalTb1;
282
283val ModelCheckTh2 = BddThmOracle EvalTb2;
284
285(*
286val ModelCheckTh3 = BddThmOracle EvalTb3;
287*)
288
289
290(*****************************************************************************)
291(* A version of the Mini Temporal Logic with Kripke structures               *)
292(*****************************************************************************)
293
294val _ =
295 Hol_datatype
296  `awff = aATOM     of string
297        | aNOT      of awff
298        | aAND      of awff => awff
299        | aOR       of awff => awff
300        | aSOMETIME of awff
301        | aALWAYS   of awff`;
302
303val aEval_def =
304 Define
305  `(aEval (aATOM a)     (R,L) s = L a s)                                           /\
306   (aEval (aNOT f)      (R,L) s = ~(aEval f (R,L) s))                              /\
307   (aEval (aAND f1 f2)  (R,L) s = (aEval f1 (R,L) s /\ aEval f2 (R,L) s))          /\
308   (aEval (aOR f1 f2)   (R,L) s = (aEval f1 (R,L) s \/ aEval f2 (R,L) s))          /\
309   (aEval (aSOMETIME f) (R,L) s = ?s'. Reachable R (Eq s) s' /\  aEval f (R,L) s') /\
310   (aEval (aALWAYS f)   (R,L) s = !s'. Reachable R (Eq s) s' ==> aEval f (R,L) s')`;
311
312(*****************************************************************************)
313(* Compute the term_bdd of                                                   *)
314(*                                                                           *)
315(* ``aEval                                                                   *)
316(*    ass                                                                    *)
317(*    ^awff                                                                  *)
318(*    (HexSolitaireTrans,^L)                                                 *)
319(*    (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)``                              *)
320(*                                                                           *)
321(* where ass is a list of assumptions that is used in simplification         *)
322(*****************************************************************************)
323
324fun aCheck ass L awff =
325 let val th = simpLib.SIMP_CONV
326               std_ss
327               ([aEval_def,EXISTS_PROD,FORALL_PROD,HexSolitaireFinal_def]
328                @ List.map ASSUME ass)
329               ``aEval
330                  ^awff
331                  (HexSolitaireTrans,^L)
332                  (T,T,T,T,T,T,T,T,T,F,T,T,T,T,T,T,T,T,T)``
333      val (t1,t2) = dest_eq(concl th)
334      val tb = GenTermToTermBdd (BddApRestrict ReachTb) hexsolitaire_varmap t2
335  in
336   BddEqMp (SYM th) tb
337  end;
338
339(*****************************************************************************)
340(* Some examples to illustrate using assumptions                             *)
341(*****************************************************************************)
342
343val aEvalTb =
344 aCheck
345 []
346 ``\a s. if a="HexSolitaireFinal" then HexSolitaireFinal s else F``
347 ``(aSOMETIME (aATOM "HexSolitaireFinal"))``;
348
349val aModelCheckTh = BddThmOracle aEvalTb;
350
351val _ = set_fixity "aAND" (Infixl 500);
352
353(*****************************************************************************)
354(* v01,...,v19 free in finalwff                                              *)
355(*****************************************************************************)
356
357val finalwff =
358 ``aNOT(aATOM v01) aAND aNOT(aATOM v02) aAND aNOT(aATOM v03) aAND
359   aNOT(aATOM v04) aAND aNOT(aATOM v05) aAND aNOT(aATOM v06) aAND
360   aNOT(aATOM v07) aAND aNOT(aATOM v08) aAND aNOT(aATOM v09) aAND
361   aATOM v10 aAND
362   aNOT(aATOM v11) aAND aNOT(aATOM v12) aAND aNOT(aATOM v13) aAND
363   aNOT(aATOM v14) aAND aNOT(aATOM v15) aAND aNOT(aATOM v16) aAND
364   aNOT(aATOM v17) aAND
365   aATOM v18 aAND
366   aNOT(aATOM v19)``;
367
368(*****************************************************************************)
369(* Assume vi equals string "vi" (0 <= i <= 19)                               *)
370(*****************************************************************************)
371
372val var_ass =
373 [``v01 = "v01"``,``v02 = "v02"``,``v03 = "v03"``,``v04 = "v04"``,
374  ``v05 = "v05"``,``v06 = "v06"``,``v07 = "v07"``,``v08 = "v08"``,
375  ``v09 = "v09"``,``v10 = "v10"``,``v11 = "v11"``,``v12 = "v12"``,
376  ``v13 = "v13"``,``v14 = "v14"``,``v15 = "v15"``,``v16 = "v16"``,
377  ``v17 = "v17"``,``v18 = "v18"``,``v19 = "v19"``];
378
379(*****************************************************************************)
380(* Assume L maps "vi" to selector on ith component of state (0 <= i <= 19)   *)
381(*****************************************************************************)
382
383val L_ass =
384 [``!v01 v02 v03 v04 v05 v06 v07 v08 v09 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19.
385    (L"v01" ^s = v01)/\(L"v02" ^s = v02)/\(L"v03" ^s = v03)/\(L"v04" ^s = v04)/\
386    (L"v05" ^s = v05)/\(L"v06" ^s = v06)/\(L"v07" ^s = v07)/\(L"v08" ^s = v08)/\
387    (L"v09" ^s = v09)/\(L"v10" ^s = v10)/\(L"v11" ^s = v11)/\(L"v12" ^s = v12)/\
388    (L"v13" ^s = v13)/\(L"v14" ^s = v14)/\(L"v15" ^s = v15)/\(L"v16" ^s = v16)/\
389    (L"v17" ^s = v17)/\(L"v18" ^s = v18)/\(L"v19" ^s = v19)``];
390
391(*****************************************************************************)
392(* Create a variable ``L`` with appropriate type                             *)
393(*****************************************************************************)
394
395val L = ``L:string->^(ty_antiq(type_of s))->bool``;
396
397(*****************************************************************************)
398(* Example with assumptions about L and vi                                   *)
399(*****************************************************************************)
400
401val aEvalTb2 =
402 aCheck
403 (L_ass @  var_ass)
404 L
405 ``(aSOMETIME ^finalwff)``;
406
407val aModelCheckTh2 = BddThmOracle aEvalTb2;
408
409val _ = export_theory();
410