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

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

Revision: 1617
          http://toss.svn.sourceforge.net/toss/?rev=1617&view=rev
Author:   lukstafi
Date:     2011-10-25 21:40:52 +0000 (Tue, 25 Oct 2011)
Log Message:
-----------
GDL translation: turning single-argument state term functions with domain greater than three into value_ terms, e.g. (x 10) into (value_ x 10); more refined handling of move clauses: not all containing a matching <does> are required; bug fix in finding fluent paths. GDL tests: asteroids-scrambled not using numbers for position and velocity (weak integration of counters and structural parts); test fails due to current shortcomings in erasure and unframed fluents handling.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml

Added Paths:
-----------
    trunk/Toss/GGP/examples/asteroids-scrambled.gdl
    trunk/Toss/GGP/tests/asteroids-scrambled-raw.toss
    trunk/Toss/GGP/tests/asteroids-scrambled-simpl.toss

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-10-25 08:24:28 UTC (rev 1616)
+++ trunk/Toss/Arena/Arena.ml	2011-10-25 21:40:52 UTC (rev 1617)
@@ -91,13 +91,20 @@
     ).ContinuousRule.discrete.DiscreteRule.lhs_struc in
   try
     List.map (fun (lhs_e, m_e) ->
-      Structure.find_elem lhs lhs_e, Structure.find_elem state.struc m_e)
+      (try Structure.find_elem lhs lhs_e
+       with Not_found -> Printf.printf "NF lhs_e=%s\n%!" lhs_e;
+         raise Not_found),
+      (try Structure.find_elem state.struc m_e
+       with Not_found -> Printf.printf "NF m_e=%s\n%!" m_e;
+         raise Not_found))
       emb_str
   with Not_found ->
     (* {{{ log entry *)
     if !debug_level > 0 then (
-      Printf.printf "emb_of_names: failed at LHS=\n%s\nSTRUC=\n%s\n%!"
+      Printf.printf "emb_of_names: failed at LHS=\n%s\nSTRUC=\n%s\nEMB=%s\n%!"
         (Structure.str lhs) (Structure.str state.struc)
+        (String.concat "; "
+           (List.map (fun (v,e) ->v^"<-"^e) emb_str))
     );
     (* }}} *)
     failwith ("emb_of_names: could not find " ^

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-10-25 08:24:28 UTC (rev 1616)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-10-25 21:40:52 UTC (rev 1617)
@@ -134,6 +134,9 @@
     literal). Compute the relation-argument-position, predicate
     implications including relations produced by gluing.
 
+    TODO-FIXME: extend operations (specifically 2) to handle formulas
+    nested in real expressions; with special treatment for update
+    expressions in rules (using the compiled precondition as context).
 *)
 
 open Formula

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-10-25 08:24:28 UTC (rev 1616)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-10-25 21:40:52 UTC (rev 1617)
@@ -17,13 +17,14 @@
     defined relation: a Toss defined relation (i.e. does not normally
     occur in the structure)
 
-    TODO: perform "fluent path prediate inversion" by transforming
-    single-argument state terms into two arguments of a "value" state
-    term.
-
     TODO-FIXME: limit translation as concurrent games to cases where
     rules do not check fluents affected by other rules to be performed
     concurrently.
+
+    TODO-FIXME: missing interactions between counters and the
+    structural part of rewriting (try translate "asteroids.gdl").
+
+    TODO-FIXME: add make_all_nondistinct by default.
 *)
 
 open GDL
@@ -90,6 +91,22 @@
     literals). *)
 let filter_possibly_redundant = ref true
 
+(** When [require_all_w_does] is true, rule generation is optimized by
+    requiring all "next" clauses that match a given "legal/does" term
+    -- that have a "does" atom -- be present in a rule. Setting to
+    true violates correctness for games like "asteroids" where a
+    single "(turn clock)" legal term is used for different headings
+    which have different "next" clauses. *)
+let require_all_w_does = ref false
+
+(** When true, keep only rule candidates with maximal sets of clauses. *)
+let filter_maximal_rules = ref true
+
+(** TODO: Translate all rules as "nondistinct", i.e. not forcing difference
+    of elements while finding the "rule embedding" homomorphism.
+    TODO: modify Arena to do that by a simple rule marker. *)
+let make_all_nondistinct = ref true
+
 let env_player = Const "environment"
 
 type tossrule_data = {
@@ -203,12 +220,27 @@
     else
       let new_paths = term_paths
         (function Func _ -> false | _ -> true) head in
-      let p_subterms = Aux.concat_map
-        (map_paths (fun p s -> p, s) new_paths) ground_state_terms in
+      let p_subterms = Aux.unique_sorted
+        (Aux.concat_map
+           (map_paths (fun p s -> p, s) new_paths) ground_state_terms) in
+      (* {{{ log entry *)
+      if !debug_level > 3 then (
+        Printf.printf "find_cl_fluent: p_subterms=%s\n%!"
+          (String.concat "; "(List.map (fun (p,s)->
+            path_str p^"->"^term_str s) p_subterms))
+      );
+      (* }}} *)
       let p_subterms = Aux.collect p_subterms in
-      match List.sort (fun (_,i) (_,j)->j-i)
-        (List.map (fun (p,ts) -> p, List.length ts) p_subterms)
-      with
+      let p_subterms = List.sort (fun (_,i) (_,j)->i-j)
+        (List.map (fun (p,ts) -> p, List.length ts) p_subterms) in
+      (* {{{ log entry *)
+      if !debug_level > 3 then (
+        Printf.printf "find_cl_fluent: p_subterm counts=%s\n%!"
+          (String.concat "; "(List.map (fun (p,num)->
+            path_str p^": "^string_of_int num) p_subterms))
+      );
+      (* }}} *)
+      match p_subterms with
         | [] -> failwith
           ("fluent_paths_and_frames: next head "^term_str head^
               " has no instance among ground state terms")
@@ -223,13 +255,13 @@
   let f_paths =
     List.fold_left find_cl_fluent empty_path_set move_cls in
   (* {{{ log entry *)
-if !debug_level > 3 then (
-  Printf.printf "frame clauses:\n%s\n"
-    (String.concat "\n"
-       (List.map (fun (h,body)->term_str h^" <== "^literals_str body)
-          frame_cls))
-);
-(* }}} *)
+  if !debug_level > 3 then (
+    Printf.printf "frame clauses:\n%s\n"
+      (String.concat "\n"
+         (List.map (fun (h,body)->term_str h^" <== "^literals_str body)
+            frame_cls))
+  );
+  (* }}} *)
   frame_cls, move_cls, f_paths
 
 
@@ -240,13 +272,18 @@
 
 let val_path = ["val_", 0]
 
-(* Expand role variables, find fluent and coordinate paths, lift
-   unused state terms into relations and add state terms / elements
-   for missing subterms. *)
-let prepare_paths_and_elems players_wo_env program ~playout_states clauses =
+(* Expand role variables. Compute all ground state terms. Transform
+   single-argument state terms with more than three ground terms
+   having the same functor into two-argument "value_" state terms:
+   e.g. "(x 10)" into "(value_ x 10)". Find fluent and coordinate
+   paths. Lift unused state terms into relations. Add state terms /
+   elements for missing subterms. *)
+let prepare_paths_and_elems players_wo_env ~playout_states clauses =
   let rules = Aux.concat_map rules_of_clause clauses in
   let static_rels, nonstatic_rels =
     static_rels (defs_of_rules rules) in
+  let static_rels = Aux.list_diff static_rels
+    ["goal"; "next"; "legal"] in
   (* Turns out the saturation-based solver is sometimes far better for
      performing aggregate playout, which is very much
      saturation-like. *)
@@ -255,9 +292,9 @@
     playout_satur ~aggregate:true players_wo_env !playout_horizon rules in
   (* *)
   (*
-  let program = preprocess_program clauses in
-  let agg_actions, agg_states =
-  playout_prolog ~aggregate:true players !playout_horizon program in
+    let program = preprocess_program clauses in
+    let agg_actions, agg_states =
+    playout_prolog ~aggregate:true players !playout_horizon program in
   *)
   (* {{{ log entry *)
   if !debug_level > 4 then (
@@ -270,8 +307,68 @@
     (fun acc st ->
       Aux.sorted_merge (Aux.unique_sorted st) acc) []
     (terminal_state::agg_states) in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf
+      "prepare_paths_and_elems: initial ground_state_terms=\n%s\n%!"
+      (String.concat " "(List.map term_str ground_state_terms))
+  );
+  (* }}} *)
   let init_state = List.hd agg_states in
   check_timeout "TranslateGame: prepare_paths_and_elems: init_state";
+  let value_terms = Aux.map_some
+    (function Func (f, [| arg |]) -> Some (f, arg)
+      | _ -> None) ground_state_terms in
+  let value_terms = List.filter
+    (fun (f, graph) -> List.length graph > 3)
+    (Aux.collect value_terms) in
+  let value_funcs = Aux.strings_of_list (List.map fst value_terms) in
+  let value_terms = Aux.concat_map
+    (fun (f,graph) -> List.map
+      (fun arg-> Func ("value_", [|Const f; arg|])) graph)
+    value_terms in
+  let ground_state_terms = List.filter
+    (function Func (f, [| _ |]) -> not (Aux.Strings.mem f value_funcs)
+      | _ -> true) ground_state_terms in
+  let ground_state_terms = value_terms @ ground_state_terms in
+  let rec lift_to_value = function
+    | Pos (True (Func (f, [|arg|])))
+        when Aux.Strings.mem f value_funcs ->
+      Pos (True (Func ("value_", [|Const f; arg|])))
+    | Neg (True (Func (f, [|arg|])))
+        when Aux.Strings.mem f value_funcs ->
+      Neg (True (Func ("value_", [|Const f; arg|])))
+    | Disj disj -> Disj (List.map lift_to_value disj)
+    | l -> l in
+  let clauses =
+    if Aux.Strings.is_empty value_funcs then clauses
+    else List.map
+      (function
+        | ("init", [|Func (f, [|arg|])|]), body
+          when Aux.Strings.mem f value_funcs ->
+          ("init", [|Func ("value_", [|Const f; arg|])|]),
+            List.map lift_to_value body
+        | ("next", [|Func (f, [|arg|])|]), body
+          when Aux.Strings.mem f value_funcs ->
+          ("next", [|Func ("value_", [|Const f; arg|])|]),
+            List.map lift_to_value body
+        | h, body ->
+          h, List.map lift_to_value body) clauses in
+  let state_lift_value state = List.map
+    (function
+      | Func (f, [|arg|]) when Aux.Strings.mem f value_funcs ->
+        Func ("value_", [|Const f; arg|])
+      | sterm -> sterm) state in
+  let playout_states = List.map state_lift_value playout_states in
+  let init_state = state_lift_value init_state in
+  let program = preprocess_program clauses in
+(* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "after-lift-value: playout_states=%s\n\n%!"
+      (String.concat "\n" (List.map (fun state->
+        String.concat " "(List.map term_str state)) playout_states))
+  );
+  (* }}} *)
   let arities =
     ("EQ_", 2)::
       Aux.unique_sorted
@@ -330,6 +427,13 @@
     (function
       | Func (f, _) when Aux.Strings.mem f unused_roots -> false
       | _ -> true) ground_state_terms in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf
+      "prepare_paths_and_elems: resulting ground_state_terms=\n%s\n%!"
+      (String.concat " "(List.map term_str ground_state_terms))
+  );
+  (* }}} *)
   let more_base = Aux.map_some
     (function
       | [|Func (f, args)|] when Aux.Strings.mem f unused_roots ->
@@ -453,7 +557,7 @@
   static_base, init_state, c_paths, f_paths, element_reps, root_reps,
     framed_fluents,
     ground_state_terms, arities, term_arities, static_rels, nonstatic_rels,
-    frame_clauses, move_clauses, clauses
+    frame_clauses, move_clauses, clauses, program, playout_states
 
 
 let default_argpaths rel ar init_state program ground_at_c_paths =
@@ -1108,37 +1212,7 @@
   subst sb head, subst_literals sb body
 
 
-(* Callgraph for creating "move tuples" and Toss rules.
 
-   (1) [create_init_struc] prepares [next_cls], segregated into frame
-   clauses and normal clauses, with head term extracted.
-
-   (2) [move_tuples] selects maximal tuples of [next_cls] such that
-   their "legal"/"does" terms unify.
-
-   (3) [add_erasure_clauses] converts frame into erasure clauses, and
-   adds the result to non-frame clauses (without framing
-   information).
-
-   (4) [process_rule_cands] calls [move_tuples], applies the unifier,
-   and calls [add_erasure_clauses].
-
-   (5) [rule_cases] distributes clauses from a move tuple to
-   disjointly cover all applicability conditions. Then it collects all
-   head terms and conflates the bodies to produce a rule
-   candidate. Legality conditions are not passed to [rule_cases].
-
-   (6) [turnbased_rule_cases], [concurrent_rule_cases] and
-   [general_int_rule_cases] call [rule_cases], add legal terms and
-   legality conditions to the result when appropriate (the
-   environment does not have legality conditions). Rules for players
-   as well as for the environment (when not turn-based) are built.
-
-   (7) [create_rule_cands] calls the right routine of (6).
-
-*)
-
-
 (* Find the rule clauses $\ol{\calC},\ol{\calN}$. Also handles as
    special cases: "concurrent" case with selecting clauses for only
    one player, and "environment" case for selecting clauses not
@@ -1233,7 +1307,7 @@
         if List.exists
           (function Pos (Does _) -> true | _ -> false) body
         then
-          head, (frame, true),
+          head, (frame, !require_all_w_does),
           List.filter
             (function Pos (Does _) -> false | _ -> true) body
         else
@@ -1575,16 +1649,12 @@
     (fun (h, required, body) ->
       if required then Some (h, body) else None) rule_cls in
   let required_body = Aux.concat_map snd required_cls in
-  let counter_cls = List.map
-    (fun (f, brs) ->
-      let brs = List.map
-        (fun (cond, update) ->
-          let sb, cond = filter_redundant required_body cond in          
-          subst_literals sb cond, update)
-        brs in
-      f, brs)
-    counter_cls in
-
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "rule_cases: required_body=%s\n%!"
+      (literals_str required_body)
+  );
+  (* }}} *)
   let unrequired_cls = Aux.map_some
     (fun (h, required, body) ->
       if not required then Some (h, body) else None) rule_cls in  
@@ -1607,9 +1677,9 @@
       (* {{{ log entry *)
       if !debug_level > 3 then (
         Printf.printf
-          "\nrule_cases: checking urequired %s\nstatic_goal=%s\n%!"
+          "\nrule_cases: checking unrequired %s\nstatic_goal=%s\n%!"
           (String.concat " "(List.map literal_str unreq_body))
-          (String.concat " "(List.map literal_str static_goal))
+          (String.concat " "(List.map literal_str static_goal));
       );
       (* }}} *)
       let res =
@@ -1655,8 +1725,9 @@
       Printf.printf "rule_cases: single partition\n%!";
     );
     (* }}} *)
-    [Aux.unique_sorted case_rhs, counter_cls,
-     Aux.unique_sorted (List.concat case_conds)]
+    [Aux.Ints.singleton 0,
+     (Aux.unique_sorted case_rhs, counter_cls,
+      Aux.unique_sorted (List.concat case_conds))]
   else
     let patterns =
       let unrequired_cls = Array.of_list unrequired_cls in
@@ -1690,18 +1761,26 @@
     );
     (* }}} *)
     let choices = Aux.power split_atoms [false; true] in
+    let unrequired_cls = Array.of_list unrequired_cls in
     let rule_case choice =
       let separation_cond =
         List.map (fun (a,b) -> if b then Pos a else Neg a) choice in
-      let case_cls =
-        List.filter (fun (_, body) ->
-          List.for_all (fun (a,b) ->
-            if b then                     (* atom not excluded *)
-              not (List.mem (Neg a) body)
-            else                          (* atom not included *)
-              not (List.mem (Pos a) body)
-          ) choice
+      let case =
+        Aux.array_mapi_some (fun i (_, body as cl) ->
+          if
+            List.for_all (fun (a,b) ->
+              if b then                     (* atom not excluded *)
+                not (List.mem (Neg a) body)
+              else                          (* atom not included *)
+                not (List.mem (Pos a) body)
+            ) choice
+          then Some (i, cl)
+          else None
         ) unrequired_cls in
+      let ids, cls = List.split (Array.to_list case) in
+      Aux.ints_of_list ids, separation_cond, cls in
+    let cases = List.map rule_case choices in
+    let process_case (ids, separation_cond, case_cls) =
       let case_cls = case_cls @ required_cls in
       let case_rhs, case_conds = List.split case_cls in
       let case_rhs =
@@ -1726,9 +1805,19 @@
           (String.concat " " (List.map literal_str case_conds))
       );
       (* }}} *)
-      case_rhs, counter_cls,
+      let case_cond =
         Aux.unique_sorted (separation_cond @ case_conds) in
-    let res = List.map rule_case choices in
+      let counter_cls = List.map
+        (fun (f, brs) ->
+          let brs = List.map
+            (fun (cond, update) ->
+              let sb, cond = filter_redundant case_cond cond in          
+              subst_literals sb cond, update)
+            brs in
+          f, brs)
+        counter_cls in      
+      ids, (case_rhs, counter_cls, case_cond) in
+    let res = List.map process_case cases in
     (* {{{ log entry *)
     if !debug_level > 2 then (
       let cond_upd_str (cond, update) =
@@ -1738,7 +1827,7 @@
         counter^": "^String.concat ", "
           (List.map cond_upd_str cond_updates) in
       Printf.printf "rule_cases: next clauses partitioned into rules\n%!";
-      let print_case  i (case_rhs, counter_cls, case_cond) =
+      let print_case  i (ids, (case_rhs, counter_cls, case_cond)) =
         Printf.printf "\nRCAND: #%d\nRHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
           (String.concat " " (List.map term_str case_rhs))
           (String.concat "; " (List.map counters_str counter_cls))
@@ -1814,8 +1903,8 @@
   let legal_cls = List.map (* required clauses *)
     (fun body -> ignore_rhs, true, body) legal_conds in
   List.map
-    (fun (case_rhs, updates, case_cond) ->
-      legal_tup, case_rhs, updates, case_cond)
+    (fun (ids, (case_rhs, updates, case_cond)) ->
+      ids, (legal_tup, case_rhs, updates, case_cond))
     (rule_cases counters num_functors static_rels testground program
        playout_states (legal_cls @ next_cls))
 
@@ -1860,12 +1949,18 @@
       used_vars f_paths next_cls `General
       players_wo_env legal_tuples in
   check_timeout "TranslateGame: turnbased_rule_cases: processed rule cands";
-  let rules = Aux.concat_map
-    (add_legal_cond counters num_functors static_rels
-       testground program playout_states) move_tups in
+  let rules = Array.mapi
+    (fun i move_tup ->
+      let res =
+        add_legal_cond counters num_functors static_rels
+          testground program playout_states move_tup in
+      (* marking candidates to not override across legal tups *)
+      List.map (fun (ids, case) ->
+        Aux.Ints.add (~-i - 1) ids, case) res)
+    (Array.of_list move_tups) in
   (* we do not look for the players -- for turn-based case, it's done
      while building game graph *)
-  Aux.Left rules
+  Aux.Left (List.concat (Array.to_list rules))
 
 
 (* If "Concurrent Moves" case, divide rule clauses among players. *)
@@ -1877,7 +1972,7 @@
     process_rule_cands used_vars f_paths next_cls `Environment [||] [[]] in
   let player_rules =
     List.map2 (fun player legal_cls ->
-    (* [process_rule_cands] works with players tuples, so we "cheat" *)
+      (* [process_rule_cands] works with players tuples, so we "cheat" *)
       let legal_tuples = List.map (fun cl -> [cl]) legal_cls in
       let move_tups =
         process_rule_cands
@@ -1887,9 +1982,16 @@
   check_timeout "TranslateGame: concurrent_rule_cases";
   let player_rules = List.map
     (fun (player, move_tups) ->
-      player, Aux.concat_map
-        (add_legal_cond counters num_functors static_rels
-           testground program playout_states) move_tups)
+      let rules = Array.mapi
+        (fun i move_tup ->
+          let res =
+            add_legal_cond counters num_functors static_rels
+              testground program playout_states move_tup in
+          (* marking candidates to not override across legal tups *)
+          List.map (fun (ids, case) ->
+            Aux.Ints.add (~-i - 1) ids, case) res)
+        (Array.of_list move_tups) in
+      player, List.concat (Array.to_list rules))
     (player_rules @ [env_pl_tups]) in
   Aux.Right player_rules
 
@@ -1981,7 +2083,7 @@
     let counters_str (counter, cond_updates) =
       counter^": "^String.concat ", "
         (List.map cond_upd_str cond_updates) in
-    let print_rcand i (_, case_rhs, counter_cls, case_cond) =
+    let print_rcand i (_, (_, case_rhs, counter_cls, case_cond)) =
       Printf.printf "\nRCAND: #%d\nRHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
         (String.concat " " (List.map term_str case_rhs))
         (String.concat "; " (List.map counters_str counter_cls))
@@ -2003,28 +2105,35 @@
 let filter_rule_cands static_rels players f_paths program
     playout_states rule_cands =
   let check_cands cands =
-    List.filter (fun (_, _, _, case_conds) ->
-      (* {{{ log entry *)
-      if !debug_level > 1 then (
-        Printf.printf "check_cands: cond %s%!"
-          (String.concat " "(List.map literal_str case_conds))
-      );
-      (* }}} *)      
-      let res =
-        run_prolog_check_goal (keep_rels static_rels case_conds) program
-        && List.exists
-        (fun state ->
-          (* {{{ log entry *)
-          if !debug_level > 1 then Printf.printf ".%!";
-          (* }}} *)
-          run_prolog_check_goal case_conds
-            (replace_rel_in_program "true" (state_cls state) program))
-        playout_states in
-      (* {{{ log entry *)
-      if !debug_level > 1 then Printf.printf " %B\n%!" res;
-      (* }}} *)      
-      res
-    ) cands in
+    let cands =
+      List.filter (fun (_, (_, _, _, case_conds)) ->
+        (* {{{ log entry *)
+        if !debug_level > 1 then (
+          Printf.printf "check_cands: cond %s%!"
+            (String.concat " "(List.map literal_str case_conds))
+        );
+        (* }}} *)      
+        let res =
+          run_prolog_check_goal (keep_rels static_rels case_conds) program
+          && List.exists
+            (fun state ->
+              (* {{{ log entry *)
+              if !debug_level > 1 then Printf.printf ".%!";
+              (* }}} *)
+              run_prolog_check_goal case_conds
+                (replace_rel_in_program "true" (state_cls state) program))
+            playout_states in
+        (* {{{ log entry *)
+        if !debug_level > 1 then Printf.printf " %B\n%!" res;
+        (* }}} *)      
+        res
+      ) cands in
+    if not !filter_maximal_rules
+    then List.map snd cands
+    else List.map snd
+      (Aux.maximal_unique
+         (fun (s1, _) (s2, _) -> Aux.Ints.subset s1 s2)
+         cands) in
   let add_rhs_as_lhs (legal_tup, case_rhs, updates, case_cond) =
     let case_blanks = List.map
       (fun s -> Pos (True (simult_subst f_paths blank s))) case_rhs in
@@ -2818,8 +2927,12 @@
   let static_base, init_state, c_paths, f_paths, element_reps, root_reps,
     framed_fluents,
     ground_state_terms, arities, term_arities, static_rels, nonstatic_rels,
-    frame_clauses, move_clauses, clauses =
-    prepare_paths_and_elems players_wo_env program ~playout_states clauses in
+    frame_clauses, move_clauses, clauses, program, playout_states =
+    prepare_paths_and_elems players_wo_env ~playout_states clauses in
+  (* recompile the program *)
+  let testground =
+    replace_rel_in_program "true" (state_cls init_state) program  in
+  let program = optimize_program ~testground program in
   let clauses = ground_goal_values ground_state_terms clauses in
   (* [lexp_frame_clauses] have only the "legal" atoms expanded *)
   let lexp_frame_clauses, frame_clauses =
@@ -2864,14 +2977,15 @@
     then elim_ground_args elim_static_rels clauses
     else elim_static_rels, clauses in
   let static_rels = elim_static_rels @ nonelim_static_rels in
-  let nonstatic_rels = Aux.list_diff nonstatic_rels ["goal"; "legal"] in
+  let nonstatic_rels =
+    Aux.list_diff nonstatic_rels ["goal"; "legal"; "next"] in
   let nonstatic_rels, clauses =
     if !perform_ground_arg_elim
     then elim_ground_args nonstatic_rels clauses
     else nonstatic_rels, clauses in
   (* eliminate once again since more variables have been instantiated *)
   let clauses = elim_ground_distinct clauses in
-  let nonstatic_rels = "goal"::"legal"::nonstatic_rels in
+  let nonstatic_rels = "goal"::(* "legal":: *)nonstatic_rels in
   (* {{{ log entry *)
   if !debug_level > 3 then (
     Printf.printf
@@ -2911,8 +3025,9 @@
   (* optimize candidates for fast pruning *)
   let rule_cands =
     let process cands = List.map
-      (fun (legal_tup, rhs_tup, updates, cond) ->
-        legal_tup, rhs_tup, updates, optimize_goal ~testground cond)
+      (fun (ids, (legal_tup, rhs_tup, updates, cond)) ->
+        ids, (legal_tup, rhs_tup, updates,
+              optimize_goal ~testground cond))
       cands in
     match rule_cands with
       | Aux.Left cands -> Aux.Left (process cands)

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-10-25 08:24:28 UTC (rev 1616)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-10-25 21:40:52 UTC (rev 1617)
@@ -45,8 +45,8 @@
 
 let game_test_case ~game_name ~player ~own_plnum ~opponent_plnum
     ~loc0_rule_name ~loc0_emb
-    ~loc0_move ~loc0_noop ~loc1 ~loc1_rule_name ~loc1_emb ~loc1_noop
-    ~loc1_move =
+    ~loc0_move ?loc0_noop ~loc1 ~loc1_rule_name ~loc1_emb ?loc1_noop
+    ~loc1_move () =
   let game = load_rules ("./GGP/examples/"^game_name^".gdl") in
   let gdl, r_game, (r_inl_game, r_struc as res) =
     TranslateGame.translate_game ~playing_as:(Const player) game in
@@ -70,10 +70,13 @@
   let transl =
     TranslateGame.translate_outgoing_move gdl res rname emb in
   assert_equal ~printer:(fun x->x) loc0_move transl;
+  let moves = match loc0_noop with
+    | Some loc0_noop -> [pte loc0_move; pte loc0_noop]
+    | None -> [pte loc0_move] in
   let moves =
     TranslateGame.translate_incoming_move gdl res
       (* FIXME: should use the player ordering "plnum" right? *)
-      [pte loc0_move; pte loc0_noop] in
+      moves 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);
@@ -83,10 +86,13 @@
   let rname = loc1_rule_name in
   let emb =
     Arena.emb_of_names res rname loc1_emb in
+  let moves = match loc1_noop with
+    | Some loc1_noop -> [pte loc1_noop; pte loc1_move]
+    | None -> [pte loc1_move] in
   let moves =
     TranslateGame.translate_incoming_move gdl res
       (* FIXME: should use the player ordering "plnum" right? *)
-      [pte loc1_noop; pte loc1_move] in
+      moves in
   let move = List.assoc opponent_plnum moves in
   assert_equal ~msg:"opponent incoming move"
     ~printer:(emb_str res)
@@ -195,7 +201,7 @@
         ~loc1_emb:[
           "cell_x7_y0__BLANK_", "cell_1_1__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(mark 1 1)"
+        ~loc1_noop:"noop" ~loc1_move:"(mark 1 1)" ()
     );
 
   "tictactoe-different definition" >::
@@ -211,7 +217,7 @@
         ~loc1_emb:[
           "cELL_X10_Y10__BLANK_", "cELL_3_3__BLANK_";
           "cONTROL__BLANK_", "cONTROL__BLANK_"]
-        ~loc1_noop:"NOOP" ~loc1_move:"(MARK 3 3)"
+        ~loc1_noop:"NOOP" ~loc1_move:"(MARK 3 3)" ()
     );
 
   "2player_normal_form_joint" >::
@@ -229,53 +235,7 @@
 ]
 
 let bigtests = "TranslateGameBig" >::: [
-  (* TODO: migrate to use [prepare_relations_and_structure]
-  "connect5 translation data" >::
-    (fun () ->
-      let descr = load_rules ("./GGP/examples/connect5.gdl") in
-      let clauses = GDL.expand_players descr in
-      let program = preprocess_program clauses in
-      let rules,
-        clauses, f_paths, c_paths, root_reps, defined_rels,
-        stable_rels, fluents,
-        init_state, struc, ground_state_terms, elem_term_map =
-        TranslateGame.create_init_struc program ~playout_states:[] clauses in
 
-      assert_equal ~msg:"f_paths" ~printer:(fun x->x)
-        "cell_2; control_0"
-        (String.concat "; "
-           (List.map GDL.path_str (GDL.paths_to_list f_paths)));
-
-      assert_equal ~msg:"c_paths" ~printer:(fun x->x)
-        "cell_0; cell_1"
-        (String.concat "; "
-           (List.map GDL.path_str (GDL.paths_to_list c_paths)));
-
-      assert_equal ~msg:"root_reps" ~printer:(fun x->x)
-        "(cell _BLANK_ _BLANK_ _BLANK_); (control _BLANK_)"
-        (String.concat "; "
-           (List.map GDL.term_str root_reps));
-
-      (* adjacent_cell is a defined relation only because it has
-         large arity: see {!TranslateGame.defined_arity_above}. *)
-      assert_equal ~msg:"defined_rels" ~printer:(fun x->x)
-        "adjacent, adjacent_cell, col, conn5, diag1, diag2, exists_empty_cell, exists_line_of_five, goal, legal, next, row, terminal"
-        (String.concat ", " (List.sort String.compare defined_rels));
-
-      assert_equal ~msg:"fluents" ~printer:(fun x->x)
-        "cell_2b, cell_2o, cell_2x, control_0o, control_0x"
-        (String.concat ", " fluents);
-
-      assert_equal ~msg:"stable_rels" ~printer:(fun x->x)
-        "EQ___cell_0__cell_0, EQ___cell_0__cell_1, EQ___cell_1__cell_0, EQ___cell_1__cell_1, cell_0a, cell_0b, cell_0c, cell_0d, cell_0e, cell_0f, cell_0g, cell_0h, cell_1a, cell_1b, cell_1c, cell_1d, cell_1e, cell_1f, cell_1g, cell_1h, cell__BLANK___BLANK___BLANK_, control__BLANK_, coordinate__cell_0, coordinate__cell_1, nextcol__cell_0__cell_0, nextcol__cell_0__cell_1, nextcol__cell_1__cell_0, nextcol__cell_1__cell_1"
-        (String.concat ", " stable_rels);
-
-      assert_equal ~msg:"structure elements" ~printer:(fun x->x)
-        "cell_a_a__BLANK_, cell_a_b__BLANK_, cell_a_c__BLANK_, cell_a_d__BLANK_, cell_a_e__BLANK_, cell_a_f__BLANK_, cell_a_g__BLANK_, cell_a_h__BLANK_, cell_b_a__BLANK_, cell_b_b__BLANK_, cell_b_c__BLANK_, cell_b_d__BLANK_, cell_b_e__BLANK_, cell_b_f__BLANK_, cell_b_g__BLANK_, cell_b_h__BLANK_, cell_c_a__BLANK_, cell_c_b__BLANK_, cell_c_c__BLANK_, cell_c_d__BLANK_, cell_c_e__BLANK_, cell_c_f__BLANK_, cell_c_g__BLANK_, cell_c_h__BLANK_, cell_d_a__BLANK_, cell_d_b__BLANK_, cell_d_c__BLANK_, cell_d_d__BLANK_, cell_d_e__BLANK_, cell_d_f__BLANK_, cell_d_g__BLANK_, cell_d_h__BLANK_, cell_e_a__BLANK_, cell_e_b__BLANK_, cell_e_c__BLANK_, cell_e_d__BLANK_, cell_e_e__BLANK_, cell_e_f__BLANK_, cell_e_g__BLANK_, cell_e_h__BLANK_, cell_f_a__BLANK_, cell_f_b__BLANK_, cell_f_c__BLANK_, cell_f_d__BLANK_, cell_f_e__BLANK_, cell_f_f__BLANK_, cell_f_g__BLANK_, cell_f_h__BLANK_, cell_g_a__BLANK_, cell_g_b__BLANK_, cell_g_c__BLANK_, cell_g_d__BLANK_, cell_g_e__BLANK_, cell_g_f__BLANK_, cell_g_g__BLANK_, cell_g_h__BLANK_, cell_h_a__BLANK_, cell_h_b__BLANK_, cell_h_c__BLANK_, cell_h_d__BLANK_, cell_h_e__BLANK_, cell_h_f__BLANK_, cell_h_g__BLANK_, cell_h_h__BLANK_, control__BLANK_"
-        (String.concat ", "
-           (List.map (Structure.elem_name struc) (Structure.elements struc)))
-    );
-*)
   "connect5" >::
     (fun () ->
       game_test_case ~game_name:"connect5" ~player:"x"
@@ -289,7 +249,7 @@
         ~loc1_emb:[
           "cell_x6_y6__BLANK_", "cell_f_g__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(mark f g)"
+        ~loc1_noop:"noop" ~loc1_move:"(mark f g)" ()
     );
 
   "breakthrough" >::
@@ -307,7 +267,7 @@
           "cellholds_x7_y9__BLANK_", "cellholds_7_7__BLANK_";
           "cellholds_x8_y10__BLANK_", "cellholds_6_6__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
+        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)" ()
     );
   
   "connect4" >::
@@ -327,7 +287,7 @@
         ~loc1_emb:[
           "cell_c12_y20__BLANK_", "cell_2_2__BLANK_";
           "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(drop 2)";
+        ~loc1_noop:"noop" ~loc1_move:"(drop 2)" ();
       TranslateGame.filter_possibly_redundant := old_filter_possibly_redundant;
     );
 
@@ -357,6 +317,31 @@
       TranslateGame.filter_possibly_redundant := old_filter_possibly_redundant;
     );
 
+  "asteroids-scrambled" >::
+    (fun () ->
+      game_test_case ~game_name:"asteroids-scrambled" ~player:"ship"
+        ~own_plnum:0 ~opponent_plnum:0
+        ~loc0_rule_name:"turn_clock2"
+        ~loc0_emb:[
+          "value___BLANK__old0", "value___BLANK__i10";
+          "value___BLANK__old", "value___BLANK__i10";
+          "value___BLANK__new0", "value___BLANK__i13";
+          "value___BLANK__new", "value___BLANK__i12";
+          "value___BLANK__east", "value___BLANK__east";
+          "gdl__counter", "gdl__counter";
+        ]
+        ~loc0_move:"(turn clock)"
+        ~loc1:0 ~loc1_rule_name:"thrust0"
+        ~loc1_emb:[
+          "gdl__counter", "gdl__counter";
+          "value___BLANK__new", "value___BLANK__i14";
+          "value___BLANK__new0", "value___BLANK__i16";
+          "value___BLANK__old", "value___BLANK__i12";
+          "value___BLANK__old0", "value___BLANK__i13";
+          "value___BLANK__s12", "value___BLANK__i3"]
+        ~loc1_move:"thrust" ();
+    );
+
 ]
 
 let set_debug_level i =
@@ -370,23 +355,27 @@
 
 let a () =
   set_debug_level 4;
-      simult_test_case ~game_name:"pacman3p" ~player:"pacman"
-        ~plnum:1       (* 0 is environment! *)
-        ~moves:[|"(move east)"; "(move nowhere)"; "(move nowhere)"|]
-        ~rules_and_embs:[|
-          "move_east", [
-            "gdl__counter", "gdl__counter";
-            "location__BLANK__x10_y10", "location__BLANK__6_3";
-            "location__BLANK__x_y", "location__BLANK__5_3";
-            "synch_control_", "synch_control_"];
-          "move_nowhere0", [
-            "location__BLANK__x11_y11", "location__BLANK__4_6";
-            "location__BLANK__x12_y12", "location__BLANK__4_6";
-            "synch_control_", "synch_control_"];
-          "move_nowhere1", [
-            "location__BLANK__x13_y13", "location__BLANK__5_6";
-            "location__BLANK__x14_y14", "location__BLANK__5_6";
-            "synch_control_", "synch_control_"]|];
+      game_test_case ~game_name:"asteroids-scrambled" ~player:"ship"
+        ~own_plnum:0 ~opponent_plnum:0
+        ~loc0_rule_name:"turn_clock2"
+        ~loc0_emb:[
+          "value___BLANK__old0", "value___BLANK__i10";
+          "value___BLANK__old", "value___BLANK__i10";
+          "value___BLANK__new0", "value___BLANK__i13";
+          "value___BLANK__new", "value___BLANK__i12";
+          "value___BLANK__east", "value___BLANK__east";
+          "gdl__counter", "gdl__counter";
+        ]
+        ~loc0_move:"(turn clock)"
+        ~loc1:0 ~loc1_rule_name:"thrust0"
+        ~loc1_emb:[
+          "gdl__counter", "gdl__counter";
+          "value___BLANK__new", "value___BLANK__i14";
+          "value___BLANK__new0", "value___BLANK__i16";
+          "value___BLANK__old", "value___BLANK__i12";
+          "value___BLANK__old0", "value___BLANK__i13";
+          "value___BLANK__s12", "value___BLANK__i3"]
+        ~loc1_move:"thrust" ();
   (* failwith "tested"; *)
   ()
 
@@ -433,6 +422,7 @@
   (* regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row"; *)
   (* regenerate ~debug:false ~game_name:"2player_normal_form_joint" ~player:"row"; *)
   (* regenerate ~debug:false ~game_name:"pacman3p" ~player:"pacman"; *)
+  (* regenerate ~debug:true ~game_name:"asteroids-scrambled" ~player:"ship"; *)
   (* failwith "generated"; *)
   ()
 

Added: trunk/Toss/GGP/examples/asteroids-scrambled.gdl
===================================================================
--- trunk/Toss/GGP/examples/asteroids-scrambled.gdl	                        (rev 0)
+++ trunk/Toss/GGP/examples/asteroids-scrambled.gdl	2011-10-25 21:40:52 UTC (rev 1617)
@@ -0,0 +1,316 @@
+; asteroids with position and velocity not using numerals
+(role ship)
+(init (x i10))
+(init (y i10))
+(init (heading north))
+(init (north-speed i3))
+(init (east-speed i2))
+(init (step 1))
+(<= (legal ship thrust))
+(<= (legal ship (turn clock)))
+(<= (legal ship (turn counter)))
+(<= (next (heading ?h))
+    (true (heading ?h))
+    (does ship thrust))
+(<= (next (heading west))
+    (true (heading north))
+    (does ship (turn counter)))
+(<= (next (heading south))
+    (true (heading west))
+    (does ship (turn counter)))
+(<= (next (heading east))
+    (true (heading south))
+    (does ship (turn counter)))
+(<= (next (heading north))
+    (true (heading east))
+    (does ship (turn counter)))
+(<= (next (heading east))
+    (true (heading north))
+    (does ship (turn clock)))
+(<= (next (heading south))
+    (true (heading east))
+    (does ship (turn clock)))
+(<= (next (heading west))
+    (true (heading south))
+    (does ship (turn clock)))
+(<= (next (heading north))
+    (true (heading west))
+    (does ship (turn clock)))
+(<= (next (north-speed ?s))
+    (true (north-speed ?s))
+    (does ship (turn clock)))
+(<= (next (north-speed ?s))
+    (true (north-speed ?s))
+    (does ship (turn counter)))
+(<= (next (north-speed ?s))
+    (true (north-speed ?s))
+    (true (heading east)))
+(<= (next (north-speed ?s))
+    (true (north-speed ?s))
+    (true (heading west)))
+(<= (next (north-speed ?s2))
+    (true (north-speed ?s1))
+    (true (heading north))
+    (does ship thrust)
+    (speed+ ?s1 ?s2))
+(<= (next (north-speed ?s2))
+    (true (north-speed ?s1))
+    (true (heading south))
+    (does ship thrust)
+    (speed- ?s1 ?s2))
+(<= (next (east-speed ?s))
+    (true (east-speed ?s))
+    (does ship (turn clock)))
+(<= (next (east-speed ?s))
+    (true (east-speed ?s))
+    (does ship (turn counter)))
+(<= (next (east-speed ?s))
+    (true (east-speed ?s))
+    (true (heading north)))
+(<= (next (east-speed ?s))
+    (true (east-speed ?s))
+    (true (heading south)))
+(<= (next (east-speed ?s2))
+    (true (east-speed ?s1))
+    (true (heading east))
+    (does ship thrust)
+    (speed+ ?s1 ?s2))
+(<= (next (east-speed ?s2))
+    (true (east-speed ?s1))
+    (true (heading west))
+    (does ship thrust)
+    (speed- ?s1 ?s2))
+(<= (next (x ?new))
+    (true (x ?old))
+    (true (east-speed ?s))
+    (map+ ?old ?s ?new))
+(<= (next (y ?new))
+    (true (y ?old))
+    (true (north-speed ?s))
+    (map+ ?old ?s ?new))
+(<= (next (step ?n++))
+    (true (step ?n))
+    (succ ?n ?n++))
+(<= terminal
+    stopped)
+(<= terminal
+    timeout)
+(<= (goal ship 100)
+    stopped
+    atplanet)
+(<= (goal ship 50)
+    stopped
+    (not atplanet))
+(<= (goal ship 0)
+    (not stopped))
+(<= stopped
+    (true (north-speed i0))
+    (true (east-speed i0)))
+(<= atplanet
+    (true (x i15))
+    (true (y i5)))
+(<= timeout
+    (true (step 50)))
+(map+ i20 i-3 i17)
+(map+ i20 i-2 i18)
+(map+ i20 i-1 i19)
+(map+ i20 i0 i20)
+(map+ i20 i1 i1)
+(map+ i20 i2 i2)
+(map+ i20 i3 i3)
+(map+ i19 i-3 i16)
+(map+ i19 i-2 i17)
+(map+ i19 i-1 i18)
+(map+ i19 i0 i19)
+(map+ i19 i1 i20)
+(map+ i19 i2 i1)
+(map+ i19 i3 i2)
+(map+ i18 i-3 i15)
+(map+ i18 i-2 i16)
+(map+ i18 i-1 i17)
+(map+ i18 i0 i18)
+(map+ i18 i1 i19)
+(map+ i18 i2 i20)
+(map+ i18 i3 i1)
+(map+ i17 i-3 i14)
+(map+ i17 i-2 i15)
+(map+ i17 i-1 i16)
+(map+ i17 i0 i17)
+(map+ i17 i1 i18)
+(map+ i17 i2 i19)
+(map+ i17 i3 i20)
+(map+ i16 i-3 i13)
+(map+ i16 i-2 i14)
+(map+ i16 i-1 i15)
+(map+ i16 i0 i16)
+(map+ i16 i1 i17)
+(map+ i16 i2 i18)
+(map+ i16 i3 i19)
+(map+ i15 i-3 i12)
+(map+ i15 i-2 i13)
+(map+ i15 i-1 i14)
+(map+ i15 i0 i15)
+(map+ i15 i1 i16)
+(map+ i15 i2 i17)
+(map+ i15 i3 i18)
+(map+ i14 i-3 i11)
+(map+ i14 i-2 i12)
+(map+ i14 i-1 i13)
+(map+ i14 i0 i14)
+(map+ i14 i1 i15)
+(map+ i14 i2 i16)
+(map+ i14 i3 i17)
+(map+ i13 i-3 i10)
+(map+ i13 i-2 i11)
+(map+ i13 i-1 i12)
+(map+ i13 i0 i13)
+(map+ i13 i1 i14)
+(map+ i13 i2 i15)
+(map+ i13 i3 i16)
+(map+ i12 i-3 i9)
+(map+ i12 i-2 i10)
+(map+ i12 i-1 i11)
+(map+ i12 i0 i12)
+(map+ i12 i1 i13)
+(map+ i12 i2 i14)
+(map+ i12 i3 i15)
+(map+ i11 i-3 i8)
+(map+ i11 i-2 i9)
+(map+ i11 i-1 i10)
+(map+ i11 i0 i11)
+(map+ i11 i1 i12)
+(map+ i11 i2 i13)
+(map+ i11 i3 i14)
+(map+ i10 i-3 i7)
+(map+ i10 i-2 i8)
+(map+ i10 i-1 i9)
+(map+ i10 i0 i10)
+(map+ i10 i1 i11)
+(map+ i10 i2 i12)
+(map+ i10 i3 i13)
+(map+ i9 i-3 i6)
+(map+ i9 i-2 i7)
+(map+ i9 i-1 i8)
+(map+ i9 i0 i9)
+(map+ i9 i1 i10)
+(map+ i9 i2 i11)
+(map+ i9 i3 i12)
+(map+ i8 i-3 i5)
+(map+ i8 i-2 i6)
+(map+ i8 i-1 i7)
+(map+ i8 i0 i8)
+(map+ i8 i1 i9)
+(map+ i8 i2 i10)
+(map+ i8 i3 i11)
+(map+ i7 i-3 i4)
+(map+ i7 i-2 i5)
+(map+ i7 i-1 i6)
+(map+ i7 i0 i7)
+(map+ i7 i1 i8)
+(map+ i7 i2 i9)
+(map+ i7 i3 i10)
+(map+ i6 i-3 i3)
+(map+ i6 i-2 i4)
+(map+ i6 i-1 i5)
+(map+ i6 i0 i6)
+(map+ i6 i1 i7)
+(map+ i6 i2 i8)
+(map+ i6 i3 i9)
+(map+ i5 i-3 i2)
+(map+ i5 i-2 i3)
+(map+ i5 i-1 i4)
+(map+ i5 i0 i5)
+(map+ i5 i1 i6)
+(map+ i5 i2 i7)
+(map+ i5 i3 i8)
+(map+ i4 i-3 i1)
+(map+ i4 i-2 i2)
+(map+ i4 i-1 i3)
+(map+ i4 i0 i4)
+(map+ i4 i1 i5)
+(map+ i4 i2 i6)
+(map+ i4 i3 i7)
+(map+ i3 i-3 i20)
+(map+ i3 i-2 i1)
+(map+ i3 i-1 i2)
+(map+ i3 i0 i3)
+(map+ i3 i1 i4)
+(map+ i3 i2 i5)
+(map+ i3 i3 i6)
+(map+ i2 i-3 i19)
+(map+ i2 i-2 i20)
+(map+ i2 i-1 i1)
+(map+ i2 i0 i2)
+(map+ i2 i1 i3)
+(map+ i2 i2 i4)
+(map+ i2 i3 i5)
+(map+ i1 i-3 i18)
+(map+ i1 i-2 i19)
+(map+ i1 i-1 i20)
+(map+ i1 i0 i1)
+(map+ i1 i1 i2)
+(map+ i1 i2 i3)
+(map+ i1 i3 i4)
+(speed+ i-3 i-2)
+(speed+ i-2 i-1)
+(speed+ i-1 i0)
+(speed+ i0 i1)
+(speed+ i1 i2)
+(speed+ i2 i3)
+(speed+ i3 i3)
+(speed- i3 i2)
+(speed- i2 i1)
+(speed- i1 i0)
+(speed- i0 i-1)
+(speed- i-1 i-2)
+(speed- i-2 i-3)
+(speed- i-3 i-3)
+(succ 1 2)
+(succ 2 3)
+(succ 3 4)
+(succ 4 5)
+(succ 5 6)
+(succ 6 7)
+(succ 7 8)
+(succ 8 9)
+(succ 9 10)
+(succ 10 11)
+(succ 11 12)
+(succ 12 13)
+(succ 13 14)
+(succ 14 15)
+(succ 15 16)
+(succ 16 17)
+(succ 17 18)
+(succ 18 19)
+(succ 19 20)
+(succ 20 21)
+(succ 21 22)
+(succ 22 23)
+(succ 23 24)
+(succ 24 25)
+(succ 25 26)
+(succ 26 27)
+(succ 27 28)
+(succ 28 29)
+(succ 29 30)
+(succ 30 31)
+(succ 31 32)
+(succ 32 33)
+(succ 33 34)
+(succ 34 35)
+(succ 35 36)
+(succ 36 37)
+(succ 37 38)
+(succ 38 39)
+(succ 39 40)
+(succ 40 41)
+(succ 41 42)
+(succ 42 43)
+(succ 43 44)
+(succ 44 45)
+(succ 45 46)
+(succ 46 47)
+(succ 47 48)
+(succ 48 49)
+(succ 49 50) 

Added: trunk/Toss/GGP/tests/asteroids-scrambled-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/asteroids-scrambled-raw.toss	                        (rev 0)
+++ trunk/Toss/GGP/tests/asteroids-scrambled-raw.toss	2011-10-25 21:40:52 UTC (rev 1617)
@@ -0,0 +1,1189 @@
+REL atplanet() =
+ ex value___BLANK__i15, value___BLANK__i5
+  (true and
+   value__0x(value___BLANK__i15) and value__1i15(value___BLANK__i15) and
+    value___BLANK___BLANK_(value___BLANK__i15) and
+    value__0y(value___BLANK__i5) and value__1i5(value___BLANK__i5) and
+    value___BLANK___BLANK_(value___BLANK__i5))
+REL stopped() =
+ ex value___BLANK__i0, value___BLANK__i0
+  (true and
+   value__0northc45speed(value___BLANK__i0) and
+    value__1i0(value___BLANK__i0) and
+    value___BLANK___BLANK_(value___BLANK__i0) and
+    value__0eastc45speed(value___BLANK__i0) and
+    value__1i0(value___BLANK__i0) and
+    value___BLANK___BLANK_(value___BLANK__i0))
+REL terminal() = (stopped() and true) or (timeout() and true)
+REL timeout() =
+ ex gdl__counter
+  (gdl__counter(gdl__counter) and (:step(gdl__counter) - 50.  = 0) and true)
+PLAYERS ship
+RULE thrust:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+   value___BLANK__old0, value___BLANK__s14 |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old, value___BLANK__s14);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__s14)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s14
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s14
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s14
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old0; value___BLANK__s14
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__s14
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__old;
+      value___BLANK__old0; value___BLANK__s14
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+    value___BLANK__old0, value___BLANK__s14 |
+     value__0eastc45speed (value___BLANK__s14);
+     value__0x (value___BLANK__new); value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    ex value___BLANK__s13, value___BLANK__s15, value___BLANK__west,
+     value___BLANK__s16
+     (value__0eastc45speed(value___BLANK__s13) and
+      value___BLANK___BLANK_(value___BLANK__s13) and
+      value__0eastc45speed(value___BLANK__s15) and
+      value___BLANK___BLANK_(value___BLANK__s15) and
+      value__0northc45speed(value___BLANK__s16) and
+      value___BLANK___BLANK_(value___BLANK__s16) and
+      value__0heading(value___BLANK__west) and
+      value__1west(value___BLANK__west) and
+      value___BLANK___BLANK_(value___BLANK__west) and
+      speedc45(value___BLANK__s13, value___BLANK__s14) and
+      mapc43(value___BLANK__old, value___BLANK__s15, value___BLANK__new) and
+      mapc43(value___BLANK__old0, value___BLANK__s16, value___BLANK__new0)))
+RULE thrust0:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+   value___BLANK__old0, value___BLANK__s12 |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old, value___BLANK__s12);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__s12)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s12
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s12
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s12
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old0; value___BLANK__s12
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__s12
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__old;
+      value___BLANK__old0; value___BLANK__s12
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+    value___BLANK__old0, value___BLANK__s12 |
+     value__0eastc45speed (value___BLANK__s12);
+     value__0x (value___BLANK__new); value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    ex value___BLANK__s11, value___BLANK__s15, value___BLANK__east,
+     value___BLANK__s16
+     (value__0heading(value___BLANK__east) and
+      value__1east(value___BLANK__east) and
+      value___BLANK___BLANK_(value___BLANK__east) and
+      value__0eastc45speed(value___BLANK__s11) and
+      value___BLANK___BLANK_(value___BLANK__s11) and
+      value__0eastc45speed(value___BLANK__s15) and
+      value___BLANK___BLANK_(value___BLANK__s15) and
+      value__0northc45speed(value___BLANK__s16) and
+      value___BLANK___BLANK_(value___BLANK__s16) and
+      speedc43(value___BLANK__s11, value___BLANK__s12) and
+      mapc43(value___BLANK__old, value___BLANK__s15, value___BLANK__new) and
+      mapc43(value___BLANK__old0, value___BLANK__s16, value___BLANK__new0)))
+RULE thrust1:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+   value___BLANK__old0, value___BLANK__s6 |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old, value___BLANK__s6);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__s6)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s6
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s6
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s6
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old0; value___BLANK__s6
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__s6
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__old;
+      value___BLANK__old0; value___BLANK__s6
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+    value___BLANK__old0, value___BLANK__s6 |
+     value__0northc45speed (value___BLANK__s6);
+     value__0x (value___BLANK__new); value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    ex value___BLANK__s15, value___BLANK__south, value___BLANK__s16,
+     value___BLANK__s5
+     (value__0eastc45speed(value___BLANK__s15) and
+      value___BLANK___BLANK_(value___BLANK__s15) and
+      value__0northc45speed(value___BLANK__s16) and
+      value___BLANK___BLANK_(value___BLANK__s16) and
+      value__0northc45speed(value___BLANK__s5) and
+      value___BLANK___BLANK_(value___BLANK__s5) and
+      value__0heading(value___BLANK__south) and
+      value__1south(value___BLANK__south) and
+      value___BLANK___BLANK_(value___BLANK__south) and
+      speedc45(value___BLANK__s5, value___BLANK__s6) and
+      mapc43(value___BLANK__old, value___BLANK__s15, value___BLANK__new) and
+      mapc43(value___BLANK__old0, value___BLANK__s16, value___BLANK__new0)))
+RULE thrust2:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+   value___BLANK__old0, value___BLANK__s4 |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old, value___BLANK__s4);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__s4)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s4
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s4
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__s4
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old0; value___BLANK__s4
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__s4
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__old;
+      value___BLANK__old0; value___BLANK__s4
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+    value___BLANK__old0, value___BLANK__s4 |
+     value__0northc45speed (value___BLANK__s4);
+     value__0x (value___BLANK__new); value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    ex value___BLANK__s15, value___BLANK__north, value___BLANK__s16,
+     value___BLANK__s3
+     (value__0heading(value___BLANK__north) and
+      value__1north(value___BLANK__north) and
+      value___BLANK___BLANK_(value___BLANK__north) and
+      value__0eastc45speed(value___BLANK__s15) and
+      value___BLANK___BLANK_(value___BLANK__s15) and
+      value__0northc45speed(value___BLANK__s16) and
+      value___BLANK___BLANK_(value___BLANK__s16) and
+      value__0northc45speed(value___BLANK__s3) and
+      value___BLANK___BLANK_(value___BLANK__s3) and
+      speedc43(value___BLANK__s3, value___BLANK__s4) and
+      mapc43(value___BLANK__old, value___BLANK__s15, value___BLANK__new) and
+      mapc43(value___BLANK__old0, value___BLANK__s16, value___BLANK__new0)))
+RULE turn_clock:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0,
+   value___BLANK__north, value___BLANK__old, value___BLANK__old0 |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__north);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__north)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__north; value___BLANK__old; value___BLANK__old0
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__north; value___BLANK__old; value___BLANK__old0
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__north; value___BLANK__old; value___BLANK__old0
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__north; value___BLANK__old0
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__north; value___BLANK__old
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0); value__1north (value___BLANK__north);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__north;
+      value___BLANK__old; value___BLANK__old0
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0,
+    value___BLANK__north, value___BLANK__old, value___BLANK__old0 |
+     value__0heading (value___BLANK__north); value__0x (value___BLANK__new);
+     value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    not
+     ex value___BLANK__east, value___BLANK__south
+      (value__0heading(value___BLANK__north) or
+       (value__0heading(value___BLANK__east) and
+        value__1east(value___BLANK__east) and
+        value___BLANK___BLANK_(value___BLANK__east)) or
+       (value__0heading(value___BLANK__south) and
+        value__1south(value___BLANK__south) and
+        value___BLANK___BLANK_(value___BLANK__south))) and
+    ex value___BLANK__s15, value___BLANK__west, value___BLANK__s16
+     (value__0eastc45speed(value___BLANK__s15) and
+      value___BLANK___BLANK_(value___BLANK__s15) and
+      value__0northc45speed(value___BLANK__s16) and
+      value___BLANK___BLANK_(value___BLANK__s16) and
+      value__0heading(value___BLANK__west) and
+      value__1west(value___BLANK__west) and
+      value___BLANK___BLANK_(value___BLANK__west) and
+      mapc43(value___BLANK__old, value___BLANK__s15, value___BLANK__new) and
+      mapc43(value___BLANK__old0, value___BLANK__s16, value___BLANK__new0)))
+RULE turn_clock0:
+ [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+   value___BLANK__old0, value___BLANK__west |
+    _nondistinct_ {
+     (value___BLANK__old, value___BLANK__new);
+      (value___BLANK__old, value___BLANK__new0);
+      (value___BLANK__old, value___BLANK__old0);
+      (value___BLANK__old, value___BLANK__west);
+      (value___BLANK__old0, value___BLANK__new);
+      (value___BLANK__old0, value___BLANK__new0);
+      (value___BLANK__old0, value___BLANK__west)
+     };
+    _opt_value__0eastc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__west
+     };
+    _opt_value__0heading {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__west
+     };
+    _opt_value__0northc45speed {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__old0; value___BLANK__west
+     };
+    _opt_value__0x {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old0; value___BLANK__west
+     };
+    _opt_value__0y {
+     gdl__counter; value___BLANK__new; value___BLANK__new0;
+      value___BLANK__old; value___BLANK__west
+     };
+    gdl__counter (gdl__counter); value__0x (value___BLANK__old);
+    value__0y (value___BLANK__old0); value__1west (value___BLANK__west);
+    value___BLANK___BLANK_ {
+     value___BLANK__new; value___BLANK__new0; value___BLANK__old;
+      value___BLANK__old0; value___BLANK__west
+     }
+   | 
+  ] ->
+  [gdl__counter, value___BLANK__new, value___BLANK__new0, value___BLANK__old,
+    value___BLANK__old0, value___BLANK__west |
+     value__0heading (value___BLANK__west); value__0x (value___BLANK__new);
+     value__0y (value___BLANK__new0)
+    | 
+  ]
+  emb value__0eastc45speed, value__0heading, value__0northc45speed,
+   value__0x, value__0y
+  update
+  :step(gdl__counter) =
+   :((true and true)) * (1. * (:step(gdl__counter) - 48.) + 49.)
+  pre
+   (not terminal() and
+    not
+     ex value___BLANK__east, value___BLANK__north
+      (value__0heading(value___BLANK__west) or
+       (value__0heading(value___BLANK__east) and
+        value__1east(value___BLANK__east) and
+        value___BLANK___BLANK_(value___BLANK__east)) or
+       (value__0heading(value___...
 
[truncated message content]