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