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