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

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

Revision: 1561
          http://toss.svn.sourceforge.net/toss/?rev=1561&view=rev
Author:   lukstafi
Date:     2011-09-09 11:12:21 +0000 (Fri, 09 Sep 2011)
Log Message:
-----------
GDL translation: handling counters updated by arbitrary numeric functions, both specification and implementation; small related fixes in reference.tex. ContinuousRule and Formula: switching dynamics updates (but not evolution) from Term.term to Formula.real_expr. FormulaOps: generating piecewise linear expressions from function graphs. TranslateGame[Test]: small fixes to concurrent games.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/Arena/ArenaParser.mly
    trunk/Toss/Arena/ContinuousRule.ml
    trunk/Toss/Arena/ContinuousRule.mli
    trunk/Toss/Arena/ContinuousRuleParser.mly
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/Formula.mli
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Formula/FormulaParser.mly
    trunk/Toss/Formula/FormulaSubst.ml
    trunk/Toss/Formula/FormulaSubst.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/Arena.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -582,7 +582,8 @@
        ContinuousRule.rule)
       (* Set a rule as given *)
   | GetRule of string                              (* Get a rule as string *)
-  | SetRuleUpd of string*string *string *Term.term (* Set a rule update eq *)
+  | SetRuleUpd of string * string * string * Formula.real_expr
+  (* Set a rule update eq *)
   | GetRuleUpd of string * string * string         (* Get a rule update eq *)
   | SetRuleDyn of string*string *string *Term.term (* Set a rule dynamics eq *)
   | GetRuleDyn of string * string * string         (* Get a rule dynamics eq *)
@@ -862,17 +863,17 @@
     | GetRule (r_name) ->
       let msg = get_from_rule ContinuousRule.str r_name state_game "get rule" in
       ((state_game, state),  msg)
-    | SetRuleUpd (r_name, f, elem_name, term) ->
+    | SetRuleUpd (r_name, f, elem_name, expr) ->
       let set_upd r =
         let new_upd =
-          Aux.replace_assoc (f,elem_name) term r.ContinuousRule.update in
+          Aux.replace_assoc (f,elem_name) expr r.ContinuousRule.update in
         { r with ContinuousRule.update = new_upd }, "UPDATE SET" in
       apply_to_rule set_upd r_name (state_game, state) "set rule upd"
     | GetRuleUpd (r_name, f, elem_name) ->
       let get_upd r =
         try
           let upd = List.assoc (f,elem_name) r.ContinuousRule.update in
-          Term.str upd
+          Formula.real_str upd
         with Not_found -> "0.0" in
       ((state_game, state),
        get_from_rule get_upd r_name state_game "get rule upd")

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/Arena.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -209,7 +209,8 @@
        ContinuousRule.rule)
       (** Set a rule as given *)
   | GetRule of string                              (** Get a rule as string *)
-  | SetRuleUpd of string*string *string *Term.term (** Set a rule update eq *)
+  | SetRuleUpd of string * string * string * Formula.real_expr
+  (** Set a rule update eq *)
   | GetRuleUpd of string * string * string         (** Get a rule update eq *)
   | SetRuleDyn of string*string *string *Term.term (** Set a rule dynamics eq *)
   | GetRuleDyn of string * string * string         (** Get a rule dynamics eq *)

Modified: trunk/Toss/Arena/ArenaParser.mly
===================================================================
--- trunk/Toss/Arena/ArenaParser.mly	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/ArenaParser.mly	2011-09-09 11:12:21 UTC (rev 1561)
@@ -222,7 +222,7 @@
     time = FLOAT
     params = separated_list (COMMA, separated_pair (ID, COLON, FLOAT))
       { ApplyRule (r, mtch, time, params) }
-  | SET_CMD RULE_SPEC UPDATE r=id_int fn=ID elem=id_int upd=term_expr
+  | SET_CMD RULE_SPEC UPDATE r=id_int fn=ID elem=id_int upd=real_expr
     { SetRuleUpd (r, fn, elem, upd) }
   | GET_CMD RULE_SPEC UPDATE r=id_int fn=ID elem=id_int
     { GetRuleUpd (r, fn, elem) }

Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/ContinuousRule.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -14,7 +14,8 @@
   discrete  : DiscreteRule.rule;                    (* The discrete part *)
   compiled  : DiscreteRule.rule_obj ;               (* Compiled discrete part *)
   dynamics  : ((string * string) * Term.term) list; (* Equation system calD *)
-  update    : ((string * string) * Term.term) list; (* Update equations calT *)
+  update    : ((string * string) * Formula.real_expr) list;
+  (* Update equations calT *)
   (* Note that, for efficiency, the precondition is part of DiscreteRule. *)
   inv       : Formula.formula;     (* Invariant for the evolution *)
   post      : Formula.formula;     (* Postcondition for application *)
@@ -101,12 +102,15 @@
   if !debug_level > 1 then print_endline ("ct: " ^ (string_of_float !time));
   let left_elname le =
     Structure.elem_str r.discrete.DiscreteRule.lhs_struc le in
+  let p_vars, p_vals = List.split params in
   let subst_params tm = 
-    let (p_vars, p_vals) = List.split params in
     List.hd
       (Term.subst_simp p_vars (List.map (fun f -> Term.Const f) p_vals) [tm]) in
+  let re_sb = List.map
+    (fun (p,v) -> p, Formula.Const v) params in
   let dyn = List.map (fun (lhs, rhs) -> (lhs, subst_params rhs)) r.dynamics in
-  let upd = List.map (fun (lhs, rhs) -> (lhs, subst_params rhs)) r.update in
+  let upd = List.map (fun (lhs, rhs) ->
+    (lhs, FormulaSubst.subst_real re_sb rhs)) r.update in
   let init_vals = 
     let get_val f a =
       (* LHS is embedded in the model *)
@@ -160,11 +164,20 @@
     f, Structure.elem_str struc i in
   let all_vals_assoc =
     select_pos (List.map lhs_to_model_str dyn) (List.rev !all_vals) in
+  (*
   let val_map = 
     if !cur_vals = [] then List.combine (List.map fst dyn) init_vals
     else List.combine (List.map fst dyn) !cur_vals in
-  let upd_vals = Term.eq_vals (Term.subst_simp_eq 
-				 [("t", Term.Const !time)] val_map upd) in
+  let upd_vals = Term.eq_vals
+    (Term.subst_simp_eq [("t", Term.Const !time)] val_map upd) in
+  *)
+  let upd = List.map (fun (lhs, rhs) ->
+    (lhs, FormulaSubst.subst_real ["t", Formula.Const !time] rhs)) upd in
+  (* we don't need to use val_map because !last_struc contains the
+     evolved values *)
+  let upd_vals = List.map
+    (fun (lhs,expr) -> lhs, Solver.M.get_real_val expr !last_struc)
+    upd in
   (* we pass the evolved structure to discrete rewriting, so that
      function values can be copied to new elements in case they are
      not updated later *)
@@ -209,10 +222,10 @@
 let str r =
   let dyn_str = 
     if r.dynamics = [] then "" else "\ndynamics\n" ^
-          Term.eq_str ~diff:true r.dynamics in
+      Term.eq_str ~diff:true r.dynamics in
   let upd_str = 
     if r.update = [] then "" else "\nupdate\n" ^ (
-            Term.eq_str r.update
+      Formula.eq_str r.update
     ) ^ "\n" in
   let pre_str = " pre " ^ (Formula.str r.discrete.DiscreteRule.pre) in
   let inv_str = " inv " ^ (Formula.str r.inv) in
@@ -234,7 +247,7 @@
       (Term.fprint_eqs ~diff:true) r.dynamics;
   if has_update r then
     Format.fprintf f "@ @[<hv>update@ %a@]"
-      (Term.fprint_eqs ~diff:false) r.update;
+      (Formula.fprint_eqs ~diff:false) r.update;
   if print_compiled then
     Format.fprintf f "@ @[<1>compiled@ %a@]"
       DiscreteRule.fprint_rule_obj r.compiled;

Modified: trunk/Toss/Arena/ContinuousRule.mli
===================================================================
--- trunk/Toss/Arena/ContinuousRule.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/ContinuousRule.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -9,15 +9,13 @@
 (** Specification of a continuous rewriting rule, as in modelling document.
    Function named foo on element i is, in a term, given by variable foo_i. *)
 type rule = {
-  discrete  : DiscreteRule.rule;                    (** The discrete part *)
-  compiled  : DiscreteRule.rule_obj ;               (** Compiled discrete part *)
-  dynamics  : ((string * string) * Term.term) list; (** Equation system calD *)
-  update    : ((string * string) * Term.term) list; (** Update equations calT *)
+  discrete  : DiscreteRule.rule;        (** The discrete part *)
+  compiled  : DiscreteRule.rule_obj ;   (** Compiled discrete part *)
+  dynamics  : Term.eq_sys;              (** Equation system calD *)
+  update    : Formula.eq_sys;           (** Update equations calT *)
   (** Note that, for efficiency, the precondition is part of DiscreteRule. *)
-  inv       : Formula.formula;     (** Invariant for the evolution *)
-  (** Optimized invariant *)
-  post      : Formula.formula;     (** Postcondition for application *)
-  (** Optimized postcondition *)
+  inv       : Formula.formula;    (** Invariant for the evolution *)
+  post      : Formula.formula;    (** Postcondition for application *)
 }
 
 (** Create a continuous rule given a named discrete rule and other params. *)
@@ -25,7 +23,7 @@
   (string * int) list ->                             (** signature *)
   (string * (string list * Formula.formula)) list -> (** defined rels *)
   (DiscreteRule.rule) ->
-  Term.eq_sys -> Term.eq_sys ->
+  Term.eq_sys -> Formula.eq_sys ->
   ?pre:Formula.formula -> ?inv:Formula.formula ->
   ?post:Formula.formula -> unit -> rule
 

Modified: trunk/Toss/Arena/ContinuousRuleParser.mly
===================================================================
--- trunk/Toss/Arena/ContinuousRuleParser.mly	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Arena/ContinuousRuleParser.mly	2011-09-09 11:12:21 UTC (rev 1561)
@@ -18,7 +18,7 @@
 %public rule_expr:
   | discr = discrete_rule_expr
     dyn  = loption (preceded (DYNAMICS, eq_sys))
-    upd  = loption (preceded (UPDATE, eq_sys))
+    upd  = loption (preceded (UPDATE, expr_eq_sys))
     pre  = option (preceded (PRE, formula_expr))
     inv  = option (preceded (INV, formula_expr))
     post = option (preceded (POST, formula_expr))

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/Formula.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -259,6 +259,25 @@
 let str = sprint
 let real_str = sprint_real
 
+type eq_sys = ((string * string) * real_expr) list
+
+(* Print an equation system. *)
+let fprint_eqs ?(diff=false) ppf eqs =
+  let sing ppf ((f, a), t) = 
+    let mid_str = if diff then "'" else "" in
+    Format.fprintf ppf "@[<1>%s(%s)%s@ =@ @[<1>%a@]@]"
+      f a mid_str fprint_real t in
+  Format.fprintf ppf "@[<hv>%a@]" (Aux.fprint_sep_list ";" sing) eqs
+
+(* Print an equation system as a string. *)
+let eq_str ?(diff=false) eqs =
+  let sing_str ((f, a), t) = 
+    let mid_str = if diff then "' = " else " = " in
+    let l_str = real_str (Fun (f, `FO a)) in
+    let r_str = real_str t in
+    l_str ^ mid_str ^ r_str in
+  "  " ^ (String.concat ";\n  " (List.map sing_str eqs))
+
 (* ------------------------ ORDER ON FORMULAS ------------------------------- *)
 
 (* Compare two variables. We assume that FO < MSO < SO < Real. *)

Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/Formula.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -82,6 +82,10 @@
 
 val is_atom : formula -> bool
 
+(** Equation system: a left-hand-side [f,a] actually represents
+    [Fun (f, `FO a)] *)
+type eq_sys = ((string * string) * real_expr) list
+
 (** {2 Printing Functions} *)
 
 (** Print a variable as a string. *)
@@ -106,6 +110,9 @@
 val fprint_prec : int -> Format.formatter -> formula -> unit
 val fprint_real_prec : int -> Format.formatter -> real_expr -> unit
 
+(** Print an equation system. *)
+val fprint_eqs : ?diff : bool -> Format.formatter -> eq_sys -> unit
+val eq_str : ?diff:bool -> eq_sys -> string
 
 (** {2 Formula syntax check} *)
 

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -1024,3 +1024,49 @@
   let tnf_lfp fprel fpvs fpdef = Lfp (fprel, fpvs, tnf_fv_nofp ?sizes fpdef) in
   let psi = map_formula { identity_map with map_Lfp = tnf_lfp } phi in
   tnf_fv_nofp ?sizes psi
+
+
+(* ------------------------------- Reals ----------------------------------- *)
+
+let l_then x y e =
+  Times (Char (RealExpr (Plus (x, Times (Const (-1.), y)),
+                         LZero)), e)
+let geq_then x y e =
+  Times (Char (RealExpr (Plus (x, Times (Const (-1.), y)),
+                         GEQZero)), e)
+let diff a b = Plus (a, Times (Const (-1.), b))
+
+(* Generate a piecewise-linear function of a given argument from a
+   graph. Raise [Failure "piecewise_linear"] if first elements of
+   the graph are not unique or graph is empty. *)
+let piecewise_linear arg graph =
+  let domain = List.sort Pervasives.compare (List.map fst graph) in
+  let slope begp endp =
+    (List.assoc endp graph -. List.assoc begp graph) /.
+      (endp -. begp) in
+  let affine begp endp =
+    Plus (Times (Const (slope begp endp), diff arg (Const begp)),
+          Const (List.assoc begp graph)) in
+  let rec step old_begp old_slope = function
+    | [] | [_] -> assert false
+    | [begp; endp] when begp = endp -> failwith "piecewise_linear"
+    | [begp; endp] when old_slope = slope begp endp -> affine begp endp
+    | [begp; endp] ->
+      Plus (l_then arg (Const begp) (affine old_begp begp),
+            geq_then arg (Const begp) (affine begp endp))
+    | begp::endp::_ when begp = endp -> failwith "piecewise_linear"
+    | begp::endp::more when old_slope = slope begp endp ->
+      step old_begp old_slope (endp::more)
+    | begp::endp::more ->
+      Plus (l_then arg (Const begp) (affine old_begp begp),
+            geq_then arg (Const endp)
+              (step begp (slope begp endp) (endp::more))) in
+  match domain with
+    | [] -> failwith "piecewise_linear"
+    | [endp] -> Const endp
+    | [begp; endp] when begp = endp -> failwith "piecewise_linear"
+    | [begp; endp] -> affine begp endp
+    | begp::endp::_ when begp = endp -> failwith "piecewise_linear"
+    | begp::endp::more -> step begp (slope begp endp) (endp::more)
+
+

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -85,6 +85,13 @@
 val to_cnf : formula -> formula list
 
 
+(** {2 Reals} *)
+
+(** Generate a piecewise-linear function of a given argument from a
+    graph. Raise [Failure "piecewise_linear"] if first elements of
+    the graph are not unique or graph is empty. *)
+val piecewise_linear : real_expr -> (float * float) list -> real_expr
+
 (** {2 Debugging} *)
 
 (** Debugging information. At level 0 nothing is printed out. *)

Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/FormulaParser.mly	2011-09-09 11:12:21 UTC (rev 1561)
@@ -14,12 +14,13 @@
     try so_var_of_string s with Failure s -> raise (Parsing_error s)
 %}
 
-%start parse_formula parse_real_expr
+%start parse_formula parse_real_expr parse_expr_eqs
 %type <Formula.formula> parse_formula formula_expr
 %type <Formula.var list> var_list
 %type <Formula.fo_var list> fo_var_list
 %type <Formula.real_expr> parse_real_expr real_expr
 %type <Formula.real_expr * Formula.sign_op> real_ineq
+%type <Formula.eq_sys> parse_expr_eqs expr_eq_sys
 
 
 %%
@@ -122,6 +123,19 @@
       { Let (rel, args, body, phi) }
 
 
+expr_eq_expr: /* we do not distinguish standard and differential equations here */
+  | ID OPEN ID CLOSE EQ real_expr             { (($1, $3), $6) }
+  | ID OPEN INT CLOSE EQ real_expr            { (($1, string_of_int $3), $6) }
+  | ID OPEN ID CLOSE APOSTROPHE EQ real_expr  { (($1, $3), $7) }
+  | ID OPEN INT CLOSE APOSTROPHE EQ real_expr { (($1, string_of_int $3), $7) }
+
+%public expr_eq_sys:
+  | expr_eq_expr                        { [$1] }
+  | expr_eq_expr SEMICOLON expr_eq_sys  { $1 :: $3 }
+
+parse_expr_eqs:
+    expr_eq_sys EOF { $1 };
+
 parse_formula:
   formula_expr EOF 
   { if Formula.syntax_ok $1 then $1 else 

Modified: trunk/Toss/Formula/FormulaSubst.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubst.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/FormulaSubst.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -107,7 +107,11 @@
       Sum(vs, subst_vars new_vs phi, subst_vars_expr new_vs r)
   | RLet _ -> failwith "FormulaSubst:subst_vars_expr: rlet substitution"
 
+let subst_real subst = FormulaMap.map_real_expr
+  {FormulaMap.identity_map with FormulaMap.map_RVar =
+      (fun v -> try List.assoc v subst with Not_found -> RVar v)}
 
+
 (* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
 
 (* Substitute in relations defined in [defs] by their definitions. *)

Modified: trunk/Toss/Formula/FormulaSubst.mli
===================================================================
--- trunk/Toss/Formula/FormulaSubst.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/Formula/FormulaSubst.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -16,6 +16,9 @@
 val subst_vars : (string * string) list -> formula -> formula
 val subst_vars_expr : (string * string) list -> real_expr -> real_expr
 
+(** Substitute a real variable with a subexpression. *)
+val subst_real : (string * real_expr) list -> real_expr -> real_expr
+
 (** Substitute once relations in [defs] by corresponding subformulas
    (with instantiated parameters). *)
 val subst_once_rels : 

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/GGP/GDL.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -152,6 +152,9 @@
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map clause_vars cls)
 
+let literals_vars lits =
+  clause_vars (("",[| |]), lits)
+
 let defs_of_rules rules =
   Aux.map_reduce (fun ((rel, args), body, neg_body) ->
     rel, (args, body, neg_body)) (fun y x->x::y) [] rules

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/GGP/GDL.mli	2011-09-09 11:12:21 UTC (rev 1561)
@@ -53,6 +53,7 @@
 val terms_vars : term array -> Aux.Strings.t
 val clause_vars : clause -> Aux.Strings.t
 val clauses_vars : clause list -> Aux.Strings.t
+val literals_vars : literal list -> Aux.Strings.t
 
 val defs_of_rules : gdl_rule list -> gdl_defs
 val rules_of_clause : clause -> gdl_rule list

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -710,14 +710,88 @@
   in
   List.filter keep literals
 
+
+let counter_path_partition num_functors counter_cands (arg, body) =
+  (* search backwards *)
+  let roots = Aux.map_some
+    (function
+      | Pos (True (Func (f, [|r|]))) as a
+          when List.mem f counter_cands -> Some (r, a)
+      | _ -> None)
+    body in
+  let rec find_path acc point =
+    if List.mem_assoc point roots
+    then List.assoc point roots::acc
+    else
+      let revcands = Aux.map_some
+        (function
+          | Pos (Rel (rel, [|x; y|])) as a
+              when y=point && List.mem rel num_functors ->
+            Some (x, a)
+          | _ -> None)
+        body in
+      match revcands with
+        | [next, edge] ->
+          find_path (edge::acc) next
+        | _ -> raise Not_found in
+  match arg with
+    | Const c when
+        (try ignore (float_of_string c); true
+         with Failure "float_of_string" -> false) ->
+      [Pos (True arg)], body
+    | Var _ as v ->
+      let path = find_path [] v in
+      path, Aux.list_diff body path
+    | _ -> raise Not_found
+
+
+let split_counter_rule_cls counters num_functors rule_cls =
+  let counter_cls, rule_cls = Aux.partition_map
+    (function
+      | Func (f, [|h|]), _, body when List.mem f counters ->
+        Aux.Left (f, h, body)
+      | cl -> Aux.Right cl)
+    rule_cls in
+  let counter_cls = Array.mapi
+    (fun i (f, h, body) ->
+      let update, cond =
+        counter_path_partition num_functors counters (h, body) in
+      (i, update),
+      (Func ("_COUNTER_CL_", [|Const (string_of_int i); Const f|]),
+       false, cond))
+    (Array.of_list counter_cls) in
+  let counter_upds, counter_cls =
+    List.split (Array.to_list counter_cls) in
+  counter_upds, counter_cls @ rule_cls
+   
+
+let counter_updates_and_preconds counters counter_upds case_cls =
+  let counter_cls, case_cls = Aux.partition_map
+    (function
+      | Func ("_COUNTER_CL_", [|Const i; Const f|]), body ->
+        Aux.Left (int_of_string i, f, body)
+      | cl -> Aux.Right cl)
+    case_cls in
+  let updates, counter_cls = List.split
+    (List.map
+       (fun (i, f, body) -> (f, List.assoc i counter_upds),
+         (ignore_rhs, body)) counter_cls) in
+  updates, counter_cls @ case_cls
+       
+
 (* Assign rule clauses to rule cases, i.e. candidates for Toss
-   rules. Collect the conditions and RHS state terms together.  Frame
+   rules. Collect the conditions and RHS state terms together. Frame
    clauses are already processed into erasure clauses. Rule clauses
    should contain the "legal" clauses with heads replaced by
    "_IGNORE_RHS_" terms which will be discarded later; "legal" clauses
    and "next" clauses that contained "does" atoms should be marked as
    required.
 
+   We preprocess the clauses by splitting the counter clauses into
+   update calculation and remaining clause condition, remembering the
+   association between the two, and adding back the counter clauses
+   (condintions) as unrequired.
+
    We call atoms or literals "deterministic" if they are not under
    disjunction. First we collect deterministic literals of required
    clauses, and remove unrequired clauses that have deterministic
@@ -734,11 +808,20 @@
    unrequired clauses that have no literals disagreeing with the sign
    assignment.
 
+   After the "partitioned" candidates are produced, we collect the
+   "RHSes" from clause heads removing "_IGNORE_RHS_" and removing
+   heads marking counter clauses, but putting in the update
+   calculations corresponding to counter clauses that made it into the
+   candidate case.
+
    TODO: unrequired clauses with disjunctions may avoid being
    excluded. If this poses problems we might need to expand
    disjunctions containing potentially case-split atoms.
 *)
-let rule_cases static_rels program playout_states rule_cls =
+let rule_cases counters num_functors static_rels program
+    playout_states rule_cls =
+  let counter_upds, rule_cls =
+    split_counter_rule_cls counters num_functors rule_cls in
   let required_cls = Aux.map_some
     (fun (h, required, body) ->
       if required then Some (h, body) else None) rule_cls in
@@ -795,6 +878,10 @@
          | _ -> None) body) unrequired_cls) in
   let split_atoms = Aux.list_diff unreq_atoms req_atoms in
   if split_atoms = [] then                    (* single partition *)
+    let updates, unrequired_cls =
+      (* also replace counter cl heads with [ignore_rhs] *)
+      counter_updates_and_preconds counters
+        counter_upds unrequired_cls in
     let rule_cls = required_cls @ unrequired_cls in
     let case_rhs, case_conds = List.split rule_cls in
     let case_rhs = Aux.list_remove ignore_rhs case_rhs in
@@ -803,7 +890,7 @@
       Printf.printf "rule_cases: single partition\n%!";
     );
     (* }}} *)
-    [Aux.unique_sorted case_rhs,
+    [Aux.unique_sorted case_rhs, updates,
      Aux.unique_sorted (List.concat case_conds)]
   else
     let patterns =
@@ -850,6 +937,10 @@
               not (List.mem (Pos a) body)
           ) choice
         ) unrequired_cls in
+      let updates, case_cls =
+        (* also replace counter cl heads with [ignore_rhs] *)
+        counter_updates_and_preconds counters
+          counter_upds case_cls in
       let case_cls = case_cls @ required_cls in
       let case_rhs, case_conds = List.split case_cls in
       let case_rhs =
@@ -858,21 +949,30 @@
         Aux.unique_sorted (List.concat case_conds) in
       (* {{{ log entry *)
       if !debug_level > 3 then (
-        Printf.printf "\nRCAND:\nsep_cond: %s\nRHS: %s\ncase_conds: %s\n\n%!"
+        let update_str (counter, update) =
+          counter^": "^
+            String.concat " " (List.map literal_str update) in
+        Printf.printf
+          "\nRCAND:\nsep_cond: %s\nRHS: %s\nUPDATEs: %s\ncase_conds: %s\n\n%!"
           (String.concat " " (List.map literal_str separation_cond))
           (String.concat " " (List.map term_str case_rhs))
+          (String.concat "; " (List.map update_str updates))
           (String.concat " " (List.map literal_str case_conds))
       );
       (* }}} *)
-      case_rhs,
+      case_rhs, updates,
         Aux.unique_sorted (separation_cond @ case_conds) in
     let res = List.map rule_case choices in
     (* {{{ log entry *)
     if !debug_level > 2 then (
+      let update_str (counter, update) =
+        counter^": "^
+          String.concat " " (List.map literal_str update) in
       Printf.printf "rule_cases: next clauses partitioned into rules\n%!";
-      let print_case  i (case_rhs, case_cond) =
-        Printf.printf "\nRCAND: #%d\nRHS: %s\nLHS: %s\n%!" i
+      let print_case  i (case_rhs, updates, case_cond) =
+        Printf.printf "\nRCAND: #%d\nRHS: %s\nUPDATEs: %s\nLHS: %s\n%!" i
           (String.concat " " (List.map term_str case_rhs))
+          (String.concat "; " (List.map update_str updates))
           (String.concat " " (List.map literal_str case_cond)) in
       Array.iteri print_case (Array.of_list res)
     );
@@ -906,18 +1006,20 @@
   List.map (add_erasure_clauses f_paths) move_tups
 
 
-let add_legal_cond static_rels program playout_states (legal_tup, next_cls) =
+let add_legal_cond counters num_functors static_rels program playout_states
+    (legal_tup, next_cls) =
   let legal_tup, legal_conds = List.split legal_tup in
   let legal_cls = List.map (* required clauses *)
     (fun body -> ignore_rhs, true, body) legal_conds in
   List.map
-    (fun (case_rhs, case_cond) -> legal_tup, case_rhs, case_cond)
-    (rule_cases static_rels program playout_states (legal_cls @ next_cls))
+    (fun (case_rhs, updates, case_cond) ->
+      legal_tup, case_rhs, updates, case_cond)
+    (rule_cases counters num_functors static_rels program playout_states
+       (legal_cls @ next_cls))
 
 
-let turnbased_rule_cases static_rels loc_noops used_vars f_paths
-    program playout_states next_cls
-    players legal_by_player =
+let turnbased_rule_cases counters num_functors static_rels loc_noops used_vars f_paths
+    program playout_states next_cls players legal_by_player =
   let legal_tuples = Aux.product legal_by_player in
   (* remove tuples with multiple players making moves
      TODO: could be enhanced by only excluding a noop of a player for
@@ -944,15 +1046,16 @@
     process_rule_cands
       used_vars f_paths next_cls `General players legal_tuples in
   let rules = Aux.concat_map
-    (add_legal_cond static_rels program playout_states) move_tups in
+    (add_legal_cond counters num_functors static_rels
+       program playout_states) move_tups in
   (* we do not look for the players -- for turn-based case, it's done
      while building game graph *)
   Aux.Left rules
 
 
 (* If "Concurrent Moves" case, divide rule clauses among players. *)
-let concurrent_rule_cases static_rels used_vars f_paths program playout_states
-    next_cls players legal_by_player =
+let concurrent_rule_cases counters num_functors static_rels used_vars f_paths
+    program playout_states next_cls players legal_by_player =
   let env_pl_tups =
     env_player,
     process_rule_cands used_vars f_paths next_cls `Environment [] [[]] in
@@ -968,27 +1071,29 @@
   let player_rules = List.map
     (fun (player, move_tups) ->
       player, Aux.concat_map
-        (add_legal_cond static_rels program playout_states) move_tups)
+        (add_legal_cond counters num_functors static_rels
+           program playout_states) move_tups)
     (player_rules @ [env_pl_tups]) in
   Aux.Right player_rules
 
-let general_int_rule_cases static_rels used_vars f_paths program
-    playout_states next_cls players legal_by_player =
+let general_int_rule_cases counters num_functors static_rels used_vars f_paths
+    program playout_states next_cls players legal_by_player =
   failwith "General Interaction Games not implemented yet"
 
 
 (* Generate rule candidates (they need to be filtered before finishing
    the translation of Toss rules): returns the "legal" terms tuple
-   (ordered by players), the right-hand-sides, and the conditions
-   (concatenated bodies of the selected "legal" and "next" clauses).
+   (ordered by players), the right-hand-sides, the counter updates (if
+   any), and the conditions (concatenated bodies of the selected
+   "legal" and "next" clauses).
 
    The "concurrent games" case is handled specifically. Instead of
    rules for tuples of "legal" terms, rules for a single legal term
    are built. The rules are partitioned among players. The last
    player is the environment, [env_player] (this way, the numbering of
    players can be the same as in turn-based case). *)
-let create_rule_cands static_rels is_turn_based used_vars f_paths
-    program playout_states next_cls clauses =
+let create_rule_cands counters num_functors static_rels is_turn_based
+    used_vars f_paths program playout_states next_cls clauses =
   let players = (* Array.of_list *)
     Aux.map_some (function
       | ("role", [|player|]), _ -> Some player
@@ -1019,16 +1124,16 @@
     ) players in
   let result =
     if is_concurrent then
-      concurrent_rule_cases static_rels used_vars f_paths program
+      concurrent_rule_cases counters num_functors static_rels used_vars f_paths program
         playout_states next_cls players legal_by_player
     else
       match is_turn_based with
         | Some (_, loc_noops) ->
-          turnbased_rule_cases static_rels loc_noops used_vars f_paths
+          turnbased_rule_cases counters num_functors static_rels loc_noops used_vars f_paths
             program playout_states next_cls
             players legal_by_player
         | None ->
-          general_int_rule_cases static_rels used_vars f_paths
+          general_int_rule_cases counters num_functors static_rels used_vars f_paths
             program playout_states next_cls
             players legal_by_player
   in
@@ -1037,9 +1142,13 @@
     let pl_rulecands = match result with
       | Aux.Left rcands -> [Const "All Players", rcands]
       | Aux.Right pl_rcands -> pl_rcands in
-    let print_rcand i (_, case_rhs, case_cond) =
-      Printf.printf "\nRCAND: #%d\nRHS: %s\nLHS: %s\n%!" i
+    let update_str (counter, update) =
+      counter^": "^
+        String.concat " " (List.map literal_str update) in
+    let print_rcand i (_, case_rhs, updates, case_cond) =
+      Printf.printf "\nRCAND: #%d\nRHS: %s\nUPDATEs: %s\nLHS: %s\n%!" i
         (String.concat " " (List.map term_str case_rhs))
+        (String.concat "; " (List.map update_str updates))
         (String.concat " " (List.map literal_str case_cond)) in
     let print_rcands (player, rcands) =
       Printf.printf "create_rule_cands: player %s --\n%!"
@@ -1058,7 +1167,7 @@
 let filter_rule_cands static_rels players f_paths program
     playout_states rule_cands =
   let check_cands cands =
-    List.filter (fun (_, _, case_conds) ->
+    List.filter (fun (_, _, _, case_conds) ->
       (* {{{ log entry *)
       if !debug_level > 1 then (
         Printf.printf "check_cands: cond %s%!"
@@ -1080,10 +1189,11 @@
       (* }}} *)      
       res
     ) cands in
-  let add_rhs_as_lhs (legal_tup, case_rhs, case_cond) =
+  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
-    legal_tup, case_rhs, Aux.unique_sorted (case_blanks @ case_cond) in
+    legal_tup, case_rhs, updates,
+    Aux.unique_sorted (case_blanks @ case_cond) in
   let process cands = List.map add_rhs_as_lhs (check_cands cands) in
   match rule_cands with
     | Aux.Left cands -> Aux.Left (process cands)
@@ -1211,9 +1321,25 @@
   else raise Not_turn_based
 
 
-let build_toss_rule transl_data rule_names struc fluents
+let counter_n = "gdl__counter"
+
+let transl_update_path num_functions update =
+  let comp_f acc = function
+    | Pos (Rel (f, _)) when List.mem_assoc f num_functions ->
+      FormulaSubst.subst_real [":x", acc]
+        (List.assoc f num_functions)
+    | _ -> assert false in
+  match update with
+    | [Pos (True (Const c))] -> Formula.Const (float_of_string c)
+    | Pos (True (Func (f, [|r|])))::path ->
+      let xvar = Formula.Fun (f, `FO counter_n) in
+      (* fold_left since the path is in the order of computation *)
+      List.fold_left comp_f xvar path
+    | _ -> assert false
+
+let build_toss_rule num_functions transl_data rule_names struc fluents
     synch_elems synch_precond synch_postcond
-    (legal_tuple, case_rhs, case_cond) =
+    (legal_tuple, case_rhs, updates, case_cond) =
   let rname =
     if legal_tuple = [] then "Environment"
     else String.concat "_" (List.map term_to_name legal_tuple) in
@@ -1227,11 +1353,13 @@
     TranslateFormula.translate transl_data [case_cond] in
   (* a defined relation for checking game termination *)
   let nonterminal = Formula.Not (Formula.Rel ("terminal", [||])) in
+  let precond = synch_precond @ [case_precond] in
   let precond =
-    if legal_tuple = [] then            (* Environment rule *)
-      Formula.And (synch_precond @ [case_precond])
-    else
-      Formula.And (nonterminal :: synch_precond @ [case_precond]) in
+    if legal_tuple = [] then precond    (* Environment rule *)
+    else nonterminal :: precond in
+  let precond =
+    if updates = [] then precond
+    else Formula.Rel (counter_n, [|`FO counter_n|]) :: precond in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf "build_toss_rule: synch precond = %s; main precond = %s\n%!"
@@ -1252,15 +1380,18 @@
         s_subterms)
     case_rhs in
   let rhs_add = synch_postcond @ rhs_add in
+  (* let rhs_add = if updates = [] then rhs_add else  *)
   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
   let rulevar_terms = Aux.strmap_of_assoc
     (List.combine struc_elems case_rhs) in
   let struc_elems = Aux.unique_sorted (synch_elems @ struc_elems) in
+  let struc_elems =
+    if updates = [] then struc_elems else counter_n::struc_elems in
   let precond = FormulaOps.del_vars_quant
     (List.map Formula.fo_var_of_string struc_elems :> Formula.var list)
-    precond in
+    (Formula.And precond) in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     let add_str (rel, args) =
@@ -1275,9 +1406,13 @@
   let discrete =
     DiscreteRule.translate_from_precond ~precond
       ~add:rhs_add ~emb_rels:fluents ~signat ~struc_elems in
+  let updates = List.map
+    (fun (f, update) -> (f, counter_n),
+      transl_update_path num_functions update)
+    updates in
   let rule =
     ContinuousRule.make_rule signat [] discrete
-      [] [] ~pre:discrete.DiscreteRule.pre () in
+      [] updates ~pre:discrete.DiscreteRule.pre () in
   let fixvar_terms = Aux.concat_map
     (fun sterm -> map_paths
       (fun path -> function Var v -> v, (sterm, path)
@@ -1307,7 +1442,7 @@
       (* a rule belongs to a player if other players' legal terms
          in the legal tuple are their noop terms for current location *)
       let loc_rules = Aux.map_some
-        (fun (legal_tup, _, _ as rcand) ->
+        (fun (legal_tup, _, _, _ as rcand) ->
           let legal_tup = Array.of_list legal_tup in
           if Aux.array_for_alli
             (fun pl noop -> pl = player_num ||
@@ -1334,8 +1469,9 @@
 
 let sControl = "CONTROL__"
   
-let loc_graph_general_int = ([||], [], []), (Structure.empty_structure ())
-  (*  failwith "GDL: General Interaction Games not implemented yet" *)
+let loc_graph_general_int players
+    player_payoffs struc build_rule fluents rule_cands =
+  failwith "GDL: General Interaction Games not implemented yet"
 
 (* "environment" will the last player -- also in payoffs
    array. [players] are all player terms, excluding "environment"! *)
@@ -1522,12 +1658,12 @@
 let encode_rule_cands_in_clauses rule_cands clauses =
   let rule_cl_i = ref 0 in
   let more_cls = ref [] in
-  let proc_cand (legal_tup, rhs_tup, cond) =
+  let proc_cand (legal_tup, rhs_tup, updates, cond) =
     let i = !rule_cl_i in
     incr rule_cl_i;
     more_cls := (("rule clause", [|Const (string_of_int i)|]), cond)::
       !more_cls;
-    legal_tup, rhs_tup, i in
+    legal_tup, rhs_tup, updates, i in
   let rule_cands =
     match rule_cands with
       | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
@@ -1544,8 +1680,8 @@
         Aux.Left (int_of_string i, cond)
       | cl -> Aux.Right cl)
     clauses in
-  let proc_cand (legal_tup, rhs_tup, cond_i) =
-    legal_tup, rhs_tup, List.assoc cond_i rule_cls in
+  let proc_cand (legal_tup, rhs_tup, updates, cond_i) =
+    legal_tup, rhs_tup, updates, List.assoc cond_i rule_cls in
   let rule_cands =
     match rule_cands with
       | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
@@ -1577,6 +1713,120 @@
   (* }}} *)
   states
 
+let is_counter_cl num_functors counter_cands (arg, body) =
+  (let try path, rem_body =
+     counter_path_partition num_functors counter_cands (arg, body) in
+   Aux.Strings.is_empty (Aux.Strings.inter (literals_vars path)
+                           (literals_vars rem_body))
+   with Not_found -> false)
+
+(* Returns counters with initial values, separated-out (unchanged)
+   counter clauses and goal clauses whose values are computed from
+   counters, numeric function relations translated into
+   piecewise-linear functions of argument [RVar ":x"], and remaining
+   (unchanged) clauses. *)
+let detect_counters clauses =
+  let num_functions =
+    Aux.map_reduce (fun ((rel,args),b) -> rel,(args,b))
+      (fun acc br ->
+        match acc, br with
+          | Some graph, ([|Const x; Const y|], []) ->
+            (try Some ((float_of_string x, float_of_string y)::graph)
+             with Failure "float_of_string" -> None)
+          | _ -> None)
+      (Some []) clauses in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "detect_counters: num_functions cands=%s\n%!"
+      (String.concat ", "(Aux.map_some (fun (r,g)->
+        if g=None then None else Some r) num_functions))
+  );
+  (* }}} *)
+  let num_functions = Aux.map_some
+    (function
+      | rel, Some graph ->
+        (try Some (rel, FormulaOps.piecewise_linear (Formula.RVar ":x") graph)
+         with Failure "piecewise_linear" -> None)
+      | _ -> None)
+    num_functions in
+  let num_functors = List.map fst num_functions in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "detect_counters: num_functors=%s\n%!"
+      (String.concat ", " num_functors)
+  );
+  (* }}} *)
+  (* Build initial counter candidates based on their "init" clauses. *)
+  let counter_inits = Aux.map_some
+    (function
+      | ("init", [|Func (cand, [|Const y|])|]), [] ->
+        (try Some (cand, float_of_string y)
+         with Failure "float_of_string" -> None)
+      | _ -> None)
+    clauses in
+  let counter_inits = Aux.map_some
+    (function f, [init_v] -> Some (f, init_v) | _ -> None)
+    (Aux.collect counter_inits) in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "detect_counters: counter_inits cands=%s\n%!"
+      (String.concat ", "(List.map fst counter_inits))
+  );
+  (* }}} *)
+  let counter_cl_cands = Aux.collect
+    (Aux.map_some
+       (function ("next",[|Func (f, [|arg|])|]),body
+         when List.mem_assoc f counter_inits ->
+         Some (f,(arg,body)) | _ -> None)
+       clauses) in
+  (* Now the operator iteration. *)
+  let rec counters counter_cl_cands =
+    let counter_cands =
+      Aux.unique_sorted (List.map fst counter_cl_cands) in
+    let res = List.filter
+      (fun (_, brs) -> List.for_all
+        (is_counter_cl num_functors counter_cands) brs)
+      counter_cl_cands in
+    if List.length counter_cl_cands = List.length res
+    then counter_cl_cands
+    else counters res in
+  let counters = List.map fst (counters counter_cl_cands) in
+  let counters = Aux.map_try
+    (fun c -> c, List.assoc c counter_inits) counters in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "detect_counters: resulting counters=%s\n%!"
+      (String.concat ", " (List.map fst counters))
+  );
+  (* }}} *)
+  let counter_cls, clauses = List.partition
+    (function
+      | ("next",[|Func (f,_)|]),_ -> List.mem_assoc f counters
+      | _ -> false) clauses in
+  let clauses = List.filter
+    (function
+      | ("init",[|Func (f,_)|]),_ -> not (List.mem_assoc f counters)
+      | _ -> true) clauses in
+  let goal_cls_w_counters, clauses = List.partition
+    (function
+      | ("goal",[|_; (Var _ as x)|]), body ->
+        is_counter_cl num_functors (List.map fst counters) (x, body)
+      | _ -> false)
+    clauses in
+  counters, counter_cls, goal_cls_w_counters, num_functions, clauses
+
+let add_counter_init_values counters struc =
+  if counters = [] then struc, None
+  else
+    let struc, counter_e =
+      Structure.add_new_elem struc ~name:counter_n () in
+    let struc = Structure.add_rel struc counter_n [|counter_e|] in
+    List.fold_left
+      (fun struc (counter, init) ->
+        Structure.add_fun struc counter (counter_e, init))
+      struc counters,
+    Some counter_e
+
 (* Expand goal value variables using values it could possibly have in
    the game. *)
 let ground_goal_values ground_state_terms clauses =
@@ -1618,12 +1868,27 @@
   let players = Array.of_list players in
   let program = preprocess_program clauses in
   let playout_states = generate_playout_states program players in
+  (* We also detect and remove the goal clauses that use counters to
+     determine values, not to expand their goal value variables later. *)
+  let counter_inits, counter_cls, goal_cls_w_counters,
+    num_functions, clauses = detect_counters clauses in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: detected counters = %s\n%!"
+      (String.concat "; "
+         (List.map (fun (c,v) -> c^"="^string_of_float v) counter_inits))
+  );
+  (* }}} *)
   let rules,
     clauses, f_paths, c_paths,
     root_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 struc, counter_e =
+    add_counter_init_values counter_inits struc in
   let clauses = ground_goal_values ground_state_terms clauses in
+  (* Now, we can add back the separated clauses. *)
+  let clauses = counter_cls @ goal_cls_w_counters @ clauses in
   let ground_at paths = List.map
     (fun p ->
       p, Aux.unique_sorted
@@ -1658,8 +1923,11 @@
       else cl) clauses) in
   let static_rels, nonstatic_rels =
     static_rels (defs_of_rules (Aux.concat_map rules_of_clause clauses)) in
+  let counters = List.map fst counter_inits
+  and num_functors = List.map fst num_functions in
   let rule_cands, is_concurrent =
-    create_rule_cands static_rels turn_data used_vars f_paths
+    create_rule_cands counters num_functors static_rels turn_data
+      used_vars f_paths
       program playout_states next_cls clauses in
   let rule_cands =
     filter_rule_cands static_rels players f_paths program
@@ -1727,19 +1995,23 @@
     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 num_functions transl_data rule_names
+            struc fluents [] [] [] in
         loc_graph_turn_based player_names payoffs
           loc_players loc_noops build_rule
           cands,
         struc
       | None, Aux.Right cands when is_concurrent ->
         let build_rule =
-          build_toss_rule transl_data rule_names in
+          build_toss_rule num_functions transl_data rule_names in
         (* add Environment's payoff *)
         loc_graph_concurrent players payoffs struc build_rule
           fluents cands
       | None, Aux.Right cands ->
-        loc_graph_general_int
+        let build_rule =                (* TODO *)
+          build_toss_rule num_functions transl_data rule_names in
+        loc_graph_general_int players payoffs struc build_rule
+          fluents cands
       | _ -> assert false
   in
   let game = {
@@ -1937,13 +2209,14 @@
 (* We translate as a suite of moves, one for each player; after these
    rules have been applied, the server should apply the environment rule. *)
 let translate_incoming_move_concurrent gdl state actions =
-  (* there is only location 0 *)
+  (* there is only location 0; Environment is not among [actions] *)
   let actions = Array.of_list actions in
   (* let location = (fst state).Arena.graph.(0) in *)
   let struc = (snd state).Arena.struc in
   (* the players actually start at 1, index 0 is the environment *)
   let candidates = Array.mapi
-    (fun player move ->
+    (fun player_not_env move ->
+      let player = player_not_env + 1 in
       let tossrules =
         Aux.strmap_filter (fun  _ rdata ->
           rdata.legal_tuple <> [||] &&  (* not Environment rule *)

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-09 11:12:21 UTC (rev 1561)
@@ -111,8 +111,12 @@
 	    (fun (e, f) -> f = List.assoc e mov.Arena.embedding) mtch then
 	    raise (Found i)
         done;
+        Printf.printf
+          "apply_rewrite: failed for pl. num %d, r_name=%s\n%!"
+          player r_name;
         failwith "GDL Play request: action mismatched with play state"
-      with Found pos -> pos) in
+      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
@@ -179,13 +183,13 @@
   "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:"r1"
-        ~own_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+        ~own_plnum:1 ~opp_plnum:2       (* 0 is environment! *)
+        ~own_rule_name:"m"
+        ~own_emb:["did__BLANK__m", "did__BLANK__r1";
                   "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~own_move:"r1"
-        ~opp_rule_name:"c1"
-        ~opp_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+        ~opp_rule_name:"m2"
+        ~opp_emb:["did__BLANK__m2", "did__BLANK__c1";
                   "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~opp_move:"c1"
     );
@@ -304,13 +308,13 @@
 let a () =
   set_debug_level 4;
       simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
-        ~own_plnum:0 ~opp_plnum:1
-        ~own_rule_name:"r1"
-        ~own_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+        ~own_plnum:1 ~opp_plnum:2       (* 0 is environment! *)
+        ~own_rule_name:"m"
+        ~own_emb:["did__BLANK__m", "did__BLANK__r1";
                   "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~own_move:"r1"
-        ~opp_rule_name:"c1"
-        ~opp_emb:["did__BLANK___BLANK_", "did__BLANK___BLANK_";
+        ~opp_rule_name:"m2"
+        ~opp_emb:["did__BLANK__m2", "did__BLANK__c1";
                   "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
         ~opp_move:"c1"
 
@@ -354,7 +358,7 @@
   (* regenerate ~debug:true ~game_name:"pawn_whopping" ~player:"x"; *)
   (* regenerate ~debug:false ~game_name:"connect4" ~player:"white"; *)
   (* regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row"; *)
-  (* regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman"; *)
+  regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman";
   (* failwith "generated"; *)
   ()
 

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-09-08 19:05:23 UTC (rev 1560)
+++ trunk/Toss/www/reference/reference.tex	2011-09-09 11:12:21 UTC (rev 1561)
@@ -1316,7 +1316,6 @@
 rules (Section~\ref{subsec-rules}) and finally the move translation
 function (Section~\ref{subsec-move-tr}).
 
-
 \subsection{Elements of the Toss Structure} \label{subsec-elems}
 
 By definition of GDL, the state of the game is described by a set
@@ -1333,7 +1332,7 @@
 % In the future, instead of an aggregate playout we
 % might use a form of type inference to approximate $\calS$.
 
-\paragraph{Fluent Paths}
+\subsubsection{Fluent Paths}
 
 We need to decide which parts of the state description will provide
 the fixed ``coordinate system'', and which will provide labels over
@@ -1404,8 +1403,72 @@
   \{(\mathtt{cell},3), (\mathtt{control},1)\}$.
 \end{example}
 
-\paragraph{Structure Elements}
+\subsubsection{Counters and Counter Clauses}
 
+In many definitions there are state terms that would lead to fluent
+paths generating a large number of fluents (\ie distinct subterms at
+the fluent path), each fluent having a numeric interpretation, for
+example being the count of play steps. We are eager to translate the
+part of the game dealing with such state terms compactly, using the
+real number facilities of Toss, since otherwise each ``numeric value''
+would be considered structurally significant, leading to combinatorial
+explosion in the translation process.
+
+In the future, the specification and implementation of counters
+handling, can be generalized for game definitions whose counters
+deviate from the (natural but very limited) format currently
+handled. Ideally, even ``structural'' functional dependencies should
+be recognized and handled compactly, but we leave it to future work.
+
+\begin{definition}
+  A \emph{numeric function relation} is a binary relation given in the
+  game definition entirely by ground facts, containing as relation
+  arguments only numerals: constants that can be parsed as (real)
+  numbers, and the first arguments of its facts are distinct for
+  distinct facts.
+\end{definition}
+
+\begin{example}
+  In the game \texttt{pacman3p.gdl}, the numeric function relations
+  are \texttt{++}, \texttt{--}, \texttt{succ}, \texttt{scoremap}. As
+  it turns out, \texttt{++} and \texttt{--} are only used for
+  structural purposes (which are not precluded by determining that a
+  relation is a numeric function relation).
+\end{example}
+
+\begin{definition}
+  A \texttt{next} clause \texttt{(<= (next ($f$ $h$)) $b$)}, where $f
+  \in C$ is an unary functor and $b$ is the clause body, is a
+  \emph{counter clause given counter candidates $C$}, when either $h$
+  is a numeral (then it is a ``counter reset clause''), or $h$ is a
+  variable, there is a directed path leading to it from some positive
+  \texttt{true} literal \texttt{(true ($g$ $h_0$))} in $b$ with $g \in
+  C$, using numeric function relation positive literals in $b$ (for
+  example an empty path when \texttt{(true ($g$ $h$))} is in $b$), and
+  the variables on the path (including $h$) do not have other
+  occurrences in $b$; in other words, when $h$ is computed from a
+  counter candidate using numeric function relations and the
+  computation does not participate in the remaining ``structural''
+  condition of the clause body.
+\end{definition}
+
+We find the set of \texttt{counters} by iterating an operator
+$\textmd{counters}(C)$, that finds functors $f$ whose all \texttt{(<=
+  (next ($f$ $h$)) $b$)} clauses are conter clauses given counter
+candidates $C$. We start with all unary functors $f$ that have exactly
+one \texttt{init} fact \texttt{(<= (init ($f$ $h$)))}, and $h$ is a
+numeral.
+
+We remove the \texttt{next} clauses that build counters before the
+aggregate playout that generates all state terms is performed, and add
+them back after the fluent paths are found. Therefore, no fluent path
+will point into a counter.
+
+We prepare the translation of numeric function relations for later
+use: they are translated as piecewise-linear functions.
+
+\subsubsection{Structure Elements}
+
 The fluent paths define the partition of GDL state terms into elements
 of the Toss structures in the following way.
 
@@ -1581,7 +1644,6 @@
 introduced fluents, \ie these predicates will change when players
 play the game and all other predicates will remain intact.
 
-
 %Let $\calM$ be any legal state of $G$. Let $\calS^\calM \coloneq \{s |
 %true(s) \in \calM \}$ be the set of state terms at state $\calM$, note
 %that $\calS = \bigcup_\calM \calS^\calM$.
@@ -1602,15 +1664,17 @@
 %  formulas.
 %\end{definition}
 
+\paragraph{Counters in the Initial Structure}
+
+If there are any counters in the definition, we add an element
+$\mathtt{COUNTER}$. We add a singleton predicate $\mathtt{COUNTER}$
+ranging only over the element $\mathtt{COUNTER}$. For each counter, we
+introduce a corresponding function over $\mathtt{COUNTER}$, with the
+initial value determined by an \texttt{init} fact from the game
+definition.
+
 \subsection{Expanding the GDL Game Definition}\label{expanding-gamedef}
 
-Prior to further processing, we modify the wave clauses of the
-game. Let $\calN \in \mathrm{Next}_{W}$, we add to the body of $\calN$
-a \texttt{true} atom $(\mathtt{true} \ BL(s_\calN))$ (where
-$\mathtt{BL}(t)=t\big[\calP_f \ot \mathtt{BLANK}\big]$). The added
-state term will be the corresponding LHS element of the RHS element
-introduced by the clause.
-
 Now we discuss transformations of the game $G$ that result in a longer
 (having more clauses) but simpler definition. \emph{Eliminating a GDL
   variable $x \in FV(\calC)$ by a set of terms $T$} means replacing
@@ -1620,10 +1684,9 @@
 (by virtue of occurring in \texttt{does}, \texttt{legal} or
 \texttt{goal} atoms), by the players of the game.
 
-Another form of expansion was the inlining of clauses, used only for
-finding fluent paths. (In particular, \texttt{does} atoms were then
-replaced by appropriately instantiated bodies of \texttt{legal}
-clauses.)
+Also at the beginning of the translation process, we removed counter
+building clauses from the game definition; we add them back at this
+point.
 
 Before generating Toss formulas we transform the definition $G$ by
 grounding all variables that have occurrences at fluent paths, \ie
@@ -1852,7 +1915,7 @@
 different matches in different game states, while the Toss rule has to
 be built from all the rule clauses that would match when the Toss rule
 matches. Therefore, we need to build a Toss rule for each subset of
-rule clauses that are ``selected'' by some game state (i.e. are
+rule clauses that are ``selected'' by some game state (\ie are
 exactly the rule clauses matching in that state), but add to it
 ``separation conditions'' that prevent the Toss rule from matching in
 game states where more rule clauses can match.
@@ -1868,8 +1931,10 @@
 
 We filter the rule candidates by checking for satisfiability (in the
 same GDL model as used for building the initial Toss structure) of the
-stable part of their clause bodies. For each remaining candidate,
-we will construct the Toss rule in two steps.
+static part of their clause bodies, and later by checking for
+satisfiability of the whole clause bodies in at least one of a
+collection of random playout states. For each remaining candidate, we
+will construct the Toss rule in two steps.
 
 In the first step we generate the \emph{matching condition}: we
 translate the conjunction of the bodies of rule clauses and the
@@ -1893,6 +1958,22 @@
 atoms involving only these variables and not occurring inside
 disjunctions are extracted to be relations tuples in $\frakL$.
 
+\paragraph{Translating Counter Clauses}
+
+We treat the counter clauses specially, to simplify presentation we
+describe the differences here. We do not add the ``blanked-out''
+counter state term to the $\frakR$-structure, instead we add a new
+element (with the $\textmd{COUNTER}$ predicate over it in the
+$\frakL$-structure). We remove the computation of the counter update
+from the counter clause, reset the resulting clause to ``unrequired'',
+and add it back to the candidate clauses, remembering the association
+with the counter update. After the rule clauses have been finally
+partitioned, we make sure that there is only one counter clause for a
+given counter in each resulting rule candidate. To complete the
+translation, we calculate the function update, inlining the
+translations of numeric function relations, and add the update to the
+rule translation for each counter occurring in a rule.
+
 Having constructed and filtered the rewriting rule candidates, we have
 almost completed the definition of $T(G)$. Payoff formulas are derived
 by instantiating variables standing for the \texttt{goal} values. The

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