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