[Toss-devel-svn] SF.net SVN: toss:[1216] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2010-12-04 13:02:41
|
Revision: 1216 http://toss.svn.sourceforge.net/toss/?rev=1216&view=rev Author: lukstafi Date: 2010-12-04 13:02:34 +0000 (Sat, 04 Dec 2010) Log Message: ----------- Handling of postconditions (not optimized yet for alpha-beta). Loading Chess in GameTest. More diagnostic logging in Heuristic and FFTNF. Modified Paths: -------------- trunk/Toss/Arena/Arena.ml trunk/Toss/Arena/ArenaTest.ml trunk/Toss/Arena/ContinuousRule.ml trunk/Toss/Arena/ContinuousRule.mli trunk/Toss/Arena/ContinuousRuleTest.ml trunk/Toss/Formula/Aux.ml trunk/Toss/Formula/Aux.mli trunk/Toss/Formula/AuxTest.ml trunk/Toss/Play/Game.ml trunk/Toss/Play/GameTest.ml trunk/Toss/Play/Heuristic.ml Modified: trunk/Toss/Arena/Arena.ml =================================================================== --- trunk/Toss/Arena/Arena.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Arena/Arena.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -508,8 +508,8 @@ AddElem loc -> apply_to_loc add_new_elem loc state "add elem" | AddRel (loc, rel, tp) -> - (* FIXME: remove this note if AddRel needs to add new - elements, otherwise simplify *) + (* FIXME: remove this note if AddRel needs to add new + elements, otherwise simplify *) let add_rel struc = let struc, tp = List.fold_right (fun n (struc, tp) -> @@ -799,14 +799,15 @@ let m = List.map (fun (l, s) -> Structure.find_elem lhs_struc l, Structure.find_elem state.struc s) mtch in - let (new_struc, new_time, shifts) = - ContinuousRule.rewrite_single struc state.time m r t p in - let val_str ((f, e), tl) = - let ts t = string_of_float (Term.term_val t) in + match ContinuousRule.rewrite_single struc state.time m r t p with + | Some (new_struc, new_time, shifts) -> + let val_str ((f, e), tl) = + let ts t = string_of_float (Term.term_val t) in (* we've moved to using element names in Term *) - f ^ ", " ^ e ^ ", " ^ (String.concat ", " (List.map ts tl)) in - let shifts_s = String.concat "; " (List.map val_str shifts) in - ({state with struc = new_struc; time = new_time}, shifts_s) + f ^ ", " ^ e ^ ", " ^ (String.concat ", " (List.map ts tl)) in + let shifts_s = String.concat "; " (List.map val_str shifts) in + ({state with struc = new_struc; time = new_time}, shifts_s) + | None -> (state, "ERR applying "^r_name^", postcondition fails") with Not_found -> (state, "ERR applying "^r_name^", rule not found") ) | GetRuleNames -> (state, String.concat "; " (fst (List.split state.game.rules))) Modified: trunk/Toss/Arena/ArenaTest.ml =================================================================== --- trunk/Toss/Arena/ArenaTest.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Arena/ArenaTest.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -113,6 +113,7 @@ "setting states from examples dir" >:: (fun () -> backtrace ( + skip_if true "Change to simpler and stable example."; let fname = "./examples/Breakthrough.toss" in let file = open_in fname in let contents = String.make 4000 '$' in Modified: trunk/Toss/Arena/ContinuousRule.ml =================================================================== --- trunk/Toss/Arena/ContinuousRule.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Arena/ContinuousRule.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -79,8 +79,8 @@ (List.hd ids, List.map List.hd llst) :: (select_pos (List.tl ids) (List.map List.tl llst)) -(* For now, we rewrite only single rules. *) -let rewrite_single struc cur_time m r t params = +(* For now, we rewrite only single rules. Does not check postcondition. *) +let rewrite_single_nocheck struc cur_time m r t params = let time = ref cur_time in let left_elname le = Structure.elem_str r.discrete.DiscreteRule.lhs_struc le in @@ -159,6 +159,26 @@ (res_struc, !time, all_vals_assoc) +(* Matches which satisfy postcondition with time 1 and empty params *) +let matches_post struc r cur_time = + let is_ok m = + let (res_struc, _, _) = + rewrite_single_nocheck struc cur_time m r 1. [] in + SolverIntf.M.check_formula res_struc r.post_pp in + if r.post = Formula.And [] then matches struc r else + List.filter is_ok (matches struc r) + +(* For now, we rewrite only single rules. Returns [None] if rewriting + fails. *) +let rewrite_single struc cur_time m r t params = + let (res_struc, _, _ as res_struc_n_shifts) = + rewrite_single_nocheck struc cur_time m r t params in + if r.post = Formula.And [] || + SolverIntf.M.check_formula res_struc r.post_pp + then Some res_struc_n_shifts + else None + + (* -------------------------- PRINTING FUNCTION ----------------------------- *) (* Print a rule to string. *) @@ -177,16 +197,6 @@ dyn_str ^ upd_str ^ pre_str ^ inv_str ^ post_str -(* Matches which satisfy postcondition with time 1 and empty params *) -let matches_post struc r cur_time = - let is_ok m = - let (res_struc, _, _) = rewrite_single struc cur_time m r 1. [] in - SolverIntf.M.check_formula res_struc r.post_pp in - if r.post = Formula.And [] then matches struc r else - List.filter is_ok (matches struc r) - - - let has_dynamics r = r.dynamics <> [] (* List.exists (fun (_, t) -> t <> Term.Const 0.) r.dynamics *) Modified: trunk/Toss/Arena/ContinuousRule.mli =================================================================== --- trunk/Toss/Arena/ContinuousRule.mli 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Arena/ContinuousRule.mli 2010-12-04 13:02:34 UTC (rev 1216) @@ -73,7 +73,17 @@ starting in [cur_time], at matching [m], and returns the rewritten structure, the time after the rewrite, and shifts (i.e. values for functions supplied with dynamics equations, at each time step). *) +val rewrite_single_nocheck : + Structure.structure -> float -> + (int * int) list -> rule -> float -> (string * float) list -> + Structure.structure * float * ((string * string) * Term.term list) list + +(* For now, we rewrite only single rules. + + Same as {!ContinuousRule.rewrite_single_nocheck}, but check if the + postcondition holds. Returns [None] if rewriting fails. *) val rewrite_single : Structure.structure -> float -> (int * int) list -> rule -> float -> (string * float) list -> - Structure.structure * float * ((string * string) * Term.term list) list + (Structure.structure * + float * ((string * string) * Term.term list) list) option Modified: trunk/Toss/Arena/ContinuousRuleTest.ml =================================================================== --- trunk/Toss/Arena/ContinuousRuleTest.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Arena/ContinuousRuleTest.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -96,7 +96,7 @@ let r = rule_of_str s signat [] in let m = List.hd (matches struc r) in let res, _, _ = - rewrite_single struc 0.0 m r 1. [] in + Aux.unsome (rewrite_single struc 0.0 m r 1. []) in assert_equal ~printer:(fun x->x) "[a | P:1 {}; Q (a); _del_P (a); _new_Q (a) | x {a->0.71}]" (remove_insignificant_digits (Structure.str res)); @@ -116,12 +116,12 @@ let r = rule_of_str s signat [] in let m = List.hd (matches struc r) in let res, _, _ = - rewrite_single struc 0.0 m r 1. [] in + Aux.unsome (rewrite_single struc 0.0 m r 1. []) in assert_equal ~printer:(fun x->x) ~msg:"first rewrite" "[a | P:1 {}; Q (a); _del_P (a); _new_Q (a) | x {a->0.71}]" (remove_insignificant_digits (Structure.str res)); let res, _, _ = - rewrite_single struc 0.0 m r 1. [] in + Aux.unsome (rewrite_single struc 0.0 m r 1. []) in assert_equal ~printer:(fun x->x) ~msg:"second rewrite" "[a | P:1 {}; Q (a); _del_P (a); _new_Q (a) | x {a->0.71}]" (remove_insignificant_digits (Structure.str res)) Modified: trunk/Toss/Formula/Aux.ml =================================================================== --- trunk/Toss/Formula/Aux.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Formula/Aux.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -140,6 +140,24 @@ | _ -> acc in List.rev (aux n [] l) +let array_map_some f a = + let r = Array.map f a in + let rl = ref (Array.length r) in + for i=0 to Array.length a - 1 do + if r.(i) = None then decr rl + done; + if !rl = 0 then [||] + else + let pos = ref 0 in + while r.(!pos) = None do incr pos done; + let res = Array.create !rl (unsome r.(!pos)) in + incr pos; + for i=1 to !rl -1 do + while r.(!pos) = None do incr pos done; + res.(i) <- unsome r.(!pos); incr pos + done; + res + let array_map2 f a b = let l = Array.length a in if l <> Array.length b then @@ -272,6 +290,9 @@ | Left e -> Left (f e) | Right e -> Right (g e) +let map_option f = function None -> None + | Some e -> Some (f e) + let transpose_lists lls = let rec aux acc = function | [] -> List.map List.rev acc Modified: trunk/Toss/Formula/Aux.mli =================================================================== --- trunk/Toss/Formula/Aux.mli 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Formula/Aux.mli 2010-12-04 13:02:34 UTC (rev 1216) @@ -93,6 +93,9 @@ [Invalid_argument "Aux.array_from_assoc"] otherwise. *) val array_from_assoc : (int * 'a) list -> 'a array +(** Map an array filtering out some elements. *) +val array_map_some : ('a -> 'b option) -> 'a array -> 'b array + (** Map a function over two arrays index-wise. Raises [Invalid_argument] if the arrays are of different lengths. *) val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array @@ -140,6 +143,8 @@ val map_choice : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) choice -> ('b, 'd) choice +val map_option : ('a -> 'b) -> 'a option -> 'b option + (** Transpose a rectangular matrix represented by lists. Raises [Invalid_argument "List.map2"] when matrix is not rectangular. *) val transpose_lists : 'a list list -> 'a list list Modified: trunk/Toss/Formula/AuxTest.ml =================================================================== --- trunk/Toss/Formula/AuxTest.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Formula/AuxTest.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -5,7 +5,7 @@ String.concat ", " (List.map (fun (k,v) -> k^": "^f v) l) let tests = "Aux" >::: [ - "concat_map, map_some" >:: + "concat_map, map_some, array_map_some" >:: (fun () -> let f = function `A -> ["a";"b"] | `B -> ["c"] | `C -> [] | `D -> ["d";"e"] in @@ -18,6 +18,12 @@ assert_equal ~printer:(String.concat "; ") ["a";"b";"d"] (Aux.map_some f [`A;`B;`C;`D]); + + let f = function `A -> Some "a" | `B -> Some "b" | `C -> None + | `D -> Some "d" in + assert_equal ~printer:(fun x->String.concat "; "(Array.to_list x)) + [|"a";"b";"d"|] + (Aux.array_map_some f [|`A;`B;`C;`D|]); ); "map_reduce" >:: Modified: trunk/Toss/Play/Game.ml =================================================================== --- trunk/Toss/Play/Game.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Play/Game.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -248,6 +248,12 @@ else None in Array.map (fun node -> Array.map (fun payoff -> + (* {{{ log entry *) + if !debug_level > 3 then ( + Printf.printf "default_hauristic: Computing of payoff %s...\n%!" + (Formula.real_str payoff); + ); + (* }}} *) Heuristic.of_payoff ?struc ?fluent_preconds advance_ratio (Aux.strings_of_list fluents) payoff) node.Arena.payoffs) graph @@ -588,13 +594,14 @@ ) matchings)) let gen_models rules defined_rels model time moves = - Array.map (fun mv -> + Aux.array_map_some (fun mv -> let rule = List.assoc mv.rule rules in - (* ignoring shifts, i.e. animation steps *) - let model, time, _ = - ContinuousRule.rewrite_single model time mv.embedding - rule mv.mv_time mv.parameters in - {loc=mv.next_loc; struc=model; time=time}) moves + Aux.map_option + (fun (model, time, _) -> + (* ignoring shifts, i.e. animation steps *) + {loc=mv.next_loc; struc=model; time=time}) + (ContinuousRule.rewrite_single model time mv.embedding + rule mv.mv_time mv.parameters)) moves let debug_count = ref 0 @@ -648,17 +655,26 @@ let agent = agents.(state.loc) in match agent with | Random_move -> - let pos = Random.int (Array.length moves) in - let mv = moves.(pos) in - let rule = List.assoc mv.rule rules in - let model, time, _ = (* ignoring shifts *) - ContinuousRule.rewrite_single state.struc state.time - mv.embedding rule mv.mv_time mv.parameters in - let state = {loc=mv.next_loc; struc=model; time=time} in + let pos = ref (Random.int (Array.length moves)) in + let nstate = ref None in + while !nstate = None do + pos := (!pos + 1) mod Array.length moves; + let mv = moves.(!pos) in + let rule = List.assoc mv.rule rules in + nstate := + Aux.map_option + (fun (model, time, _) -> + (* ignoring shifts, i.e. animation steps *) + {loc=mv.next_loc; struc=model; time=time}) + (ContinuousRule.rewrite_single state.struc state.time + mv.embedding rule mv.mv_time mv.parameters); + done; + let state = Aux.unsome !nstate in + (* FIXME: [pos] refers to unfiltered array! *) Aux.Left - (pos, moves, memory, + (!pos, moves, memory, {game_state = state; - memory = update_memory ~num_players state pos memory}) + memory = update_memory ~num_players state !pos memory}) | Maximax_evgame (subgames, cooperative, depth, use_pruning, reorder) -> (* {{{ log entry *) @@ -1171,9 +1187,6 @@ (* {{{ log entry *) if !debug_level > 0 then printf "\ninitializing game and play\n%!"; (* }}} *) - (* {{{ log entry *) - if !debug_level > 2 then printf "game initialized\n%!"; - (* }}} *) (* TODO: default_heuristic redoes payoff normalization. *) let game = state.Arena.game in let play = Modified: trunk/Toss/Play/GameTest.ml =================================================================== --- trunk/Toss/Play/GameTest.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Play/GameTest.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -25,9 +25,13 @@ (Lexing.from_string s) let state_of_file s = + Printf.printf "Loading file %s...\n%!" s; let f = open_in s in - ArenaParser.parse_game_state Lexer.lex - (Lexing.from_channel f) + let res = + ArenaParser.parse_game_state Lexer.lex + (Lexing.from_channel f) in + Printf.printf "File %s loaded.\n%!" s; + res module StrMap = Structure.StringMap module IntMap = Structure.IntMap @@ -463,6 +467,9 @@ let breakthrough_heur = breakthrough_heur_adv 1.5 +let chess_game = + 2.0, state_of_file "./examples/Chess.toss" + let check_loc_random = function | Game.Tree_search (_,_,_,evgames) -> if @@ -555,6 +562,22 @@ assert_bool "Game is not over yet -- some move expected." (move_opt <> None) ); + + "play: chess suggest first move" >:: + (fun () -> + todo "Payoff too difficult for heuristic generation."; + let state = chess_game in + Game.set_debug_level 7; + Heuristic.debug_level := 7; + FFTNF.debug_level := 7; + let move_opt = (let p,ps = Game.initialize_default (snd state) + ~heur_adv_ratio:(fst state) + ~loc:0 ~effort:2 + ~search_method:"alpha_beta_ord" () in + Game.suggest p ps) in + assert_bool "Game is not over yet -- some move expected." + (move_opt <> None) + ); "breakthrough payoff" >:: (fun () -> @@ -1085,7 +1108,7 @@ let a () = match test_filter - ["Game:1:alpha_beta_ord:10:breakthrough suggest depth"] + ["Game:0:misc:0:play: chess suggest first move"] tests with | Some tests -> ignore (run_test_tt ~verbose:true tests) Modified: trunk/Toss/Play/Heuristic.ml =================================================================== --- trunk/Toss/Play/Heuristic.ml 2010-12-04 01:59:06 UTC (rev 1215) +++ trunk/Toss/Play/Heuristic.ml 2010-12-04 13:02:34 UTC (rev 1216) @@ -613,37 +613,45 @@ let rec aux all_vars = function | Or phis -> Or (List.map (aux all_vars) phis) | And phis as phi when has_rels frels phi -> - And (List.map (aux all_vars) phis) + And (List.map (aux all_vars) phis) | Ex (vs, phi) when has_rels frels phi -> - Ex (vs, aux (add_strings (List.map var_str vs) all_vars) phi) + Ex (vs, aux (add_strings (List.map var_str vs) all_vars) phi) | phi -> - if has_rels frels phi then phi - else - let vars = - (* TODO: assumes all variables are FO! *) - List.map Formula.to_fo (FormulaOps.free_vars phi) in - if vars = [] then phi - else - let substs = - AssignmentSet.fo_assgn_to_list elems vars - (SolverIntf.M.evaluate struc - (SolverIntf.M.register_formula phi)) in - (* sort substitutions; TODO: optimizable *) - let substs = trunc_to_vars vars substs in - let all_vars = add_strings (List.map var_str vars) all_vars in - match - expanded_descr max_alt_descr elems rels struc - all_vars vars substs - with - | Or [] -> - (match phi with - | And phis -> And (List.map (aux all_vars) phis) - | Ex (vs, phi) -> - Ex (vs, aux - (add_strings (List.map var_str vs) all_vars) phi) - | _ -> phi) - | Or [psi] -> psi - | psi -> psi in + if has_rels frels phi then phi + else + let vars = + (* TODO: assumes all variables are FO! *) + List.map Formula.to_fo (FormulaOps.free_vars phi) in + if vars = [] then phi + else begin + (* {{{ log entry *) + if !debug_level > 3 then ( + Printf.printf + "Heuristic: computing expanded description for %s...\n%!" + (Formula.str phi) + ); + (* }}} *) + let substs = + AssignmentSet.fo_assgn_to_list elems vars + (SolverIntf.M.evaluate struc + (SolverIntf.M.register_formula phi)) in + (* sort substitutions; TODO: optimizable *) + let substs = trunc_to_vars vars substs in + let all_vars = add_strings (List.map var_str vars) all_vars in + match + expanded_descr max_alt_descr elems rels struc + all_vars vars substs + with + | Or [] -> + (match phi with + | And phis -> And (List.map (aux all_vars) phis) + | Ex (vs, phi) -> + Ex (vs, aux + (add_strings (List.map var_str vs) all_vars) phi) + | _ -> phi) + | Or [psi] -> psi + | psi -> psi + end in aux Strings.empty phi @@ -805,14 +813,44 @@ | None -> (* not monotonic *) let phi' = match struc with | Some struc -> - (* guards are currently ignored *) - expanded_form max_alt_descr frels struc - (FFTNF.ff_tnf (FFTNF.promote_rels frels) phi) + (* guards are currently ignored *) + (* {{{ log entry *) + if !debug_level > 2 then ( + Printf.printf + "Heuristic: for expanding, get ff-tnf of %s...\n%!" + (Formula.str phi); + ); + (* }}} *) + let phi'' = + FFTNF.ff_tnf (FFTNF.promote_rels frels) phi in + (* {{{ log entry *) + if !debug_level > 2 then ( + Printf.printf + "Heuristic: computing expanded form of %s...\n%!" + (Formula.str phi''); + ); + (* }}} *) + expanded_form max_alt_descr frels struc phi'' | None -> phi in + (* {{{ log entry *) + if !debug_level > 2 then ( + Printf.printf + "Heuristic: computing for (expanded) formula %s...\n%!" + (Formula.str phi') + ); + (* }}} *) of_formula adv_ratio (FFTNF.ff_tnf (FFTNF.promote_rels frels) phi') | Some fluent_preconds -> (* monotonic case *) + (* {{{ log entry *) + if !debug_level > 2 then ( + Printf.printf + "Heuristic: computing monotonic for %s...\n%!" + (Formula.str phi); + ); + (* }}} *) + (* FIXME: shouldn't be expanding? *) of_preconds fluent_preconds adv_ratio frels phi ) | Sum (vl, gd, e) -> Sum (vl, gd, aux (gd::gds) e) in This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |