1(*****************************************************************************) 2(* Game of Solitaire (example from Bill Roscoe, but suggested by Tony Hoare) *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* State variable numbering: *) 7(* *) 8(* ---------------- *) 9(* | 07 | 14 | 21 | *) 10(* ---------------- *) 11(* | 08 | 15 | 22 | *) 12(* ------------------------------------ *) 13(* | 01 | 04 | 09 | 16 | 23 | 28 | 31 | *) 14(* ------------------------------------ *) 15(* | 02 | 05 | 10 | 17 | 24 | 29 | 32 | *) 16(* ------------------------------------ *) 17(* | 03 | 06 | 11 | 18 | 25 | 30 | 33 | *) 18(* ------------------------------------ *) 19(* | 12 | 19 | 26 | *) 20(* ---------------- *) 21(* | 13 | 20 | 27 | *) 22(* ---------------- *) 23(* *) 24(*****************************************************************************) 25 26(* 27load "HolBddLib"; 28load "PrimitiveBddRules"; 29load "ListPair"; 30*) 31 32open HolKernel Parse boolLib; 33infixr 3 -->; 34infix 9 by; 35infix ++; 36infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 37 38 39open HolBddLib; 40open pairSyntax; 41open bossLib; 42 43val _ = (Globals.priming := SOME ""); 44 45val _ = new_theory "Solitaire"; 46 47val var_list as 48 [v01,v02,v03,v04,v05,v06,v07,v08,v09,v10, 49 v11,v12,v13,v14,v15,v16,v17,v18,v19,v20, 50 v21,v22,v23,v24,v25,v26,v27,v28,v29,v30, 51 v31,v32,v33] = 52 ["v01","v02","v03","v04","v05", 53 "v06","v07","v08","v09","v10", 54 "v11","v12","v13","v14","v15", 55 "v16","v17","v18","v19","v20", 56 "v21","v22","v23","v24","v25", 57 "v26","v27","v28","v29","v30", 58 "v31","v32","v33"]; 59 60val var_list' as 61 [v01',v02',v03',v04',v05',v06',v07',v08',v09',v10', 62 v11',v12',v13',v14',v15',v16',v17',v18',v19',v20', 63 v21',v22',v23',v24',v25',v26',v27',v28',v29',v30', 64 v31',v32',v33'] = 65 map (fn v => v^"'") var_list; 66 67(*****************************************************************************) 68(* Make boolean variables (unprimed and primed) *) 69(*****************************************************************************) 70 71fun mk_bool_var s = mk_var(s,bool) 72and mk_primed_bool_var s = mk_bool_var(s^"'"); 73 74(*****************************************************************************) 75(* Good variable order is V01 < v01' < v02 < v02' ... *) 76(* Function shuffle below used to create it *) 77(*****************************************************************************) 78 79fun shuffle (l1,l2) = 80 ListPair.foldr (fn(x1,x2,l) => x1 :: x2 :: l) [] (l1,l2); 81 82val solitaire_varmap = 83 extendVarmap (map mk_bool_var (shuffle(var_list,var_list'))) empty; 84 85(*****************************************************************************) 86(* State vectors *) 87(*****************************************************************************) 88 89val st = list_mk_pair (map mk_bool_var var_list) 90and st' = list_mk_pair (map mk_bool_var var_list'); 91 92(*****************************************************************************) 93(* Initial state *) 94(*****************************************************************************) 95 96val SolitaireInit_def = 97 Define 98 `SolitaireInit ^st = 99 ^(list_mk_conj(map (fn v => if v="v17" then mk_neg(mk_bool_var v) 100 else mk_bool_var v) var_list))`; 101 102(*****************************************************************************) 103(* Final goal state *) 104(*****************************************************************************) 105 106val SolitaireFinal_def = 107 Define 108 `SolitaireFinal ^st = 109 ^(list_mk_conj 110 (map (fn v => if v="v17" then mk_bool_var v 111 else mk_neg(mk_bool_var v)) var_list))`; 112 113(*****************************************************************************) 114(* Function to create a formula to represent a move in which a counter at v1 *) 115(* jumps over and takes one at v2 and lands at v3, which must have been *) 116(* unoccupied. *) 117(*****************************************************************************) 118 119fun make_move_trans (v1,v2,v3) = 120 let val (_,unchanged) = List.partition (fn v => mem v [v1,v2,v3]) var_list 121 in 122 list_mk_conj 123 ([mk_bool_var v1, mk_bool_var v2, mk_neg(mk_bool_var v3), 124 mk_neg(mk_primed_bool_var v1), mk_neg(mk_primed_bool_var v2), mk_primed_bool_var v3] 125 @ 126 (map (fn v => mk_eq(mk_primed_bool_var v,mk_bool_var v)) unchanged)) 127 end; 128 129(*****************************************************************************) 130(* List of all possible moves *) 131(*****************************************************************************) 132 133val moves = 134 [(v01,v04,v09), (v01,v02,v03), 135 (v02,v05,v10), 136 (v03,v02,v01), (v03,v06,v11), 137 (v04,v05,v06), (v04,v09,v16), 138 (v05,v10,v17), 139 (v06,v05,v04), (v06,v11,v18), 140 (v07,v08,v09), (v07,v14,v21), 141 (v08,v09,v10), (v08,v15,v22), 142 (v09,v08,v07), (v09,v10,v11), (v09,v04,v01), (v09,v16,v23), 143 (v10,v09,v08), (v10,v11,v12), (v10,v05,v02), (v10,v17,v24), 144 (v11,v10,v09), (v11,v12,v13), (v11,v06,v03), (v11,v18,v25), 145 (v12,v11,v10), (v12,v19,v26), 146 (v13,v12,v11), (v13,v20,v27), 147 (v14,v15,v16), 148 (v15,v16,v17), 149 (v16,v15,v14), (v16,v17,v18), (v16,v09,v04), (v16,v23,v28), 150 (v17,v16,v15), (v17,v18,v19), (v17,v10,v05), (v17,v24,v29), 151 (v18,v17,v16), (v18,v19,v20), (v18,v11,v06), (v18,v25,v30), 152 (v19,v18,v17), 153 (v20,v19,v18), 154 (v21,v22,v23), (v21,v14,v07), 155 (v22,v23,v24), (v22,v15,v08), 156 (v23,v22,v21), (v23,v24,v25), (v23,v16,v09), (v23,v28,v31), 157 (v24,v23,v22), (v24,v25,v26), (v24,v17,v10), (v24,v29,v32), 158 (v25,v24,v23), (v25,v26,v27), (v25,v18,v11), (v25,v30,v33), 159 (v26,v25,v24), (v26,v19,v12), 160 (v27,v26,v25), (v27,v20,v13), 161 (v28,v29,v30), (v28,v23,v16), 162 (v29,v24,v17), 163 (v30,v29,v28), (v30,v25,v18), 164 (v31,v32,v33), (v31,v28,v23), 165 (v32,v29,v24), 166 (v33,v32,v31), (v33,v30,v25)]; 167 168(*****************************************************************************) 169(* Define transition relation as disjunction of all moves *) 170(*****************************************************************************) 171 172val SolitaireTrans_def = 173 Define 174 `SolitaireTrans(^st,^st') = ^(list_mk_disj(map make_move_trans moves))`; 175 176val (initth,transthl,finalth) = 177 time 178 (findTrace solitaire_varmap SolitaireTrans_def SolitaireInit_def) 179 SolitaireFinal_def; 180 181(* 182val trace_list = ref[]; 183 184fun report n tb = 185 (trace_list := append (!trace_list) [tb]; print "Iteration: "; print (Int.toString n); 186 print " Node size: "; print(Int.toString(bdd.nodecount(getBdd tb))); print "\n"); 187 188val (in_th0,in_thsuc) = 189 time 190 (REWRITE_RULE[SolitaireInit_def] ## REWRITE_RULE[SolitaireTrans_def]) 191 (MkIterThms 192 MachineTransitionTheory.ReachBy_rec 193 (lhs(concl(SPEC_ALL SolitaireTrans_def))) 194 (lhs(concl(SPEC_ALL SolitaireInit_def)))); 195 196val (tb,tb') = time (computeFixedpoint report solitaire_varmap) (in_th0,in_thsuc); 197 198val (in_th0,in_thsuc) = 199 time 200 (REWRITE_RULE[SolitaireInit_def] ## 201 simpLib.SIMP_RULE boolSimps.bool_ss [SolitaireTrans_def,LEFT_AND_OVER_OR,EXISTS_OR_THM]) 202 (MkIterThms 203 MachineTransitionTheory.ReachBy_rec 204 (lhs(concl(SPEC_ALL SolitaireTrans_def))) 205 (lhs(concl(SPEC_ALL SolitaireInit_def)))); 206 207val (tb1,tb1') = time (computeFixedpoint report solitaire_varmap) (in_th0,in_thsuc); 208*) 209 210(*****************************************************************************) 211(* Print out a picture of a Solitaire board from a tuple *) 212(* *) 213(* (c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19, *) 214(* (c21,c22,c23,c24,c25,c26,c27,c28,c29,c30,c31,c32,c3) *) 215(* *) 216(* where cij is T or F *) 217(* *) 218(* and the printing is *) 219(* *) 220(* XXX *) 221(* XXX *) 222(* XXXXXXX *) 223(* XXXXXXX *) 224(* XXXXXXX *) 225(* XXX *) 226(* XXX *) 227(*****************************************************************************) 228 229fun PrintState tm = 230 let val cl = strip_pair tm 231 fun p n = if el n cl = ``T`` then print "1" else print "0" 232 fun sp () = print " " 233 fun nl () = print"\n" 234 in 235 (print" ";p 07;p 14;p 21;nl(); 236 print" ";p 08;p 15;p 22;nl(); 237 p 01;p 04;p 09;p 16;p 23;p 28;p 31;nl(); 238 p 02;p 05;p 10;p 17;p 24;p 29;p 32;nl(); 239 p 03;p 06;p 11;p 18;p 25;p 30;p 33;nl(); 240 print" ";p 12;p 19;p 26;nl(); 241 print" ";p 13;p 20;p 22;nl();nl()) 242 end; 243 244(*****************************************************************************) 245(* Print out a trace as found by findTrace *) 246(*****************************************************************************) 247 248val _ = 249 List.map 250 PrintState 251 (List.map (fst o dest_pair o rand o concl) transthl @ [rand(concl finalth)]); 252 253val _ = export_theory(); 254 255 256(* Reachable state with/without disjunctive partitioning 257 258fun computeSimpReachable vm Rth Bth = 259 let val (by_th0,by_thsuc) = 260 (REWRITE_RULE[Bth,pairTheory.PAIR_EQ] ## REWRITE_RULE[Rth]) 261 (MkIterThms 262 MachineTransitionTheory.ReachBy_rec 263 (lhs(concl(SPEC_ALL Rth))) 264 (lhs(concl(SPEC_ALL Bth)))) 265 val _ = print "Starting disjunctive partitioning ...\n" 266 val by_thsuc_simp = time MakeSimpRecThm by_thsuc 267 val _ = print "disjunctive partitioning complete.\n" 268 val _ = print "Computing reachable states ...\n" 269 in 270 time (computeFixedpoint (fn n=>fn tb=>print".") vm) (by_th0,by_thsuc_simp) 271 end; 272 273val SimpReachable = 274 computeSimpReachable solitaire_varmap SolitaireTrans_def SolitaireInit_def; 275 276(* 277Starting disjunctive partitioning ... 278runtime: 1112.520s, gctime: 512.900s, systime: 1.750s. 279disjunctive partitioning complete. 280Computing reachable states ... 281 282*) 283 284fun computeReachable vm Rth Bth = 285 let val (by_th0,by_thsuc) = 286 (REWRITE_RULE[Bth,pairTheory.PAIR_EQ] ## REWRITE_RULE[Rth]) 287 (MkIterThms 288 MachineTransitionTheory.ReachBy_rec 289 (lhs(concl(SPEC_ALL Rth))) 290 (lhs(concl(SPEC_ALL Bth)))) 291 in 292 time (computeFixedpoint (fn n=>fn tb=>print".") vm) (by_th0,by_thsuc) 293 end; 294 295val Reachable = 296 computeSimpReachable solitaire_varmap SolitaireTrans_def SolitaireInit_def; 297 298*) 299