[Toss-devel-svn] SF.net SVN: toss:[1216] trunk/Toss

[<luk...@us...>]

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.