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