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

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

Revision: 1546
          http://toss.svn.sourceforge.net/toss/?rev=1546&view=rev
Author:   lukstafi
Date:     2011-08-28 21:08:34 +0000 (Sun, 28 Aug 2011)
Log Message:
-----------
GDL translation: translate definition from command-line provided file; semantic definition of fluent paths and frame clauses, approximated on random playout states, refining the syntactic definition whenever sensible.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGame.mli
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/Formula/Aux.ml	2011-08-28 21:08:34 UTC (rev 1546)
@@ -288,11 +288,12 @@
   aux [] l
     
 
-let maximal cmp l =
+let maximal leq l =
+  let less x y = leq x y && not (leq y x) in
   let rec aux acc = function
     | hd::tl when
-        not (List.exists (fun x-> cmp hd x) acc) &&
-          not (List.exists (fun x-> cmp hd x) tl) ->
+        not (List.exists (fun x-> less hd x) acc) &&
+          not (List.exists (fun x-> less hd x) tl) ->
 	aux (hd::acc) tl
     | hd::tl -> aux acc tl
     | [] -> acc in

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/Formula/Aux.mli	2011-08-28 21:08:34 UTC (rev 1546)
@@ -176,9 +176,8 @@
 (** Find an element satisfying the predicate and separate it from the list. *)
 val pop_find : ('a -> bool) -> 'a list -> 'a * 'a list
 
-(** Return the list of maximal elements, under the given less-or-equal
-    comparison (the input does not need to be sorted). (Currently, of
-    equal elements only the last one is preserved.) *)
+(** Return the list of all maximal elements, under the given less-or-equal
+    comparison. (Maximal elements can be equivalent or incomparable.) *)
 val maximal : ('a -> 'a -> bool) -> 'a list -> 'a list
 
 (** Assuming that [l2] already has only maximal elements,

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/GGP/GDL.ml	2011-08-28 21:08:34 UTC (rev 1546)
@@ -1445,6 +1445,29 @@
   in
   aux (p, ps)
 
+let paths_intersect ps1 ps2 =
+  let rec aux = function
+    | Empty, p | p, Empty -> Empty
+    | Here, Here
+    | Here, Here_and_below _
+    | Here_and_below _, Here -> Here
+    | Here, Below _ | Below _, Here -> Empty
+    | Below ps1, Here_and_below ps2
+    | Here_and_below ps2, Below ps1
+    | Below ps1, Below ps2 -> Below (join (ps1, ps2))
+    | Here_and_below ps1, Here_and_below ps2
+      -> Here_and_below (join (ps1, ps2))
+  and join = function
+    | [], _ | _, [] -> []
+    | ((rel1, args1)::ps1), ((rel2, args2)::ps2) when rel1 = rel2 ->
+      let args = Aux.array_map2 (fun x y->aux (x,y)) args1 args2 in
+      (rel1, args)::join (ps1, ps2)
+    | ((rel1, _)::ps1), ((rel2, _)::_ as ps2) when rel1 < rel2 ->
+      join (ps1, ps2)
+    | ((rel1, _)::_ as ps1), ((rel2, _)::ps2) ->
+      join (ps1, ps2) in
+  aux (ps1, ps2)
+
 (** Find a path in a term and substitute, raise [Not_found] if path
     not present. [subst_at_path p s t] is $t[p \ot s]$. *)
 let subst_at_path p s t =

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/GGP/GDL.mli	2011-08-28 21:08:34 UTC (rev 1546)
@@ -235,6 +235,7 @@
 (** 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
+val paths_intersect : path_set -> path_set -> path_set
 
 (** List the paths in a set. *)
 val paths_to_list : path_set -> path list

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-08-28 21:08:34 UTC (rev 1546)
@@ -26,13 +26,6 @@
 let debug_level = ref 0
 let generate_test_case = ref None
 
-(** Treat "next" clauses which introduce a fluent position for a
-    variable-variable mismatch, as non-erasing frame clauses (to be
-    ignored). ("Wave" refers to the process of "propagating the frame
-    condition" that these clauses are assumed to do, if
-    [nonerasing_frame_wave] is set to [true].) *)
-let nonerasing_frame_wave = 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). *)
@@ -119,36 +112,99 @@
    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
    \mathrm{Next}_{e}$. Among the most similar terms finds one that is
-   not a "frame wave", if not possible and if {!nonerasing_frame_wave}
-   is [true] -- raises [Not_found]. *)
+   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
   (* worse-or-equal as "leq" *)
   let cmp (_, (_, pn1, siz1)) (_, (_, pn2, siz2)) =
-    not (siz1 > siz2) && pn2 >= pn1 in
+    siz1 < siz2 || siz1 = siz2 && pn1 >= pn2 in
   let best = Aux.maximal cmp gens in
-  (* avoid "frame wave" if possible *)
-  (* FIXME: TODO: handle frame waves as in updated reference spec *)
-  let t, (ps, _, _) =
-    if !nonerasing_frame_wave
-    then
-      List.find (fun (t, (ps, _, _)) ->
-        c = t ||
-          List.for_all
-          (fun fluent -> Aux.Strings.is_empty (term_vars fluent))
-          (at_paths ps t)) best
-    else List.hd best in
-  t, ps
+  (* avoid "wave" if possible *)
+  let nonwave_best, wave_best = Aux.partition_map
+    (fun (t, (ps, _, _)) ->
+      if List.for_all
+        (fun fluent -> Aux.Strings.is_empty (term_vars fluent))
+        (at_paths ps t)
+      then Aux.Left (ps, t)
+      else Aux.Right (ps, t))
+    best in
+  if nonwave_best = [] then true, wave_best
+  else false, nonwave_best
 
-    
+(* Find semantically the fluent paths of a clause -- works only for
+   clauses that are not "negative true". Find paths that merge with
+   nearest terms in prior state, better are paths that have less of
+   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. *)
+let semantic_fluent_paths program playout_states cl =
+  let head, body = match cl with
+    | ("next", [|head|]), body -> head, body
+    | _ -> assert false in
+  let old_run_aggregate = !run_prolog_aggregate in
+  run_prolog_aggregate := true;  
+  let state_fpaths state =
+    let new_sterms =
+      run_prolog_goal body
+        (replace_rel_in_program "true" (state_cls state) program) in
+    if new_sterms = []
+    then None
+    else
+      let new_sterms = List.map (fun sb->subst sb head) new_sterms in
+      let term_paths s =
+        if List.mem s state then empty_path_set
+        else
+          let _, best = most_similar s state in
+          let best = List.map
+            (fun (ps,_) -> ps,
+              List.length (Aux.unique_sorted
+                             (Aux.concat_map (at_paths ps) state)))
+            best in
+          let ps, _ = List.hd
+            (List.sort (fun (_,nts1) (_,nts2) -> nts1 - nts2) best) in
+        (* {{{ log entry *)
+          if !debug_level > 4 then (
+            Printf.printf "semantic_fluent_paths: for %s paths = %s\n%!"
+              (term_str s)
+              (String.concat ", " (List.map path_str (paths_to_list ps)));
+            if List.length (paths_to_list ps) > 1 then
+              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
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "semantic_fluent_paths: computing for body=%s...\n%!"
+      (String.concat " " (List.map literal_str body))
+  );
+  (* }}} *)
+  let fpaths_if_matched = Aux.map_some state_fpaths playout_states in
+  if fpaths_if_matched = [] then None
+  else
+    let res =
+      List.fold_left paths_union empty_path_set
+        fpaths_if_matched in
+    run_prolog_aggregate := old_run_aggregate;
+    (* {{{ log entry *)
+    if !debug_level > 2 then (
+      Printf.printf "semantic_fluent_paths: f_paths=%s\n%!"
+        (String.concat "; "(List.map path_str (paths_to_list res)))
+    );
+    (* }}} *)
+    Some res
 
 (* 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$). *)
-let fluent_paths_and_frames clauses =
+   (as in definition of $\calP_f$). 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
   let static, nonstatic = static_rels defs in
@@ -164,10 +220,8 @@
   let inline_defs =
     ("does", List.assoc "legal" defs)::inline_defs in
   (* To determine whether a clause is a frame, we need to know its
-     expansion, so we expand clauses separately. A proper frame clause
-     must have *all* expansions being proper frame clauses. But a
-     clause is dropped as "frame wave" if any of its expansions is
-     regarded as "frame wave". *)
+     expansion, so we expand clauses separately. A frame clause
+     must have *all* expansions being frame clauses. *)
   let next_clauses =
     List.filter (fun ((rel,_),_) -> rel="next") clauses in
   (* {{{ log entry *)
@@ -200,33 +254,52 @@
       (Aux.assoc_all "true" body) in
     let p_ts = true_args body in
     let n_ts = true_args neg_body in
-    let t_C, ps = most_similar s_C (p_ts @ n_ts) in
+    let wave, best = most_similar s_C (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 *)
-    t_C, ps, List.mem t_C n_ts in
-  let is_frame s_C (t_C, _, neg_true) =
+    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
   let find_fluents (c, c_e) =
     let s_C = (snd (fst c)).(0) in
-    (* discarding frame waves *)
-    (* FIXME: TODO: handle frame waves as in updated reference spec *)
-    let res = Aux.map_try (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"
         (term_str s_C) (String.concat ", "
-                          (List.map (fun (t,_,_)->term_str t) res))
+                          (List.map (fun (_,t,_,_)->term_str t) 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
+    then
+      let f_paths =
+        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 =
+        semantic_fluent_paths program playout_states c in
+      if sem_f_paths = Some empty_path_set (* frame clause *)
+      then Aux.Left c
+      else
       let f_paths =
-        List.map (fun (t_C, ps, neg_true) ->
-          if neg_true
-          then
-            term_paths (function Const _ -> true | _ -> false) t_C
-          else ps) res in
+        List.map (fun (wave, t_C, ps, neg_true) ->
+          let ps =
+            if neg_true
+            then
+              term_paths (function Const _ -> true | _ -> false) t_C
+            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 res = List.map find_fluents next_e in
   let frames, fluents = Aux.partition_choice res in
@@ -244,7 +317,7 @@
 (* Expand role variables, find fluent and mask paths, generate the
    initial structure. Encode frame clauses by using the unique
    relation name "frame next". *)
-let create_init_struc clauses =
+let create_init_struc program ~playout_states clauses =
   let players =
     Aux.map_some (function
       | ("role", [|player|]), _ -> Some player
@@ -275,7 +348,7 @@
   );
   (* }}} *)
   let frame_clauses, move_clauses, f_paths =
-    fluent_paths_and_frames clauses in
+    fluent_paths_and_frames program playout_states clauses in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf
@@ -435,7 +508,7 @@
   let frame_clauses = List.map
     (fun ((_,args),body) -> ("frame next", args), body) frame_clauses in
 
-  players, rules,
+  rules,
   frame_clauses @ move_clauses @ clauses,
   f_paths, m_paths, mask_reps, defined_rels,
   Aux.Strings.elements !stable_rels, Aux.Strings.elements !fluents,
@@ -740,10 +813,6 @@
    TODO: unrequired clauses with disjunctions may avoid being
    excluded. If this poses problems we might need to expand
    disjunctions containing potentially case-split atoms.
-
-   TODO: (important) filter-out case-split atoms based on conjoining
-   them with deterministic literals of required clauses (and checking
-   on the suite of random playout states).
 *)
 let rule_cases program playout_states rule_cls =
   let required_cls = Aux.map_some
@@ -1538,11 +1607,19 @@
 let translate_game ~playing_as clauses =
   let clauses = expand_players clauses in
   let used_vars, clauses = rename_clauses clauses in
-  let players, rules,
+  let players =
+    Aux.map_some (function
+      | ("role", [|player|]), _ -> Some player
+      | _ -> None
+    ) clauses in
+  let players = Array.of_list players in
+  let program = preprocess_program clauses in
+  let playout_states = generate_playout_states program players in
+  let rules,
     clauses, f_paths, m_paths,
     mask_reps, defined_rels, stable_rels, fluents,
     (*static_base,*) init_state, struc, ground_state_terms, elem_term_map =
-    create_init_struc clauses in
+    create_init_struc program ~playout_states clauses in
   let ground_at paths = List.map
     (fun p ->
       p, Aux.unique_sorted
@@ -1572,7 +1649,6 @@
     (List.map (fun ((rel,args),body as cl)->
       if rel = "frame next" then ("next", args), body
       else cl) clauses) in
-  let playout_states = generate_playout_states program players in
   let turn_data =
     try Some (check_turn_based players program)
     with Not_turn_based -> None in

Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/GGP/TranslateGame.mli	2011-08-28 21:08:34 UTC (rev 1546)
@@ -64,17 +64,18 @@
    purposes. Encode frame clauses by using the unique
    relation name "frame next".
 
-   [players, rules, frame_cls, move_cls, f_paths, m_paths, mask_reps,
-   defined_rels, stable_rels, fluents, init_state,
-   struc, ground_state_terms, elem_term_map = create_init_struc clauses] *)
+   [rules, clauses, f_paths, m_paths, mask_reps,
+   defined_rels, stable_rels, fluents,
+   init_state, struc, ground_state_terms, elem_term_map =
+   create_init_struc program ~playout_states clauses] *)
 val create_init_struc :
+  GDL.prolog_program ->
+  playout_states:GDL.term list list ->
   GDL.clause list ->
-  GDL.term array * GDL.gdl_rule list *
-    GDL.clause list * GDL.path_set *
-    GDL.path_set * GDL.term list * string list * string list *
-    string list * GDL.term list *
-    Structure.structure * GDL.term list *
-    GDL.term Aux.IntMap.t
+  GDL.gdl_rule list * GDL.clause list *
+    GDL.path_set * GDL.path_set * GDL.term list * string list *
+    string list * string list * GDL.term list * Structure.structure *
+    GDL.term list * GDL.term Aux.IntMap.t
 
 
 (* [playing_as] is only used for building move translation data, the

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-08-28 21:08:34 UTC (rev 1546)
@@ -116,11 +116,12 @@
     (fun () ->
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
       let clauses = GDL.expand_players descr in
-      let players, rules,
+      let program = preprocess_program clauses in
+      let rules,
         clauses, f_paths, m_paths, mask_reps, defined_rels,
         stable_rels, fluents,
         init_state, struc, ground_state_terms, elem_term_map =
-        TranslateGame.create_init_struc clauses in
+        TranslateGame.create_init_struc program ~playout_states:[] clauses in
 
       assert_equal ~msg:"f_paths" ~printer:(fun x->x)
         "cell_2; control_0"
@@ -209,16 +210,17 @@
 
 ]
 
-let a () =
-  (* GDL.debug_level := 4; *)
-  TranslateGame.debug_level := 4;
-  TranslateFormula.debug_level := 4;
-  GameSimpl.debug_level := 4;
-  DiscreteRule.debug_level := 4;
+let set_debug_level i =
+  (* GDL.debug_level := i; *)
+  TranslateGame.debug_level := i;
+  TranslateFormula.debug_level := i;
+  GameSimpl.debug_level := i;
+  DiscreteRule.debug_level := i;
   ()
 
 
 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"
@@ -278,3 +280,20 @@
   Aux.run_test_if_target "TranslateGameTest"
     ("TranslateGame" >::: [tests; bigtests])
 
+
+let main () =
+  Aux.set_optimized_gc ();
+  let (file) = (ref "") in
+  let opts = [
+    ("-v", Arg.Unit (fun () -> set_debug_level 1), "be verbose");
+    ("-d", Arg.Int (fun i -> set_debug_level i), "set debug level");
+    ("-f", Arg.String (fun s -> file := s), "process file");
+  ] in
+  Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
+  if !file = "" then exec () else
+    let descr = load_rules !file in
+    let gdl_data, result =
+      TranslateGame.translate_game ~playing_as:(GDL.Const "") descr in
+    print_endline (Arena.state_str result)
+      
+let _ = Aux.run_if_target "TranslateGameTest" main

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-08-27 09:44:45 UTC (rev 1545)
+++ trunk/Toss/www/reference/reference.tex	2011-08-28 21:08:34 UTC (rev 1546)
@@ -1335,7 +1335,7 @@
 
 To construct the elements of the structure from state terms, 
 and to make that structure a good representation of the game in Toss,
-we first determine which state terms always have common subtrees.
+we first determine which state terms have common subtrees.
 
 \begin{definition} \label{def-merge}
 For two terms $s$ and $t$ we say that a set of paths $P$ \emph{merges}
@@ -1361,10 +1361,10 @@
   $s_\calC$)}.  The term $t_\calC$ is the argument of \texttt{true} in
 the body of $\calC$ which is most similar to $s$ in the sense of
 Definition~\ref{def-merge}, and of equally similar has smallest
-$d\calP(s,t)$ (if there are several, we pick one arbitrarily).
+$d\calP(s,t)$.
 
 
-\paragraph{Wave Clauses}
+\paragraph{Wave Clauses and Fluent Paths}
 
 Let \emph{wave clauses} $\mathrm{Next}_{W}$ be defined as follows:
 $\calC \in \mathrm{Next}_{W}$ if there is $\calC' \in
@@ -1375,19 +1375,32 @@
 \emptyset \}$. Wave clauses propagate information across terms rather
 than describing a change of a term.
 
-\paragraph{Fluent Paths and Structure Elements}
+We often use the word \emph{fluent} for changing objects, and so we
+define the set of \emph{fluent paths}, $\calP_f$, based on two
+intuitions. Semantically, the intuition is that fluent paths are all
+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
+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.
 
-We often use the word \emph{fluent} for changing objects, and so we
-define the set of \emph{fluent paths}, $\calP_f$, in the following way.
-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 \texttt{true} in $\calC$.
-We write $\calL(t)$ for the set of paths to all constant leaves in $t$.
-The set
-\[ \calP_f \ = \ 
-      \bigcup_{\calC \in \mathrm{Next}_{f}} d\calP(s_\calC, t_\calC) \ \cup \
-      \bigcup_{\calC \in \mathrm{Next}_{f},\
-               t_\calC \text{ negative true in } \calC} \calL(t_\calC).
- \]
+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
+\texttt{true} in $\calC$.  We write $\calL(t)$ for the set of paths to
+all constant leaves in $t$.  The set
+\begin{align*}
+ \calP_f \ = \ &
+      \bigcup_{\calC \in \mathrm{Next}_{W}} d\calP(s^{sem}_\calC,t^{sem}_\calC) \ \cup \\
+     & \bigcup_{\calC \in \mathrm{Next}_{f}} d\calP(s_\calC, t_\calC) \ \cup \\
+     & \bigcup_{\calC \in \mathrm{Next}_{f},\
+               t_\calC \text{ negative true in } \calC} \calL(t_\calC) \cap d\calP(s^{sem}_\calC,t^{sem}_\calC).
+ \end{align*}
 Note that $\calP_f$ contains all merge sets for the selected terms in
 $\mathrm{Next}_e$ clauses, and additionally, when $t_\calC$ is a negative true,
 we add the paths to all constant leaves in $t_\calC$.
@@ -1434,6 +1447,8 @@
   $\calP_f = \{(\mathtt{cell},3), (\mathtt{control},1)\}$.
 \end{example}
 
+\paragraph{Structure Elements}
+
 The fluent paths define the partition of GDL state terms into elements
 of the Toss structures in the following way.
 
@@ -1796,32 +1811,22 @@
 So far, we have not accounted for the fact that rewrite rules of Toss
 only affect the matched part of the structure, while the GDL game
 definition explicitly describes the construction of the whole
-successive structure. We will say that a \texttt{next} clause is a
-\emph{frame clause} if and only if it contains a \texttt{true}
-relation applied to a term equal to the \texttt{next} argument. (TODO:
-a clause is a frame clause if it does not add a state term not
-present in the current state -- we will check empirically). Negating
-the frame clauses from the tuple $\ol{\calN}$ and transforming them
-into \emph{erasure clauses} will keep track of the elements that
-possibly lose fluents and ensure correct translation.
+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,
+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
+\emph{erasure clauses} will keep track of the elements that possibly
+lose fluents and ensure correct translation.
 
 We determine which clauses are frame clauses prior to partitioning
 into the rule clauses and computing the substitution
 $\sigma_{\ol{\calC},\ol{\calN}}$ -- at the point where fluent paths
-are computed. It is difficult to establish which wave clauses should
-be considered frame clauses. In the current implementation, we
-optimistically assume that all wave clauses not depending on player
-actions (\ie not containing \texttt{does}) are frame clauses (and
-currently we ignore frame-wave clauses as they do not provide useful
-erasure clauses). In the future, we might perform deeper checking as
-to which wave clauses are frame clauses. (TODO: redo this whole
-paragraph -- there will be no ``wave clauses'', we'll just detect
-frame clauses from random playouts.)
+are computed. We transform frame clauses by expanding relations that
+would otherwise be translated as defined relations: so as to eliminate
+local variables whenever possible.
 
-We transform frame clauses by expanding relations that would otherwise
-be translated as defined relations: so as to eliminate local variables
-whenever possible.
-
 From the frame clauses in $\sigma_{\ol{\calC}, \ol{\calN}}(\calN_1), \dots,
 \sigma_{\ol{\calC}, \ol{\calN}}(\calN_m)$, we select subsets $J$
 such that, clauses in $J$ having the form $\mathtt{(<= (next\ s_i)\ b_i)}$,

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