[Toss-devel-svn] SF.net SVN: toss:[1647] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
|
From: <luk...@us...> - 2012-01-20 02:32:28
|
Revision: 1647
http://toss.svn.sourceforge.net/toss/?rev=1647&view=rev
Author: lukaszkaiser
Date: 2012-01-20 02:32:20 +0000 (Fri, 20 Jan 2012)
Log Message:
-----------
Learning Pawn-Whopping.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Learn/Distinguish.ml
trunk/Toss/Learn/LearnGame.ml
trunk/Toss/Learn/LearnGameTest.ml
trunk/Toss/Learn/Makefile
trunk/Toss/Learn/examples/Pawn-Whopping001_02.wrg
Added Paths:
-----------
trunk/Toss/Learn/examples/Pawn-Whopping001_03.wrg
trunk/Toss/Learn/examples/Pawn-Whopping001_04.wrg
trunk/Toss/Learn/examples/Pawn-Whopping001_05.nwn
trunk/Toss/Learn/examples/Pawn-Whopping001_05.wrg
trunk/Toss/Learn/examples/Pawn-Whopping001_06.wrg
Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Formula/FormulaOpsTest.ml 2012-01-20 02:32:20 UTC (rev 1647)
@@ -32,6 +32,8 @@
nnf_eq "true" "true";
nnf_eq "(not false)" "true";
nnf_eq "not (P(x) and not Q(x))" "not P(x) or Q(x)";
+ nnf_eq "tc 1 x, y R(x, y)" "x = y or R(x, y)";
+ nnf_eq "tc !1 x, y R(x, y)" "R(x, y)";
nnf_eq "not ex x (not P(x) and Q(x))" "all x (P(x) or not Q(x))";
nnf_eq "not ex :x, :y (:x^2 + 3*:y + 2 < 0)"
"all :x, :y (not :x^2 + 3*:y + 2 < 0)";
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Formula/FormulaParser.mly 2012-01-20 02:32:20 UTC (rev 1647)
@@ -96,7 +96,7 @@
| TC ID COMMA ID formula_expr { FormulaSubst.make_lfp_tc $2 $4 $5 }
| TC IN_MOD ID COMMA ID formula_expr { FormulaSubst.make_mso_tc $3 $5 $6 }
| TC INT ID COMMA ID formula_expr { FormulaSubst.make_fo_tc_conj $2 $3 $5 $6 }
- | TC PLUS INT ID COMMA ID formula_expr
+ | TC NOT INT ID COMMA ID formula_expr
{ FormulaSubst.make_fo_tc_disj ~reflexive:false $3 $4 $6 $7 }
| LFP ID OPEN fo_var_list CLOSE EQ formula_expr
{ let vs = Array.of_list $4 in if Array.length vs <> 1 then
Modified: trunk/Toss/Learn/Distinguish.ml
===================================================================
--- trunk/Toss/Learn/Distinguish.ml 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Learn/Distinguish.ml 2012-01-20 02:32:20 UTC (rev 1647)
@@ -188,6 +188,7 @@
List.map Array.of_list (Aux.all_ntuples (Array.to_list tup) k) in
let ktups = List.rev_map k_subtuples (Aux.unique_sorted tups) in
let ktups = Aux.unique_sorted (List.concat ktups) in
+ if !debug_level>0 then print_endline "guarded_types:\t\t tuples generated";
let mem = Hashtbl.create 63 in
Aux.unique_sorted (List.rev_map
(guarded_type_memo existential struc mem qr) ktups)
@@ -211,6 +212,8 @@
let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in
let atoms = Array.of_list (FormulaOps.atoms ~repetitions:repeat_vars
(Structure.rel_signature struc) (varnames 2)) in
+ if !debug_level > 0 then
+ Printf.printf "tc_atomic:\t\t %i atoms\n%!" (Array.length atoms);
let choices = List.rev_map Array.of_list
(if positive then Aux.product (rept (Array.length atoms) [0; 1]) else
Aux.product (rept (Array.length atoms) [0; 1; -1])) in
@@ -258,17 +261,27 @@
(* Helper function: remove atoms from a formula if [cond] is still satisfied.
Note that this is just a greedy heuristic, only And/Or and into Ex/All. *)
let rec greedy_remove ?(pos=false) cond phi =
- let rec greedy_remove_list constructor acc = function
+ if !debug_level > 1 then
+ Printf.printf "greedy_remove:\t\t %s\n%!" (Formula.str phi);
+ let rec greedy_remove_list minimize constructor acc = function
| [] -> acc
| x :: xs ->
let rest = acc @ xs in
- if cond (constructor rest) then greedy_remove_list constructor acc xs else
- let minx = greedy_remove (fun y -> cond (constructor (y :: rest))) x in
- greedy_remove_list constructor (minx::acc) xs in
+ if cond (constructor rest) then
+ greedy_remove_list minimize constructor acc xs
+ else if minimize then
+ let minx = greedy_remove (fun y-> cond (constructor (y :: rest))) x in
+ greedy_remove_list minimize constructor (minx::acc) xs
+ else greedy_remove_list minimize constructor (x::acc) xs in
+ let greedy_remove_lst cons lst =
+ let l = greedy_remove_list false cons [] lst in
+ if !debug_level > 1 then Printf.printf "greedy_remove_lst:\t min %i: %s\n%!"
+ (List.length l) (Formula.str (cons l));
+ greedy_remove_list true cons [] (List.rev l) in
match phi with
- | And fl -> And (greedy_remove_list (fun l -> And l) [] (List.rev fl))
+ | And fl -> And (greedy_remove_lst (fun l -> And l) (List.rev fl))
| Or fl -> if pos then Or fl else
- Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
+ Or (greedy_remove_lst (fun l -> Or l) (List.rev fl))
| Not f -> if pos then Not f else
Not (greedy_remove (fun x -> cond (Not x)) f)
| Ex (vs, f) -> Ex (vs, greedy_remove (fun x -> cond (Ex (vs, x))) f)
@@ -291,9 +304,10 @@
| ExGuardedFO -> guarded_types ~existential:true struc ~qr ~k
| FO -> ntypes struc ~qr ~k
| ExFO -> ntypes ~existential:true struc ~qr ~k in
+ if !debug_level > 0 then print_endline "min_type_omitting:\t types generated";
let ok_types = List.filter (fun f -> not (List.mem f neg_types)) pos_types in
let ok_types = List.sort !compare_types ok_types in
- if ok_types = [] then None else Some (List.hd ok_types)
+ if ok_types = [] then None else Some (Formula.flatten_sort (List.hd ok_types))
(* Find a [logic]-formula with at most [qr] quantifiers and [k] variables
which holds on all [pos_strucs] and on no [neg_strucs]. *)
@@ -304,6 +318,7 @@
| FO -> ntypes s ~qr ~k
| ExFO -> ntypes ~existential:true s ~qr ~k in
let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
+ if !debug_level > 0 then print_endline "distinguish_upto:\t neg types done";
let fails_on_negs f = not (List.exists (fun s-> check s [||] f) neg_strucs) in
let extend_by_pos acc struc =
if check struc [||] (Or acc) then acc else
@@ -313,6 +328,8 @@
let pos_formulas =
try List.fold_left extend_by_pos [] pos_strucs with Not_found -> [] in
let pos_formulas = Aux.unique_sorted ~cmp:!compare_types pos_formulas in
+ if !debug_level > 0 then Printf.printf
+ "distinguish_upto:\t pos_formulas %i\n%!" (List.length pos_formulas);
if pos_formulas = [] then None else
let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_strucs in
let is_ok f = fails_on_negs f && succ_pos [f] in
@@ -330,7 +347,8 @@
(String.concat "\n" (List.map Structure.str s2));
let rec diff qr k =
if qr > k then diff 0 (k+1) else (
- if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
+ if !debug_level > 0 then
+ Printf.printf "distinguish:\t\t qr %i k %i\n%!" qr k;
if qr = 0 then
match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
| Some f -> f | None ->
@@ -340,9 +358,13 @@
else
match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
| Some f ->
- (match distinguish_upto ~logic:ExGuardedFO ~qr ~k s1 s2 with
- | Some g-> if 2*(Formula.size f) < Formula.size g then f else g
- | None -> f)
+ if qr > 1 (* hurry up for large qr *) then f else (
+ if !debug_level > 0 then Printf.printf
+ "distinguish:\t\t guarded found: %s\n%!" (Formula.str f);
+ match distinguish_upto ~logic:ExGuardedFO ~qr ~k s1 s2 with
+ | Some g-> if 2*(Formula.size f) < Formula.size g then f else g
+ | None -> f
+ )
| None -> diff (qr+1) k
) in
let res = diff 0 1 in
Modified: trunk/Toss/Learn/LearnGame.ml
===================================================================
--- trunk/Toss/Learn/LearnGame.ml 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Learn/LearnGame.ml 2012-01-20 02:32:20 UTC (rev 1647)
@@ -20,7 +20,8 @@
(String.concat "\n" (List.map Structure.str winningStates)) ^ "\nNOT\n"^
(String.concat "\n" (List.map Structure.str notWinningStates)));
let res = Distinguish.distinguish winningStates notWinningStates in
- let print_tc (i,f) = Printf.sprintf "(tc+ %i x0 x1 (%s))" i (Formula.str f) in
+ let print_tc (i, f) =
+ Printf.sprintf "(tc !%i x0, x1 (%s))" i (Formula.str f) in
match !Distinguish.distinguish_result_tc with
| None | Some [(1, _)] -> Formula.str (FormulaOps.tnf_fv res)
| Some l -> if not nicetc then Formula.str (FormulaOps.tnf_fv res) else
@@ -81,7 +82,9 @@
let mright = List.filter (fun (l, r, x) -> movecmp x m = 0) moves in
let mark (l, r, _) =
let chg = Aux.unique_sorted (List.map fst (Structure.diff_elems l r)) in
- Structure.add_rels l "chg" (List.map (fun e -> [|e|]) chg) in
+ let mark_el (st, i) e =
+ (Structure.add_rel st ("ch" ^ string_of_int i) [|e|], i+1) in
+ fst (List.fold_left mark_el (l, 1) chg) in
let (good, bad) = (List.map mark mright, List.map mark mwrong) in
if !debug_level > 0 then (
List.iter Structure.print good;
@@ -91,10 +94,10 @@
let pre = Distinguish.distinguish good bad in
if !debug_level > 0 then print_endline (Formula.str pre);
let elems = Aux.range ~from:1 ((Structure.nbr_elems (fst m)) + 1) in
- let eqs = List.map (fun i -> "x = e" ^ (string_of_int i)) elems in
- let let_part = "let chg(x) = " ^ (String.concat " or " eqs) ^ " in " in
+ let let_part i = Printf.sprintf "let ch%i (x) = x = e%i in" i i in
+ let let_all = String.concat " " (List.map let_part elems) in
let phi = FormulaParser.parse_formula Lexer.lex
- (Lexing.from_string (let_part ^ (Formula.str pre))) in
+ (Lexing.from_string (let_all ^ " " ^ (Formula.str pre))) in
(m, FormulaOps.tnf_fv phi)
let learnFromParties ~win0 ~win1 ~notwon ~wrong =
@@ -105,7 +108,7 @@
let win1f = winFormula
(List.map (fun x -> List.hd (List.rev x)) win1)
(List.flatten ((List.map (fun x-> List.tl (List.rev x))
- win1) @ win0 @ notwon)) in
+ win1) @ win0 @ notwon)) in
let fullMoves0 = movesi 0 (win0 @ win1 @ notwon) in
let fullMoves1 = movesi 1 (win0 @ win1 @ notwon) in
@@ -123,7 +126,7 @@
let cmpll l1 l2 = (List.length l2) - (List.length l1) in
let longest = List.hd (List.sort cmpll (win0 @ win1 @ notwon)) in
- let mvlst pre post l = String.concat "; " (List.map (
+ let mvlst pre post l = String.concat "]; [" (List.map (
fun i -> pre ^ (string_of_int i) ^ post) (Aux.range (List.length l))) in
"PLAYERS 1, 2\n" ^
@@ -131,27 +134,26 @@
"REL Win2() = "^ win1f ^ "\n"^
(fst (List.fold_left
(fun (old, i) ((l, r), pre) ->
- (old ^ "\n" ^ "RULE Mv1-" ^ (string_of_int i) ^ ": \n" ^
+ (old ^ "\n" ^ "RULE Mv1r" ^ (string_of_int i) ^ ": \n" ^
(Structure.str l) ^ " -> " ^ (Structure.str r) ^ "\nemb " ^
(String.concat "," (List.map fst (Structure.rel_signature l))) ^
"\npre (" ^ (Formula.str pre) ^ ") and not Win2()"), i+1)
("", 0) moves0)) ^ "\n\n" ^
(fst (List.fold_left
(fun (old, i) ((l, r), pre) ->
- (old ^ "\n" ^ "RULE Mv2-" ^ (string_of_int i) ^ ": \n" ^
+ (old ^ "\n" ^ "RULE Mv2r" ^ (string_of_int i) ^ ": \n" ^
(Structure.str l) ^ " -> " ^ (Structure.str r) ^ "\nemb "^
(String.concat "," (List.map fst (Structure.rel_signature l))) ^
"\npre (" ^ (Formula.str pre) ^ ") and not Win1()"), i+1)
("",0) moves1)) ^ "\n\n" ^
"LOC 0 {
PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
- MOVES [" ^ (mvlst "Mv1-" " -> 1" moves0) ^ "]}
+ MOVES [" ^ (mvlst "Mv1r" " -> 1" moves0) ^ "]}
PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
}
LOC 1 {
PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
- MOVES [" ^ (mvlst "Mv2-" " -> 0" moves1) ^ "] }
+ MOVES [" ^ (mvlst "Mv2r" " -> 0" moves1) ^ "]}
}" ^ "\n" ^
"MODEL "^(Structure.str (List.hd longest))
-
Modified: trunk/Toss/Learn/LearnGameTest.ml
===================================================================
--- trunk/Toss/Learn/LearnGameTest.ml 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Learn/LearnGameTest.ml 2012-01-20 02:32:20 UTC (rev 1647)
@@ -6,7 +6,7 @@
let struc_of_string ?(diag=false) s =
if diag then
let s = "MODEL " ^ s ^ " with Da (x, y) = ex u (R(x, u) and C(u, y));" ^
- " Db (x, y) = ex u (R(x, u) and C(y, u))" in
+ " Db (x, y) = ex u (C(x, u) and R(y, u))" in
match ArenaParser.parse_game_defs Lexer.lex (Lexing.from_string s) with
| Arena.StateStruc struc -> struc
| _ -> failwith "LearnGameTest:struc_of_string: not a structure"
Modified: trunk/Toss/Learn/Makefile
===================================================================
--- trunk/Toss/Learn/Makefile 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Learn/Makefile 2012-01-20 02:32:20 UTC (rev 1647)
@@ -21,15 +21,15 @@
%.learn:
make -C .. Learn/LearnGameTest.native
- ../LearnGameTest.native -f $(basename $@)
+ time ../LearnGameTest.native -f $(basename $@) > $(basename $@).toss
learntests:
make Tic-Tac-Toe001.learn
make Tic-Tac-Toe002.learn
- #make Breakthrough001.learn
+ make Breakthrough001.learn
make Gomoku001.learn
make Connect4001.learn
- make Pawn-Whopping001.learn
+ #make Pawn-Whopping001.learn
.PHONY: clean
Modified: trunk/Toss/Learn/examples/Pawn-Whopping001_02.wrg
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_02.wrg 2012-01-19 03:06:07 UTC (rev 1646)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_02.wrg 2012-01-20 02:32:20 UTC (rev 1647)
@@ -9,11 +9,11 @@
... ... ... ...
... ... ... ...
... ... ... ...
- ... ... ... ...
+ ... W.. ... ...
... ... ... ...
-... ...W ... ...
+... ... ... ...
... ... ... ...
- ... ... ... ...
+ ... W.. ... ...
... ... ... ...
... ... ... ...
@@ -22,15 +22,15 @@
... ... ... ...
... ... ... ...
... ... ... ...
- ... ... ... ...
+ ... W.. ... ...
... ... ... ...
-... ...W ... ...
+... ... ... ...
... ... ... ...
... ... ... ...
... ... ... ...
... ... ... ...
... ... ... ...
- ... ... ... ...
+ ... W.. ... ...
... ... ... ...
... ... ... ...
Added: trunk/Toss/Learn/examples/Pawn-Whopping001_03.wrg
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_03.wrg (rev 0)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_03.wrg 2012-01-20 02:32:20 UTC (rev 1647)
@@ -0,0 +1,36 @@
+[ | B:1 {}; W:1 {} | ]
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... B.. ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
Added: trunk/Toss/Learn/examples/Pawn-Whopping001_04.wrg
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_04.wrg (rev 0)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_04.wrg 2012-01-20 02:32:20 UTC (rev 1647)
@@ -0,0 +1,36 @@
+[ | B:1 {}; W:1 {} | ]
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
Added: trunk/Toss/Learn/examples/Pawn-Whopping001_05.nwn
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_05.nwn (rev 0)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_05.nwn 2012-01-20 02:32:20 UTC (rev 1647)
@@ -0,0 +1,53 @@
+[ | B:1 {}; W:1 {} | ]
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... W..
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
Added: trunk/Toss/Learn/examples/Pawn-Whopping001_05.wrg
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_05.wrg (rev 0)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_05.wrg 2012-01-20 02:32:20 UTC (rev 1647)
@@ -0,0 +1,36 @@
+[ | B:1 {}; W:1 {} | ]
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... W.. ... ...
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... W.. ...
+... ... ... ...
+... ... ... ..
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
Added: trunk/Toss/Learn/examples/Pawn-Whopping001_06.wrg
===================================================================
--- trunk/Toss/Learn/examples/Pawn-Whopping001_06.wrg (rev 0)
+++ trunk/Toss/Learn/examples/Pawn-Whopping001_06.wrg 2012-01-20 02:32:20 UTC (rev 1647)
@@ -0,0 +1,36 @@
+[ | B:1 {}; W:1 {} | ]
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ...B ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+...B ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...W
+ ... ... ... ...
+ ... ... ... ...
+... ... ... ...
+... ... ... ...
+
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|