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

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

Revision: 1550
          http://toss.svn.sourceforge.net/toss/?rev=1550&view=rev
Author:   lukstafi
Date:     2011-08-31 13:56:07 +0000 (Wed, 31 Aug 2011)
Log Message:
-----------
GDL translation specification-level: optionally forcing fluent and within-mask paths to point to leaves of relevant terms. GDL translation major fixes: wrong algo for eliminating variables at fluent position subterms; do not consider terminal states for building rewrite rules; wrong algo for computing within-mask paths. Concurrent moves games: bug fixes in GDL translation; new translation test; small fixes (work remains) in ReqHandler.

Modified Paths:
--------------
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGame.mli
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/Server/ReqHandler.ml
    trunk/Toss/Server/ReqHandler.mli
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/GDL.ml	2011-08-31 13:56:07 UTC (rev 1550)
@@ -1130,13 +1130,15 @@
      if step < horizon then
        loop (actions::actions_accu) (state::state_accu) (step+1) next
      else 
-       let states = List.rev (next::state::state_accu) in
+       let states = List.rev (state::state_accu) in
        List.rev (actions::actions_accu),
-       List.map (fun ts->state_of_tups ts) states
+       List.map (fun ts->state_of_tups ts) states,
+       state_of_tups next
      with Playout_over ->
        List.rev actions_accu,
        List.map (fun ts->state_of_tups ts)
-         (List.rev (state::state_accu))) in
+         (List.rev state_accu),
+       state_of_tups state) in
   (* FIXME: this is identity, right? remove *)
   let init_base = saturate static_base state_rules in
   let init_state = Aux.StrMap.find "init" init_base in
@@ -1227,8 +1229,8 @@
     | _ -> false in
   List.map (fun (h, b) -> h, List.filter (Aux.neg neg_lit) b) cls
 
-(* Note that the list of playout states is
-   one longer than that of playout actions.
+(* Return the terminal state separately. The list of playout states is
+   same length as that of playout actions.
 
    To keep monotonicity, besides removing negative literals from
    "legal" clauses, we also add old terms to the state. (Only when
@@ -1267,9 +1269,9 @@
        loop (actions::actions_accu) (state::state_accu) (step+1) next
      else 
        List.rev (actions::actions_accu),
-       List.rev (next::state::state_accu)
+       List.rev (state::state_accu), next
      with Playout_over ->
-       List.rev actions_accu, List.rev (state::state_accu)) in
+       List.rev actions_accu, List.rev state_accu, state) in
   let init_state = List.map (fun (_,args) -> args.(0))
     (run_prolog_atom ("init", [|Var "x"|]) program) in
   (* {{{ log entry *)
@@ -1307,7 +1309,8 @@
         let trav = x::trav in
         let cycle = List.rev trav in
         loop cycle trav [] cycle tail in
-  loop [] [] [] [] cands
+  if cands = [] then []
+  else loop [] [] [] [] cands
 
 
 let player_vars_of rels =
@@ -1392,10 +1395,14 @@
 (* Subtries are in sorted order. *)
 
 let empty_path_set = Empty
+let eps_path = []
+let eps_path_set = Here
 
 let path_str p =
-  String.concat "_" (List.map (fun (rel, arg) ->
-    rel ^ "_" ^ string_of_int arg) p)
+  if p = [] then "eps_path"
+  else
+    String.concat "_" (List.map (fun (rel, arg) ->
+      rel ^ "_" ^ string_of_int arg) p)
 
 let paths_union ps1 ps2 =
   let rec aux = function
@@ -1607,21 +1614,30 @@
   path_str path ^ term_to_name subterm
 
 
-(* [expand_path_vars_by prepare_lits p ts clauses] expands variables
+(* [expand_path_vars_by prepare_lits p ts clauses] expands subterms
    that have occurrences at path [p] in some state term of a clause
    (from which pre-processed literals are extracted by
-   [prepare_lits]), by terms [ts]. *)
+   [prepare_lits]), by substituting their variables with corresponding
+   subterms of terms [ts]. *)
 let expand_path_vars_by prepare_lits p ts clauses =
   let exp_clause clause =
-    (* determine variables standing for players *)
     let pstates = state_terms (prepare_lits clause) in
-    let pvars = Aux.map_try
-      (fun s -> term_vars (at_path s p)) pstates in
-    let pvars = Aux.Strings.elements
-      (List.fold_left Aux.Strings.union Aux.Strings.empty pvars) in
-    if pvars = [] then [clause]
+    let pterms = Aux.map_try
+      (fun s -> at_path s p) pstates in
+    let multi_sb = Aux.concat_map
+      (fun gterm -> Aux.concat_map
+        (fun pterm ->
+          try match_nonblank [] [pterm] [gterm] with Not_found -> [])
+        pterms)
+      ts in
+    let multi_sb = Aux.collect multi_sb in
+    let multi_sb =
+      List.map (fun (v, ts) -> v, Aux.unique_sorted ts) multi_sb in
+    if multi_sb = [] then [clause]
     else
-      let sbs = Aux.power pvars ts in
+      let sb_vars, sb_terms = List.split multi_sb in
+      let sb_terms = Aux.product sb_terms in
+      let sbs = List.map (List.combine sb_vars) sb_terms in
       List.map (fun sb -> subst_clause sb clause) sbs in
   Aux.concat_map exp_clause clauses
 
@@ -1663,3 +1679,124 @@
       blank path_subts
   with Not_found ->
     invalid_arg "blank_outside_subterms: conflicting paths"
+
+
+(* If some path points only to bigger than one (i.e. non-leaf)
+   subterms in the given set of terms, then expand/split it to longer
+   paths that together cover all leafs the original path covered. *)
+let refine_leaf_paths paths terms =
+  let rec aux terms = function
+    | Empty -> Empty
+    | Here ->
+      if terms=[] ||
+        List.exists (function Func _ -> false | _ -> true) terms
+      then Here
+      else
+        let subterms = Aux.collect
+          (List.map (function Func (rel,args) -> rel,args
+            | _ -> assert false) terms) in
+        Below (List.map (fun (rel, args_set) ->
+          let arity =
+            Array.length (List.hd args_set) in
+          (* {{{ log entry *)
+          if !debug_level > 3 then (
+            Printf.printf "refine_leaf_paths: aux rel=%s, no terms=%d\n%!"
+              rel (List.length args_set)
+          );
+          (* }}} *)
+          rel, aux2 (Array.make arity Here) args_set) subterms)
+    | Below subpaths as path ->
+      let subterms = Aux.collect
+        (Aux.map_some (function Func (rel,args) -> Some (rel,args)
+          | _ -> None) terms) in
+      if subterms = []
+      then path
+      else
+        Below (List.map (fun (rel, arg_paths as r_subpaths) ->
+          try
+            rel, aux2 arg_paths (List.assoc rel subterms)
+          with Not_found -> r_subpaths) subpaths)
+    | Here_and_below subpaths as path ->
+      if terms=[] ||
+        List.exists (function Func _ -> false | _ -> true) terms
+      then path
+      else
+        let subterms = Aux.collect
+          (List.map (function Func (rel,args) -> rel,args
+            | _ -> assert false) terms) in
+        (* so far as [Here], from now as [Below] *)
+        Below (List.map (fun (rel, arg_paths as r_subpaths) ->
+          try
+            rel, aux2 arg_paths (List.assoc rel subterms)
+          with Not_found -> r_subpaths) subpaths)
+  and aux2 arg_paths args_set = Array.mapi
+    (fun i path ->
+      aux (List.map (fun a->a.(i)) args_set) path)
+    arg_paths in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "refine_leaf_paths:\npaths=%s\nterms=%s\n%!"
+      (String.concat "; " (List.map path_str (paths_to_list paths)))
+      (String.concat ", " (List.map term_str terms))
+  );
+  (* }}} *)
+  let res = aux terms paths in
+  res  
+
+(* Split paths in the set until, if possible, none of subterms at the
+   paths meets the predicate. Also remove paths not present in terms. *)
+let refine_paths_avoiding paths avoid terms =
+  let rec aux terms = function
+    | Empty -> Empty
+    | Here ->
+      if terms=[] then Empty
+      else if not (List.exists avoid terms)
+      then Here
+      else
+        let subterms =
+          Aux.map_some (function
+            | Func (rel,args) as t when not (avoid t) -> Some (rel,args)
+            | _ -> None) terms in
+        if subterms = [] then Empty
+        else
+          let subterms = Aux.collect subterms in
+          Below (List.map (fun (rel, args_set) ->
+            let arity =
+              Array.length (List.hd args_set) in
+            (* {{{ log entry *)
+            if !debug_level > 3 then (
+              Printf.printf "refine_paths_avoiding: aux rel=%s, no terms=%d\n%!"
+                rel (List.length args_set)
+            );
+            (* }}} *)
+            rel, aux2 (Array.make arity Here) args_set) subterms)
+    | (Here_and_below subpaths | Below subpaths) as path ->
+      if terms=[] then Empty
+      else if not (List.exists avoid terms)
+      then path
+      else
+        let subterms =
+          Aux.map_some (function
+            | Func (rel,args) as t when not (avoid t) -> Some (rel,args)
+            | _ -> None) terms in
+        if subterms = [] then Empty
+        else
+          let subterms = Aux.collect subterms in
+          let subpaths =
+            Aux.map_try (fun (rel, args_subpaths) ->
+              let args_subterms = List.assoc rel subterms in
+              rel, aux2 args_subpaths args_subterms) subpaths in
+          Below subpaths
+  and aux2 arg_paths args_set = Array.mapi
+    (fun i path ->
+      aux (List.map (fun a->a.(i)) args_set) path)
+    arg_paths in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "refine_paths_avoiding:\npaths=%s\nterms=%s\n%!"
+      (String.concat "; " (List.map path_str (paths_to_list paths)))
+      (String.concat ", " (List.map term_str terms))
+  );
+  (* }}} *)
+  let res = aux terms paths in
+  res  

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/GDL.mli	2011-08-31 13:56:07 UTC (rev 1550)
@@ -185,11 +185,11 @@
   aggregate:bool -> term array -> int -> gdl_rule list ->
   gdl_rule list * gdl_rule list * 
     graph * term list *
-    (term array list list * term list list)
+    (term array list list * term list list * term list)
 
 val playout_prolog :
   aggregate:bool -> term array -> int -> prolog_program ->
-  term array list list * term list list
+  term array list list * term list list * term list
 
 val find_cycle : term option list -> term option list
 
@@ -232,6 +232,7 @@
 val at_paths : ?fail_at_missing:bool -> path_set -> term -> term list
 
 val empty_path_set : path_set
+val eps_path_set : path_set
 (** Add path to a set. First argument gives term arities. *)
 val add_path : (string -> int) -> path -> path_set -> path_set
 val paths_union : path_set -> path_set -> path_set
@@ -243,9 +244,10 @@
 val path_str : path -> string
 
 (** [ground_vars_at_paths prepare_lits ps_sterms clauses] expands
-    variables that have occurrences at paths in [ps_sterms] in some
+    subterms that have occurrences at paths in [ps_sterms] in some
     state term of a clause (from which pre-processed literals are
-    extracted by [prepare_lits]), by terms provided in [ps_sterms]. *)
+    extracted by [prepare_lits]), by substituting their variables with
+    corresponding subterms of terms provided in [ps_sterms]. *)
 val ground_vars_at_paths :
   (clause -> literal list) ->
   (path * term list) list -> clause list -> clause list
@@ -256,3 +258,14 @@
 
 val blank_outside_subterms :
   (string * int) list -> (path * term) list -> term
+
+(** If some path points only to bigger than one (i.e. non-leaf)
+    subterms in the given set of terms, then expand/split it to longer
+    paths that together cover all leafs the original path covered. *)
+val refine_leaf_paths : path_set -> term list -> path_set
+
+(** Split paths in the set until, if possible, none of subterms at the
+    paths meets the predicate. Also remove paths not present in
+    terms. *)
+val refine_paths_avoiding :
+  path_set -> (term -> bool) -> term list -> path_set

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/GDLTest.ml	2011-08-31 13:56:07 UTC (rev 1550)
@@ -198,7 +198,7 @@
 	(not (true (control ?r))))
 " in
 
-      let _, _, _, _, (agg_actions, _) =
+      let _, _, _, _, (agg_actions, _, _) =
         GDL.playout_satur ~aggregate:true [|GDL.Const "x"; GDL.Const "o"|]
           10 (Aux.concat_map GDL.rules_of_clause descr) in
       let actions = List.map (List.map (fun a->"does", a)) agg_actions in      
@@ -208,7 +208,7 @@
         (String.concat ";\n" (List.map (fun step -> String.concat " "
           (List.map GDL.rel_atom_str step)) actions));
 
-      let _, _, _, _, (rand_actions, _) =
+      let _, _, _, _, (rand_actions, _, _) =
         GDL.playout_satur ~aggregate:false [|GDL.Const "x"; GDL.Const "o"|]
           10 (Aux.concat_map GDL.rules_of_clause descr) in
       let actions = List.map (List.map (fun a->"does", a)) rand_actions in      
@@ -251,7 +251,7 @@
 " in
 
       let program = GDL.preprocess_program descr in
-      let agg_actions, _ =
+      let agg_actions, _, _ =
         GDL.playout_prolog ~aggregate:true [|GDL.Const "x"; GDL.Const "o"|]
           10 program in
       let actions = List.map (List.map (fun a->"does", a)) agg_actions in      
@@ -261,7 +261,7 @@
         (String.concat ";\n" (List.map (fun step -> String.concat " "
           (List.map GDL.rel_atom_str step)) actions));
 
-      let rand_actions, _ =
+      let rand_actions, _, _ =
         GDL.playout_prolog ~aggregate:false [|GDL.Const "x"; GDL.Const "o"|]
           10 program in
       let actions = List.map (List.map (fun a->"does", a)) rand_actions in      
@@ -404,7 +404,7 @@
         GDL.playout_satur ~aggregate:false [|GDL.Const "x"; GDL.Const "o"|]
           10 (Aux.concat_map GDL.rules_of_clause clauses) in
       *)
-      let rand_actions, _ =
+      let rand_actions, _, _ =
         GDL.playout_prolog ~aggregate:false [|GDL.Const "x"; GDL.Const "o"|]
           10 (GDL.preprocess_program clauses) in
       let noop_actions = Aux.take_n 9

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-08-31 13:56:07 UTC (rev 1550)
@@ -26,6 +26,20 @@
 let debug_level = ref 0
 let generate_test_case = ref None
 
+(** Refine fluent paths to always point to some leaf, keeping the same
+    coverage of leafs on all ground state terms. *)
+let refine_leaf_f_paths = ref false
+
+(** Refine within-mask paths to always point to some leaf, keeping the same
+    coverage of leafs on all ground state terms. *)
+let refine_leaf_m_paths = ref true
+
+(** Refine fluent paths generated for a "next" clause to always point
+    to some leaf, with respect to the right-hand-side state
+    term. (Makes [refine_leaf_f_paths] redundant but generates
+    less fluent paths.) *)
+let propose_leaf_f_paths = ref true
+
 (** two heuristics for selecting defined relations: select relations
     with arity smaller than three; or, select relations that have ground
     defining clauses (i.e. defining clauses with empty bodies). *)
@@ -46,7 +60,7 @@
     rule needs to match in at least one generated state to be kept). *)
 let playouts_for_rule_filtering = ref 4
 
-let env_player = Const "ENVIRONMENT"
+let env_player = Const "Environment"
 
 type tossrule_data = {
   legal_tuple : term array;
@@ -103,11 +117,7 @@
   fluents = [];
 }
 
-let our_turn gdl state = true
 
-let noop_move gdl state = "NOOP"
-
-
 (* [most_similar c ts] finds a term from [ts] most similar to [c], and
    the set of paths that merges the found term and [c]; as in the
    definition of $s_\calC$ and $t_\calC$ for a clause $\calC \in
@@ -115,6 +125,15 @@
    not a "wave", if possible; returns the list of best candidates. *)
 let most_similar c ts =
   let gens = List.map (fun t -> t, merge_terms c t) ts in
+  (* {{{ log entry *)
+  if !debug_level > 4 then (
+    Printf.printf "most_similar: %s -->%!"(term_str c);
+    List.iter (fun (t, (ps, card, size)) ->
+      Printf.printf ", %s (at %d,%d: %s)" (term_str t) card size
+        (String.concat "; " (List.map path_str (paths_to_list ps)))) gens;
+    Printf.printf "\n%!";
+  );
+  (* }}} *)
   (* worse-or-equal as "leq" *)
   let cmp (_, (_, pn1, siz1)) (_, (_, pn2, siz2)) =
     siz1 < siz2 || siz1 = siz2 && pn1 >= pn2 in
@@ -137,7 +156,8 @@
    different subterms (at them) among prior state terms. Return fluent
    paths, an empty path set if the clause is a frame clause. Return
    [None] when the clause does not generate any state terms for any
-   provided playout state. *)
+   provided playout state. Refine the fluent paths with just the RHS
+   state term of the clause if [propose_leaf_f_paths] is true. *)
 let semantic_fluent_paths program playout_states cl =
   let head, body = match cl with
     | ("next", [|head|]), body -> head, body
@@ -163,7 +183,7 @@
             best in
           let ps, _ = List.hd
             (List.sort (fun (_,nts1) (_,nts2) -> nts1 - nts2) best) in
-        (* {{{ log entry *)
+          (* {{{ log entry *)
           if !debug_level > 4 then (
             Printf.printf "semantic_fluent_paths: for %s paths = %s\n%!"
               (term_str s)
@@ -172,7 +192,7 @@
               Printf.printf "state: %s\n\n%!"
                 (String.concat ", " (List.map term_str state))
           );
-        (* }}} *)
+          (* }}} *)
           ps in
       Some (List.fold_left paths_union empty_path_set
               (List.map term_paths new_sterms)) in
@@ -188,6 +208,9 @@
     let res =
       List.fold_left paths_union empty_path_set
         fpaths_if_matched in
+    let res =
+      if !propose_leaf_f_paths then refine_leaf_paths res [head]
+      else res in
     run_prolog_aggregate := old_run_aggregate;
     (* {{{ log entry *)
     if !debug_level > 2 then (
@@ -199,11 +222,11 @@
 
 (* Find $s_\calC$ and $t_\calC$ for a clause $\calC \in
    \mathrm{Next}_{e}$, i.e. in expanded "next" clauses. Determine
-   which original clauses are frame clauses, and which have to
-   be dropped (under assumption of being "frame waves"). Return the
-   proper frame clauses, the non-frame clauses, and the fluent paths
-   (as in definition of $\calP_f$). Augment the syntactic check with
-   semantic exploration whenever sensible. *)
+   which original clauses are frame clauses. Return the frame clauses,
+   the non-frame clauses, and the fluent paths (as in definition of
+   $\calP_f$). If [propose_leaf_f_paths] is true, refine fluent paths
+   of a clause with respect to the clause head state term. Augment the
+   syntactic check with semantic exploration whenever sensible. *)
 let fluent_paths_and_frames program playout_states clauses =
   let defs =
     defs_of_rules (Aux.concat_map rules_of_clause clauses) in
@@ -248,38 +271,40 @@
       (GDL.def_str ("next", next_exp))
   );
   (* }}} *)
-  let find_br_fluents s_C (_,body,neg_body) =
+  let find_br_fluents (* s_C *) (head,body,neg_body) =
+    let s_Ce = head.(0) in
     let true_args body = List.map
       (function [|t|] -> t | _ -> assert false)
       (Aux.assoc_all "true" body) in
     let p_ts = true_args body in
     let n_ts = true_args neg_body in
-    let wave, best = most_similar s_C (p_ts @ n_ts) in
+    let wave, best = most_similar s_Ce (p_ts @ n_ts) in
     let ps, t_C =
       try List.find (fun (_,t) -> not (List.mem t n_ts)) best
       with Not_found -> List.hd best in
     (* "negative true" check *)
-    wave, t_C, ps, List.mem t_C n_ts in
-  let is_frame s_C (_, t_C, _, neg_true) =
-    not neg_true && s_C = t_C in
+    wave, s_Ce, t_C, ps, List.mem t_C n_ts in
+  let is_frame (* s_C *) (_, s_Ce, t_C, _, neg_true) =
+    not neg_true && s_Ce = t_C in
   let find_fluents (c, c_e) =
     let s_C = (snd (fst c)).(0) in
-    let res = List.map (find_br_fluents s_C) c_e in
+    let res = List.map find_br_fluents (*s_C*) c_e in
     (* {{{ log entry *)
     if !debug_level > 3 then (
       Printf.printf
-        "find_fluents: most_similar for s_C=%s expansions t_C=%s\n"
+        "find_fluents: most_similar for s_C=%s expansions s_Ce-t_C=%s\n"
         (term_str s_C) (String.concat ", "
-                          (List.map (fun (_,t,_,_)->term_str t) res))
+                          (List.map (fun (_,s,t,_,_)->
+                            term_str s^"-"^term_str t) res))
     );
     (* }}} *)
-    if List.for_all (is_frame s_C) res
+    if List.for_all is_frame (*s_C*) res
     then Aux.Left c
     else if List.for_all
-        (fun (wave,_,_,neg_true)-> not wave && not neg_true) res
+        (fun (wave,_,_,_,neg_true)-> not wave && not neg_true) res
     then
       let f_paths =
-        List.map (fun (_, _, ps, _) -> ps) res in
+        List.map (fun (_, _, _, ps, _) -> ps) res in
       Aux.Right (c, List.fold_left paths_union empty_path_set f_paths)
     else
       let sem_f_paths =
@@ -288,24 +313,32 @@
       then Aux.Left c
       else
       let f_paths =
-        List.map (fun (wave, t_C, ps, neg_true) ->
+        List.map (fun (wave, s_Ce, t_C, ps, neg_true) ->
           let ps =
             if neg_true
             then
               term_paths (function Const _ -> true | _ -> false) t_C
             else ps in
+          let ps =
+            if !propose_leaf_f_paths then refine_leaf_paths ps [s_Ce]
+            else ps in
           if wave || neg_true then
             match sem_f_paths with
               | Some sem_ps -> paths_intersect sem_ps ps
               | None -> ps
           else ps
           ) res in
-      Aux.Right (c, List.fold_left paths_union empty_path_set f_paths) in
+      let f_paths =
+        List.fold_left paths_union empty_path_set f_paths in
+      Aux.Right (c, f_paths) in
   let res = List.map find_fluents next_e in
   let frames, fluents = Aux.partition_choice res in
   let move_clauses, f_paths = List.split fluents in
-  frames, move_clauses,
-  List.fold_left paths_union empty_path_set f_paths
+  let f_paths = List.fold_left paths_union empty_path_set f_paths in
+  if f_paths = empty_path_set then
+    failwith "fluent_path_and_frames: no fluent paths found";
+  frames, move_clauses, f_paths
+  
 
 
 let rec contains_blank = function
@@ -329,12 +362,12 @@
      performing aggregate playout, which is very much
      saturation-like. *)
   let static_rel_defs, nonstatic_rel_defs,
-    static_base, init_state, (agg_actions, agg_states) =
+    static_base, init_state, (agg_actions, agg_states, terminal_state) =
     playout_satur ~aggregate:true players !playout_horizon rules in
   (* *)
   (*
-  let program = preprocess_program clauses in
-  let agg_actions, agg_states =
+    let program = preprocess_program clauses in
+    let agg_actions, agg_states =
     playout_prolog ~aggregate:true players !playout_horizon program in
   *)
   let init_state = List.hd agg_states in
@@ -362,9 +395,24 @@
       Aux.unique_sorted
       (List.map (fun ((rel, args),_) -> rel, Array.length args)
          clauses) in
-  let ground_state_terms =
-    List.fold_left (fun acc st -> Aux.unique_sorted (st @ acc)) []
-      agg_states in
+  let ground_state_terms = List.fold_left
+    (fun acc st ->
+      Aux.sorted_merge (Aux.unique_sorted st) acc) []
+    (terminal_state::agg_states) in
+  let f_paths =
+    if !refine_leaf_f_paths
+    then (
+      let res = refine_leaf_paths f_paths ground_state_terms in
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf
+          "create_init_struc: refined f_paths=%s\n%!"
+          (String.concat "; "
+             (List.map GDL.path_str (GDL.paths_to_list res)))
+      );
+      (* }}} *)
+      res
+    ) else f_paths in
   let element_reps =
     Aux.unique_sorted (List.map (fun t ->
       simult_subst f_paths blank t) ground_state_terms) in
@@ -375,10 +423,8 @@
       (String.concat ", " (List.map term_str element_reps))
   );
   (* }}} *)
-  let m_paths = List.map
-    (term_paths ~prefix_only:true (Aux.neg contains_blank)) element_reps in
   let m_paths =
-    List.fold_left paths_union empty_path_set m_paths in
+    refine_paths_avoiding eps_path_set contains_blank element_reps in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf
@@ -387,6 +433,20 @@
          (List.map GDL.path_str (GDL.paths_to_list m_paths)))
   );
   (* }}} *)
+  let m_paths =
+    if !refine_leaf_m_paths
+    then (
+      let res = refine_leaf_paths m_paths ground_state_terms in
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf
+          "create_init_struc: refined m_paths=%s\n%!"
+          (String.concat "; "
+             (List.map GDL.path_str (GDL.paths_to_list res)))
+      );
+      (* }}} *)
+      res
+    ) else m_paths in
   let mask_reps =
     Aux.unique_sorted (List.map (fun t ->
       simult_subst m_paths blank t) element_reps) in
@@ -445,7 +505,7 @@
           let tup = Array.of_list (List.map2 at_path etup ptup) in
           if rel = "EQ_" && arity = 2 && tup.(0) = tup.(1) ||
             rel <> "EQ_" && graph_mem rel tup static_base
-            (* rel <> "EQ_" && run_prolog_check_atom (rel, tup) program *)
+          (* rel <> "EQ_" && run_prolog_check_atom (rel, tup) program *)
           then (
             stable_rels := Aux.Strings.add fact_rel !stable_rels;
             Structure.add_rel_named_elems struc fact_rel
@@ -1154,8 +1214,9 @@
     let _, _, _, _, (playout_actions, playout_states) =
       playout_satur ~aggregate:false players !playout_horizon rules in
   *)
-    let playout_actions, playout_states =
+    let playout_actions, playout_states, terminal_state =
       playout_prolog ~aggregate:false players !playout_horizon program in
+    if playout_actions = [] then raise Not_turn_based;
     (* {{{ log entry *)
     if !debug_level > 3 then (
       let actions = List.map
@@ -1164,7 +1225,7 @@
         String.concat ";\n" (List.map (fun step -> String.concat " "
           (List.map GDL.rel_atom_str step)) actions) in
       Printf.printf
-        "check_turn_based: no of states: %d, playout actions:\n%s\n%!"
+        "check_turn_based: no of in-game states: %d, playout actions:\n%s\n%!"
         (List.length playout_states) res
     );
     (* }}} *)
@@ -1259,10 +1320,13 @@
 
 
 let build_toss_rule transl_data rule_names struc fluents
-    synch_precond synch_postcond (legal_tuple, case_rhs, case_cond) =
+    synch_elems synch_precond synch_postcond
+    (legal_tuple, case_rhs, case_cond) =
   let rname =
-    Aux.not_conflicting_name !rule_names
-      (String.concat "_" (List.map term_to_name legal_tuple)) in
+    if legal_tuple = [] then "Environment"
+    else String.concat "_" (List.map term_to_name legal_tuple) in
+  let rname =
+    Aux.not_conflicting_name !rule_names rname in
   rule_names := Aux.Strings.add rname !rule_names;
   let label =
     {Arena.lb_rule = rname; time_in = 0.1, 0.1; parameters_in = []} in
@@ -1295,14 +1359,24 @@
   let rhs_add = synch_postcond @ rhs_add in
   let signat = Structure.rel_signature struc in
   let struc_elems = List.map
-    (fun sterm -> term_to_name (blank_out transl_data sterm))
-    case_rhs in
+    (fun sterm -> term_to_name (blank_out transl_data sterm)) case_rhs in
   let rulevar_terms = Aux.strmap_of_assoc
     (List.combine struc_elems case_rhs) in
-  let struc_elems = Aux.unique_sorted struc_elems in
+  let struc_elems = Aux.unique_sorted (synch_elems @ struc_elems) in
   let precond = FormulaOps.del_vars_quant
     (List.map Formula.fo_var_of_string struc_elems :> Formula.var list)
     precond in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    let add_str (rel, args) =
+      rel^"("^String.concat ", " (Array.to_list args)^")" in
+    Printf.printf
+      "build_toss_rule: rhs_add=%s; struc_elems=%s; total precond=\n%s\n\n%!"
+      (String.concat ", "(List.map add_str rhs_add))
+      (String.concat ", " struc_elems)
+      (Formula.str precond)
+  );
+  (* }}} *)
   let discrete =
     DiscreteRule.translate_from_precond ~precond
       ~add:rhs_add ~emb_rels:fluents ~signat ~struc_elems in
@@ -1373,7 +1447,6 @@
 let loc_graph_concurrent players
     player_payoffs struc build_rule fluents rule_cands =
   (* finding or creating the control predicate *)
-  let num_players = Array.length players in
   let control_pred, control_e, struc =
     try
       let control_pred, _ =
@@ -1408,17 +1481,19 @@
   let rules = ref [] in
   let tossr_data = ref [] in
   let players_with_env = Array.of_list
-    (Array.to_list players @ [env_player]) in
+    (env_player :: Array.to_list players) in
   let player_moves = List.map
     (fun (pl, p_rules) ->
       let pl_num =
         Aux.array_argfind (fun x -> x = pl) players_with_env in
       let p_rules = List.map
         (fun rcand ->
-          if pl_num = num_players then  (* environment *)
-            build_rule struc fluents all_players_precond [] rcand
+          if pl_num = 0 then  (* environment *)
+            build_rule struc fluents [control_vn]
+              all_players_precond [] rcand
           else
-            build_rule struc fluents [] (player_marker_rhs pl) rcand)
+            build_rule struc fluents [control_vn]
+              [] (player_marker_rhs pl) rcand)
         p_rules in
       (* we need to build first before adding [player_cond] because
          of how formula translation works *)
@@ -1466,7 +1541,8 @@
         let score =
           match score with
             | Const pay ->
-              (try float_of_string pay with _ -> assert false)
+              (try float_of_string pay with _ -> failwith
+                "TranslateGame.compute_payoffs: non-numeric goal value")
             | _ -> failwith
               ("TranslateGame.compute_payoffs: non-constant " ^
                   "goal values not implemented yet") in
@@ -1515,34 +1591,35 @@
 
 let transl_arg_type_no_side defined_rels init_state program
     ground_at_m_paths =
-  assert (ground_at_m_paths <> []);
-  let program =
-    replace_rel_in_program "true" (state_cls init_state) program in
-  List.map (fun (rel, ar) ->
-    let vtup = Array.init ar (fun i -> Var ("v"^string_of_int i)) in
-    let rel_graph = List.map snd
-      (run_prolog_atom (rel, vtup) program) in
-    match rel_graph with
+  if ground_at_m_paths = [] then []
+  else
+    let program =
+      replace_rel_in_program "true" (state_cls init_state) program in
+    List.map (fun (rel, ar) ->
+      let vtup = Array.init ar (fun i -> Var ("v"^string_of_int i)) in
+      let rel_graph = List.map snd
+        (run_prolog_atom (rel, vtup) program) in
+      match rel_graph with
       (* empty graph, take any path *)
-      | [] -> rel, Array.make ar None
-      | tup::tups ->
-        let projs =
-          List.fold_left
-            (fun agg_tup tup ->
-              Aux.array_map2 (fun x y->x::y) tup agg_tup)
-            (Array.map (fun t->[t]) tup) tups in
-        let intersects = Array.map
-          (fun rel_proj ->
-            let rel_proj = Aux.unique_sorted rel_proj in
-            List.sort (fun (i,_) (j,_) -> j-i) (
-              List.map
-                (fun (p, pts) ->
-                  List.length (Aux.list_inter rel_proj pts), p)
-                ground_at_m_paths)) projs in
-        rel,
-        Array.map (function (_, p)::_ -> Some p | [] -> None)
-          intersects
-  ) defined_rels
+        | [] -> rel, Array.make ar None
+        | tup::tups ->
+          let projs =
+            List.fold_left
+              (fun agg_tup tup ->
+                Aux.array_map2 (fun x y->x::y) tup agg_tup)
+              (Array.map (fun t->[t]) tup) tups in
+          let intersects = Array.map
+            (fun rel_proj ->
+              let rel_proj = Aux.unique_sorted rel_proj in
+              List.sort (fun (i,_) (j,_) -> j-i) (
+                List.map
+                  (fun (p, pts) ->
+                    List.length (Aux.list_inter rel_proj pts), p)
+                  ground_at_m_paths)) projs in
+          rel,
+          Array.map (function (_, p)::_ -> Some p | [] -> None)
+            intersects
+    ) defined_rels
 
 (* Representing rule candidates as (rule) clauses. *)
 let encode_rule_cands_in_clauses rule_cands clauses =
@@ -1580,7 +1657,7 @@
            cands) in
   rule_cands, clauses
 
-let generate_playout_states program players =
+let generate_playout_states ?(with_terminal=false) program players =
   (* {{{ log entry *)
   if !debug_level > 1 then (
     Printf.printf "translate_game: generating states...\n%!";
@@ -1589,10 +1666,11 @@
   (* }}} *)
   let states = Aux.fold_n
     (fun acc ->
-      let _, states =
+      let _, states, terminal_state =
         playout_prolog ~aggregate:false players !playout_horizon
           program in
-      states @ acc) [] !playouts_for_rule_filtering in
+      if with_terminal then terminal_state :: states @ acc
+      else states @ acc) [] !playouts_for_rule_filtering in
   (* {{{ log entry *)
   if !debug_level > 1 then (
     (* GDL.debug_level := 0; *)
@@ -1602,6 +1680,34 @@
   (* }}} *)
   states
 
+(* Expand goal value variables using values it could possibly have in
+   the game. *)
+let ground_goal_values ground_state_terms clauses =
+  (* the un-grounded goals, and remaining clauses *)
+  let goal_cls, clauses = Aux.partition_map
+    (function ("goal",[|_; Var v|]),_ as cl -> Aux.Left (v, cl)
+      | cl -> Aux.Right cl) clauses in
+  let rec neg_true = function
+    | Neg (True _) | Neg (Rel ("true",_)) -> true
+    | Disj disj -> List.exists neg_true disj
+    | _ -> false in
+  let pos_clauses = List.map
+    (fun (head, body) -> head, List.filter (Aux.neg neg_true) body)
+    clauses in
+  let pos_clauses =
+    List.map (fun t-> ("true",[|t|]),[]) ground_state_terms @
+      pos_clauses in
+  (* TODO: saturation-like memoization in the Prolog interpreter
+     might be needed because many "true" facts and removed negative
+     literals can lead to explosion of the amount of derivations. *)
+  let program = preprocess_program pos_clauses in
+  let expand (v, (_,body as g_cl)) =
+    let sbs = run_prolog_goal body program in
+    let v_sbs = Aux.unique_sorted
+      (List.map (fun sb-> [v, List.assoc v sb]) sbs) in
+    List.map (fun sb->subst_clause sb g_cl) v_sbs in
+  Aux.concat_map expand goal_cls @ clauses
+
 (* [playing_as] is only used for building move translation data, the
    translation is independent of the selected player. *)
 let translate_game ~playing_as clauses =
@@ -1620,6 +1726,7 @@
     mask_reps, defined_rels, stable_rels, fluents,
     (*static_base,*) init_state, struc, ground_state_terms, elem_term_map =
     create_init_struc program ~playout_states clauses in
+  let clauses = ground_goal_values ground_state_terms clauses in
   let ground_at paths = List.map
     (fun p ->
       p, Aux.unique_sorted
@@ -1688,17 +1795,22 @@
     TranslateFormula.build_defrels transl_data clauses in
   let rule_cands, clauses =
     decode_rule_cands_of_clauses rule_cands clauses in
-
-  let player_names = Array.to_list
-    (Array.mapi (fun i p -> term_to_name p, i) players) in
   (* possibly update the structure with a control element and predicate *)
   let rule_names = ref Aux.Strings.empty in
   let payoffs = compute_payoffs transl_data players clauses in
+  let player_names = Array.to_list
+    (Array.mapi (fun i p -> term_to_name p, i)
+       (if turn_data = None then Array.append [|env_player|] players
+        else players)) in
+  let payoffs =
+    if turn_data = None
+    then Array.append [|Formula.Const 0.0|] payoffs
+    else payoffs in
   let (graph, rules, tossrule_data), struc =
     match turn_data, rule_cands with
       | Some (loc_players, loc_noops), Aux.Left cands ->
         let build_rule =
-          build_toss_rule transl_data rule_names struc fluents [] [] in
+          build_toss_rule transl_data rule_names struc fluents [] [] [] in
         loc_graph_turn_based player_names payoffs
           loc_players loc_noops build_rule
           cands,
@@ -1706,6 +1818,7 @@
       | None, Aux.Right cands when is_concurrent ->
         let build_rule =
           build_toss_rule transl_data rule_names in
+        (* add Environment's payoff *)
         loc_graph_concurrent players payoffs struc build_rule
           fluents cands
       | None, Aux.Right cands ->
@@ -2040,3 +2153,22 @@
   );
   (* }}} *)
   res
+
+(* Returns [false] only if playing a turn-based game and the "playing
+   as" player should return the NOOP move; otherwise returns [true]. *)
+let our_turn gdl state =
+  match gdl.turnbased_noops with
+    | None -> true
+    | Some noops ->
+      noops.(state.Arena.cur_loc).(gdl.playing_as) <> None
+
+let noop_move gdl state =
+  match gdl.turnbased_noops with
+    | None -> failwith "noop_move: not a turn-based game"
+    | Some noops ->
+      match noops.(state.Arena.cur_loc).(gdl.playing_as) with
+        | None -> failwith "noop_move: not a NOOP location"
+        | Some noop -> term_str noop
+
+let is_turnbased gdl =
+  gdl.turnbased_noops <> None

Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/TranslateGame.mli	2011-08-31 13:56:07 UTC (rev 1550)
@@ -96,6 +96,11 @@
 val translate_outgoing_move : gdl_translation -> 
   (Arena.game * Arena.game_state) -> string -> (int * int) list -> string
 
+
 val noop_move : gdl_translation -> Arena.game_state -> string
 
-val our_turn : gdl_translation -> (Arena.game * Arena.game_state) -> bool
+(* Returns [false] only if playing a turn-based game and the "playing
+   as" player should return the NOOP move; otherwise returns [true]. *)
+val our_turn : gdl_translation -> Arena.game_state -> bool
+
+val is_turnbased : gdl_translation -> bool

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-08-31 13:56:07 UTC (rev 1550)
@@ -72,6 +72,7 @@
   assert_equal ~printer:(fun x->x) loc0_move transl;
   let moves =
     TranslateGame.translate_incoming_move gdl res
+      (* FIXME: should use the player ordering "plnum" right? *)
       [pte loc0_move; pte loc0_noop] in
   let move = List.assoc own_plnum moves in
   assert_equal ~msg:"own incoming move" ~printer:(emb_str res)
@@ -84,13 +85,84 @@
     Arena.emb_of_names res rname loc1_emb in
   let moves =
     TranslateGame.translate_incoming_move gdl res
+      (* FIXME: should use the player ordering "plnum" right? *)
       [pte loc1_noop; pte loc1_move] in
   let move = List.assoc opponent_plnum moves in
   assert_equal ~msg:"opponent incoming move"
     ~printer:(emb_str res)
     (norm_move (rname, emb)) (norm_move move)
 
+(* COPIED FROM ReqHandler. *)
+let select_moving a = (* temporary func - accept just one player w/ moves *)
+  let locs = Aux.array_find_all (fun l -> l.Arena.moves <> []) a in
+  if List.length locs <> 1 then failwith "too many moves" else
+    if locs = [] then a.(0) else List.hd locs
+exception Found of int
+(* The player applying the rewrite seems not to be used. *)
+(* FIXME: adapt to simultaneous moves. *)
+let apply_rewrite state (player, (r_name, mtch)) =
+  if r_name <> "" then (
+    let {Arena.rules=rules; graph=graph} = fst state in
+    let mv_loc = select_moving graph.((snd state).Arena.cur_loc) in
+    let moves =
+      Move.gen_moves Move.cGRID_SIZE rules
+        (snd state).Arena.struc mv_loc in
+    let pos = (
+      try
+        for i = 0 to Array.length moves - 1 do
+          let mov = moves.(i) in
+          if r_name = mov.Arena.rule && List.for_all 
+	    (fun (e, f) -> f = List.assoc e mov.Arena.embedding) mtch then
+	    raise (Found i)
+        done;
+        failwith "GDL Play request: action mismatched with play state"
+      with Found pos -> pos) in
+    let req = Arena.ApplyRuleInt (r_name, mtch, 0.1, []) in
+    let (new_state_noloc, resp) = Arena.handle_request state req in
+    let new_loc = moves.(pos).Arena.next_loc in
+    (fst new_state_noloc,
+     {snd new_state_noloc with Arena.cur_loc = new_loc})
+  ) else state
 
+let simult_test_case ~game_name ~player ~own_plnum ~opp_plnum
+    ~own_rule_name ~own_emb ~own_move ~opp_rule_name ~opp_emb
+    ~opp_move =
+  let game = load_rules ("./GGP/examples/"^game_name^".gdl") in
+  let gdl, res =
+    TranslateGame.translate_game ~playing_as:(Const player) game in
+  let goal_name = game_name^"-simpl.toss" in
+  (* let goal = state_of_file ("./GGP/tests/"^goal_name) in *)
+  let goal_str = Aux.input_file (open_in ("./GGP/tests/"^goal_name)) in
+  let resf = open_out ("./GGP/tests/"^game_name^"-temp.toss") in
+  let res_str = Arena.state_str res in
+  output_string resf res_str;
+  close_out resf;
+  (* let eq, msg = Arena.compare_diff goal res in *)
+  let eq, msg = goal_str = res_str, "sorry, just comparing as strings" in
+  assert_bool
+    ("GGP/examples/"^game_name^".gdl to GGP/tests/"^goal_name^
+        ", see GGP/tests/"^game_name^"-temp.toss: "^msg)
+        eq;
+  Sys.remove ("./GGP/tests/"^game_name^"-temp.toss");
+  let rname = own_rule_name in
+  let emb =
+    Arena.emb_of_names res rname own_emb in
+  let transl =
+    TranslateGame.translate_outgoing_move gdl res rname emb in
+  assert_equal ~printer:(fun x->x) own_move transl;
+  let moves =
+    TranslateGame.translate_incoming_move gdl res
+      [pte own_move; pte opp_move] in
+  let move = List.assoc own_plnum moves in
+  assert_equal ~msg:"own incoming move" ~printer:(emb_str res)
+    (norm_move (rname, emb)) (norm_move move);
+  let res =
+    List.fold_left apply_rewrite res moves in
+  (* TODO: perform a move by Environment once it is nicely provided
+     by for example ReqHandler. *)
+  ignore res;
+  ()
+
 let tests = "TranslateGame" >::: [
   "tictactoe" >::
     (fun () ->
@@ -108,6 +180,18 @@
         ~loc1_noop:"noop" ~loc1_move:"(mark 1 1)"
     );
 
+  "2player_normal_form_2010" >::
+    (fun () ->
+      simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
+        ~own_plnum:0 ~opp_plnum:1
+        ~own_rule_name:"row"
+        ~own_emb:["_BLANK_", "_BLANK_"]
+        ~own_move:"r1"
+        ~opp_rule_name:"column"
+        ~opp_emb:["_BLANK_", "_BLANK_"]
+        ~opp_move:"c1"
+    );
+
 ]
 
 let bigtests = "TranslateGameBig" >::: [
@@ -211,7 +295,7 @@
 ]
 
 let set_debug_level i =
-  (* GDL.debug_level := i; *)
+  GDL.debug_level := (i-2);
   TranslateGame.debug_level := i;
   TranslateFormula.debug_level := i;
   GameSimpl.debug_level := i;
@@ -221,18 +305,14 @@
 
 let a () =
   set_debug_level 4;
-      game_test_case ~game_name:"connect4" ~player:"white"
-        ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"drop_c11_noop"
-        ~loc0_emb:[
-          "cell_c11_h4__BLANK_", "cell_2_1__BLANK_";
-          "control__BLANK_", "control__BLANK_"]
-        ~loc0_move:"(drop 2)" ~loc0_noop:"noop"
-        ~loc1:1 ~loc1_rule_name:"noop_drop_c12"
-        ~loc1_emb:[
-          "cell_c12_h6__BLANK_", "cell_2_1__BLANK_";
-          "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(drop 2)"
+      simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
+        ~own_plnum:0 ~opp_plnum:1
+        ~own_rule_name:"row"
+        ~own_emb:["_BLANK_", "_BLANK_"]
+        ~own_move:"r1"
+        ~opp_rule_name:"column"
+        ~opp_emb:["_BLANK_", "_BLANK_"]
+        ~opp_move:"c1"
 
 
 let a () =

Modified: trunk/Toss/Server/ReqHandler.ml
===================================================================
--- trunk/Toss/Server/ReqHandler.ml	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/Server/ReqHandler.ml	2011-08-31 13:56:07 UTC (rev 1550)
@@ -53,6 +53,7 @@
 
 
 (* The player applying the rewrite seems not to be used. *)
+(* FIXME: adapt to simultaneous moves. *)
 let apply_rewrite state (player, (r_name, mtch)) =
   if r_name <> "" then (
     let {Arena.rules=rules; graph=graph} = fst state in
@@ -128,7 +129,11 @@
       TranslateGame.translate_incoming_move gdl_transl state actions in
 
     let state = List.fold_left apply_rewrite state rewrites in
-
+    let state =
+      if rewrites = [] || TranslateGame.is_turnbased gdl_transl
+      then state
+      else failwith
+        "ReqHandler: implement performing a move by player Environment" in
     let resp =
       if (match rq with 
 	| Aux.Right (GDL.Stop (_, actions)) -> true
@@ -138,7 +143,7 @@
       else
 	let mov_msg =
           let time_used = time_started -. Unix.gettimeofday () in
-	  if TranslateGame.our_turn gdl_transl state then (
+	  if TranslateGame.our_turn gdl_transl (snd state) then (
 	    Play.set_timeout (float(playclock) -. time_used -. 0.07);
 	    let heur = match g_heur with
 	      | Some h -> h

Modified: trunk/Toss/Server/ReqHandler.mli
===================================================================
--- trunk/Toss/Server/ReqHandler.mli	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/Server/ReqHandler.mli	2011-08-31 13:56:07 UTC (rev 1550)
@@ -14,6 +14,11 @@
 
 val html_dir_path : string ref
 
+val apply_rewrite :
+  Arena.game * Arena.game_state ->
+  (string * (string * DiscreteRule.matching)) ->
+  Arena.game * Arena.game_state
+
 type req_state =
   Formula.real_expr array array option (** heuristic option *)
     * bool (** game modified *)

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-08-29 21:08:20 UTC (rev 1549)
+++ trunk/Toss/www/reference/reference.tex	2011-08-31 13:56:07 UTC (rev 1550)
@@ -1381,14 +1381,14 @@
 the $d\calP(s,t)$ paths where $s$ is any new state term and $t$ is its
 closest state term from the prior state, for any reachable prior
 state. Let us represent such paths, summed over $s$ generated by a
-clause $\calC$, as $d\calP(s^{sem}_\calC,t^{sem}_\calC)$. The other
+clause $\calC$, as $d\calP(s^{sem}_\calC,t^{sem}_\calC)$. We approximate the sets
+$d\calP(s^{sem}_\calC,t^{sem}_\calC)$ from below by computing them on
+states from a small number of random playouts. The other
 intuition applies to some games that start with a small set of state
 terms, and we do not want to consider the whole gradually introduced
 state terms as fluent, rather we determine syntactically which
 subterms would change no matter what state terms were already
-introduced. We approximate the sets
-$d\calP(s^{sem}_\calC,t^{sem}_\calC)$ from below by computing them on
-states from a small number of random playouts.
+introduced.
 
 We say that a term $t$ is a \emph{negative true} in a
 clause $\calC$ if it is the argument of a negative occurrence of
@@ -1405,6 +1405,12 @@
 $\mathrm{Next}_e$ clauses, and additionally, when $t_\calC$ is a negative true,
 we add the paths to all constant leaves in $t_\calC$.
 
+Optionally, we refine the paths (that is, replace with a larger set of
+longer paths) $d\calP(s^{sem}_\calC,t^{sem}_\calC)$ and
+$d\calP(s_\calC, t_\calC)$ to point to the leaves of the relevant
+state terms that contain them (the $t_\calC$ term and the terms
+$t^{sem}_\calC$ that are closest to $s_\calC$ in the state transitions
+considered).
 
 \begin{example}
 There are three \texttt{next} clauses in Figure~\ref{fig-ttt-gdl}.
@@ -1491,6 +1497,8 @@
 is $\calP_m = \{(\mathtt{cell},1), (\mathtt{cell},2)\}$. 
 \end{example}
 
+Optionally, we refine $\calP_m$ afterwards to point to the leaves of
+the state terms that contain a path, among all ground state terms.
 
 \subsection{Relations in the Structure} \label{subsec-rels}
 
@@ -1791,10 +1799,11 @@
 \end{example}
 
 With all tuples $\ol{\calC}, \ol{\calN}$ selected and the MGU
-$\sigma_{\ol{\calC},\ol{\calN}}$ computed, we are almost ready to construct
-the rewriting rules. Still, for a fixed tuple $\ol{\calC}, \ol{\calN}$,
-we first need to compute erasure clauses to prevent constructing
-too general rules in the end.
+$\sigma_{\ol{\calC},\ol{\calN}}$ computed, we are almost ready to
+construct the rewriting rules. Still, for a fixed tuple $\ol{\calC},
+\ol{\calN}$, we first need to compute ``erasure clauses'' to make sure
+that a rewrite rule captures the whole substructure that should be
+affected.
 
 \paragraph{Concurrent Moves Games} Introduced in
 Section~\ref{subsec-concurrency}, concurrent moves games use a
@@ -1813,7 +1822,7 @@
 definition explicitly describes the construction of the whole
 successive structure. We say that a \texttt{next} clause $\calC$ is a
 \emph{frame clause} when $d\calP(s^{sem}_\calC,t^{sem}_\calC) =
-\setempty$ (if possible, \ie when the clause is not a wave clause,
+\emptyset$ (if possible, \ie when the clause is not a wave clause,
 approximated by checking whether it contains a \texttt{true} relation
 applied to a term equal to the \texttt{next} argument). Negating the
 frame clauses from the tuple $\ol{\calN}$ and transforming them into

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.