1 2 3(********************************************************************************************************) 4(* Tic-tac-toe or naughts-and-crosses *) 5(* *) 6(* State vars are m (A has just moved), ui_j (A has claimed grid square (i,j), vi_j (ditto for B) *) 7(* *) 8(* This example is mainly for testing algorithms on an interleaved transition system. It is also the *) 9(* simplest example (other than the mod8 counter toy example). *) 10(* *) 11(********************************************************************************************************) 12 13(* usage example (start hol including the HolCheck/examples directory, using the -I command line option) 14 15val _ = app load ["holCheckLib","ttt"]; 16(*val _ = set_trace "HolCheckDBGLZ" 0; val _ = set_trace "HolCheckDBG" 0; 17val _ = set_trace "HolCheckPRF" 0; val _ = set_trace "HolCheckLZ" 1; *) 18val ttt1 = ttt.makeTTT 1; (* n=1 gives more interesting results. Most props fail for n=3 and can't get traces *) 19val ttt2 = holCheckLib.holCheck ttt1 handle ex => Raise ex; 20val ttt3 = holCheckLib.prove_model ttt2; 21val res = holCheckLib.get_results ttt3; 22 23*) 24 25structure ttt = 26 27struct 28 29local 30 31open Globals HolKernel Parse 32open Array2 ListPair bossLib simpLib Binarymap pairSyntax boolSyntax stringLib 33open ctlTheory ctlSyntax commonTools holCheckLib 34 35in 36 37(* n is size of grid *) 38fun makeTTT n = 39 let 40 val am = Array2.tabulate Array2.RowMajor (n,n,(fn (x,y) => "u"^Int.toString(x)^"_"^Int.toString(y))) 41 val bm = Array2.tabulate Array2.RowMajor (n,n,(fn (x,y) => "v"^Int.toString(x)^"_"^Int.toString(y))) 42 val am' = Array2.array(n,n,"") 43 val bm' = Array2.array(n,n,"") 44 val _ = Array2.copy {src=({base=am,row=0,col=0,nrows=NONE,ncols=NONE}),dst=am',dst_row=0,dst_col=0} 45 val _ = Array2.copy {src=({base=bm,row=0,col=0,nrows=NONE,ncols=NONE}),dst=bm',dst_row=0,dst_col=0} 46 val _ = Array2.modify Array2.RowMajor (fn s => s^"'") am' 47 val _ = Array2.modify Array2.RowMajor (fn s => s^"'") bm' 48 val lam = Array2.fold Array2.RowMajor (fn (h,t) => t@[h]) [] am 49 val lbm = Array2.fold Array2.RowMajor (fn (h,t) => t@[h]) [] bm 50 val lam' = Array2.fold Array2.RowMajor (fn (h,t) => t@[h]) [] am' 51 val lbm' = Array2.fold Array2.RowMajor (fn (h,t) => t@[h]) [] bm' 52 53 (* Good variable order is V01 < v01' < v02 < v02' ... *) 54 (* Function shuffle below used to create it *) 55 56 fun shuffle (l1,l2) = 57 ListPair.foldr (fn(x1,x2,l) => x1 :: x2 :: l) [] (l1,l2); 58 59 val bvm = ["m","m'"]@(shuffle(lam @ lbm, lam' @ lbm')); 60 61 (* Finishing condition *) 62 63 fun bwin pm pl = 64 let 65 val r = List.map (fn x => Vector.foldr (fn (h,t) => h::t) [] (Array2.row(pm,x))) (List.tabulate (n, (fn x => x))) 66 val c = List.map (fn x => Vector.foldr (fn (h,t) => h::t) [] (Array2.column(pm,x))) (List.tabulate (n, (fn x => x))) 67 val d1 = List.foldr (fn ((h1,h2),t) => if h1=h2 then h1::t else t) [] 68 (ListPair.zip((List.foldr (fn (h,t) => h @ t) [] r), 69 (List.foldr (fn (h,t) => h @ t) [] c))) 70 val d2 = List.foldr (fn ((h1,h2),t) => if h1=h2 then h1::t else t) [] 71 (ListPair.zip((List.foldr (fn (h,t) => h @ t) [] r), 72 (List.rev(List.foldr (fn (h,t) => h @ t) [] c)))) 73 val aps = List.map (fn l => List.map (fn v => mk_bool_var v) l) (d1::d2::(r @ c)) 74 val wn = list_mk_disj (List.map list_mk_conj aps) 75 val mv = if (pl=0) then (mk_neg(mk_bool_var "m")) else (mk_bool_var "m"); 76 in 77 mk_conj(mv, wn) 78 end; 79 80 (* Note: fin is used only in making the moves. A draw is accounted for automatically because no moves are available *) 81 val fin = mk_disj(bwin am 0,bwin bm 1); 82 83 (* Initial state *) 84 85 val I1 = list_mk_conj(List.map (fn v => if v="m" then (mk_bool_var v) else mk_neg(mk_bool_var v)) (lam @ lbm @ ["m"])) 86 87 (* Function to create a relation to represent a move in which a 'o' or an 'x' *) 88 (* is placed at x which must have been unoccupied *) 89 fun make_move_trans (x) = 90 let 91 val (_,unchanged) = List.partition (fn v => mem v [x]) (lam @ lbm); 92 val cp = if (String.compare(String.substring(x,0,1),"u")=EQUAL) 93 then (String.concat ["v", String.substring(x,1,String.size(x)-1)]) 94 else (String.concat ["u", String.substring(x,1,String.size(x)-1)]) 95 in 96 list_mk_conj 97 ([mk_neg(mk_bool_var x), 98 mk_neg(mk_bool_var cp), 99 (if (mem x lam) then mk_bool_var "m" else mk_neg(mk_bool_var "m")), 100 mk_neg(fin), 101 mk_primed_bool_var x, 102 (if (mem x lam) then mk_neg(mk_primed_bool_var "m") else mk_primed_bool_var "m")] 103 @ 104 (List.map (fn v => mk_eq(mk_primed_bool_var v,mk_bool_var v)) unchanged)) 105 end; 106 107 (* List of all possible moves *) 108 val moves = lam @ lbm; 109 110 (* Define transition relation as disjunction of all moves *) 111 (*val R1 = list_mk_disj(List.map make_move_trans moves)*) 112 val T1 = List.map (fn v => (v,(make_move_trans v))) moves; 113 114 (* Properties for players A and B, as ctl formulae *) 115 infixr 5 C_AND infixr 5 C_OR infixr 2 C_IMP infix C_IFF; 116 val state = mk_state I1 T1 117 fun ttt_AP s = C_AP state (mk_bool_var s) 118 fun win pm pl = 119 let 120 val r = List.map (fn x => Vector.foldr (fn (h,t) => h::t) [] (Array2.row(pm,x))) (List.tabulate (n, (fn x => x))) 121 val c = List.map (fn x => Vector.foldr (fn (h,t) => h::t) [] (Array2.column(pm,x))) (List.tabulate (n, (fn x => x))) 122 val d1 = List.foldr (fn ((h1,h2),t) => if h1=h2 then h1::t else t) [] 123 (ListPair.zip((List.foldr (fn (h,t) => h @ t) [] r),(List.foldr (fn (h,t) => h @ t) [] c))) 124 val d2 = List.foldr (fn ((h1,h2),t) => if h1=h2 then h1::t else t) [] 125 (ListPair.zip((List.foldr (fn (h,t) => h @ t) [] r),(List.rev(List.foldr (fn (h,t) => h @ t) [] c)))) 126 val aps = List.map (fn l => List.map (fn v => ttt_AP v) l) (d1::d2::(r @ c)) 127 val wn = list_C_OR (List.map list_C_AND aps) 128 val mv = if (pl=0) then C_NOT(ttt_AP "m") else ttt_AP "m"; 129 in 130 mv C_AND wn 131 end; 132 133 (* pl has a winning strategy if there exists a path from the current position such that either pl has already won, 134 or, it is pl's move and there exists a path to a win, or, it is not pl's move but in all paths pl wins *) 135 fun can_win pm pl = 136 let 137 val pl_won = win pm pl 138 val pl_mv = if pl=0 then ttt_AP "m" else C_NOT(ttt_AP "m") 139 in C_EG (pl_won C_OR ((pl_mv C_AND (C_EF pl_won)) C_OR ((C_NOT pl_mv) C_AND (C_AF pl_won)))) end 140 141 val isInit = list_C_AND (List.map (fn v => if v = "m" then ttt_AP "m" else C_NOT(ttt_AP v)) (lam @ lbm @ ["m"])) 142 143 val A_win = win am 0; (* a win position for A *) 144 145 val A_can_win = can_win am 0; (* A has a winning strategy *) 146 147 val B_win = win bm 1; (* a win position for B *) 148 149 val B_can_win = can_win bm 1 (* B has a winning strategy *) 150 151 val fl =[("isInit",isInit),("A_win",A_win),("B_win",B_win),("A_canwin",A_can_win),("B_can_win",B_can_win)] 152 (* this is for testing what holCheck does if supplied with both mu and CTL forumlas 153 val fl' = [("muisInit",ctl2muTools.ctl2mu ((snd o hd) fl))]@fl@ 154 [("muAcw",ctl2muTools.ctl2mu ((snd o last o butlast) fl))]*) 155 in 156 ((set_init I1) o (set_trans T1) o (set_flag_ric false) o (set_name "ttt") o (set_vord bvm)o (set_state state) o 157 (set_props fl)) empty_model 158 end 159 160end 161end 162