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

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

Revision: 1563
          http://toss.svn.sourceforge.net/toss/?rev=1563&view=rev
Author:   lukstafi
Date:     2011-09-11 18:47:06 +0000 (Sun, 11 Sep 2011)
Log Message:
-----------
GDL translation: translating goal values (i.e. payoffs) computed from counters; bug fix: update conditions now processed with other clauses. (Uses of counters other than counter updates and goal values not implemented yet, coming soon.)

Modified Paths:
--------------
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-09-10 13:02:00 UTC (rev 1562)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-09-11 18:47:06 UTC (rev 1563)
@@ -98,7 +98,8 @@
   
 let find_defrel_arg sterms args apset =
   List.find
-    (fun s -> List.for_all (fun (p,i) -> at_path s p = args.(i)) apset)
+    (fun s -> List.for_all (fun (p,i) ->
+      try at_path s p = args.(i) with Not_found -> false) apset)
     sterms
 
 let translate_defrel data sterms sign rel args =
@@ -109,7 +110,10 @@
   );
   (* }}} *)
   let partition = List.assoc rel data.defrel_argpaths in
-  let s_l = List.map (find_defrel_arg sterms args) partition in
+  let s_l =
+    try List.map (find_defrel_arg sterms args) partition
+    with Not_found -> failwith
+      ("could not build arguments for defined relation "^rel) in
   let vtup = Array.of_list (List.map (var_of_term data) s_l) in
   let defrel_phi = Formula.Rel (rel, vtup) in
   if sign then defrel_phi else Formula.Not defrel_phi

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-09-10 13:02:00 UTC (rev 1562)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-11 18:47:06 UTC (rev 1563)
@@ -754,32 +754,17 @@
         Aux.Left (f, h, body)
       | cl -> Aux.Right cl)
     rule_cls in
-  let counter_cls = Array.mapi
-    (fun i (f, h, body) ->
+  let counter_cls = List.map
+    (fun (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
+      f, (cond, update))
+      counter_cls in
+  Aux.collect 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
-       
+let remove_local_vars gvars lits =
+  List.filter (fun l -> Aux.Strings.subset (literals_vars [l]) gvars) lits
 
 (* Assign rule clauses to rule cases, i.e. candidates for Toss
    rules. Collect the conditions and RHS state terms together. Frame
@@ -789,10 +774,13 @@
    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 preprocess the clauses by filtering out the counter clauses,
+   splitting them into update calculation and remaining clause
+   condition. (For each counter, the counter clauses will later be
+   merged into a single update by turning clause conditions into
+   characteristic functions multiplied by update calculations, and
+   summing up.) At the end, we add the update clauses to each rule
+   case.
 
    We call atoms or literals "deterministic" if they are not under
    disjunction. First we collect deterministic literals of required
@@ -811,10 +799,7 @@
    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.
+   "RHSes" from clause heads removing "_IGNORE_RHS_".
 
    TODO: unrequired clauses with disjunctions may avoid being
    excluded. If this poses problems we might need to expand
@@ -822,7 +807,7 @@
 *)
 let rule_cases counters num_functors static_rels testground program
     playout_states rule_cls =
-  let counter_upds, rule_cls =
+  let counter_cls, rule_cls =
     split_counter_rule_cls counters num_functors rule_cls in
   let required_cls = Aux.map_some
     (fun (h, required, body) ->
@@ -890,10 +875,6 @@
          | _ -> 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
@@ -902,7 +883,7 @@
       Printf.printf "rule_cases: single partition\n%!";
     );
     (* }}} *)
-    [Aux.unique_sorted case_rhs, updates,
+    [Aux.unique_sorted case_rhs, counter_cls,
      Aux.unique_sorted (List.concat case_conds)]
   else
     let patterns =
@@ -949,42 +930,46 @@
               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 =
         Aux.list_remove ignore_rhs (Aux.unique_sorted case_rhs) in
       let case_conds =
         Aux.unique_sorted (List.concat case_conds) in
+      let separation_cond =
+        remove_local_vars (literals_vars case_conds) separation_cond in
       (* {{{ log entry *)
       if !debug_level > 3 then (
-        let update_str (counter, update) =
-          counter^": "^
+        let cond_upd_str (cond, update) =
+          ":(and "^String.concat " " (List.map literal_str cond)^")*{"^
             String.concat " " (List.map literal_str update) in
+        let counters_str (counter, cond_updates) =
+          counter^": "^String.concat ", "
+            (List.map cond_upd_str cond_updates) in
         Printf.printf
-          "\nRCAND:\nsep_cond: %s\nRHS: %s\nUPDATEs: %s\ncase_conds: %s\n\n%!"
+          "\nRCAND:\nsep_cond: %s\nRHS: %s\nCOUNTER_CLs: %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 counters_str counter_cls))
           (String.concat " " (List.map literal_str case_conds))
       );
       (* }}} *)
-      case_rhs, updates,
+      case_rhs, counter_cls,
         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^": "^
+      let cond_upd_str (cond, update) =
+        ":(and "^String.concat " " (List.map literal_str cond)^")*{"^
           String.concat " " (List.map literal_str update) in
+      let counters_str (counter, cond_updates) =
+        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, updates, case_cond) =
-        Printf.printf "\nRCAND: #%d\nRHS: %s\nUPDATEs: %s\nLHS: %s\n%!" i
+      let print_case  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 update_str updates))
+          (String.concat "; " (List.map counters_str counter_cls))
           (String.concat " " (List.map literal_str case_cond)) in
       Array.iteri print_case (Array.of_list res)
     );
@@ -1158,13 +1143,16 @@
     let pl_rulecands = match result with
       | Aux.Left rcands -> [Const "All Players", rcands]
       | Aux.Right pl_rcands -> pl_rcands in
-    let update_str (counter, update) =
-      counter^": "^
+    let cond_upd_str (cond, update) =
+      ":(and "^String.concat " " (List.map literal_str cond)^")*{"^
         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
+    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) =
+      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 update_str updates))
+        (String.concat "; " (List.map counters_str counter_cls))
         (String.concat " " (List.map literal_str case_cond)) in
     let print_rcands (player, rcands) =
       Printf.printf "create_rule_cands: player %s --\n%!"
@@ -1353,9 +1341,22 @@
       List.fold_left comp_f xvar path
     | _ -> assert false
 
+let transl_cond_updates transl_data num_functions cond_updates =
+  let cond_update (cond, update) =
+    let update = transl_update_path num_functions update in
+    let cond = TranslateFormula.translate transl_data [cond] in
+    Formula.Times (Formula.Char cond, update) in
+  match cond_updates with
+    | [] -> assert false
+    | [c_upd] -> cond_update c_upd
+    | c_upd::c_upds ->
+      List.fold_left
+        (fun acc c_upd -> Formula.Plus (acc, cond_update c_upd))
+        (cond_update c_upd) c_upds
+
 let build_toss_rule num_functions transl_data rule_names struc fluents
     synch_elems synch_precond synch_postcond
-    (legal_tuple, case_rhs, updates, case_cond) =
+    (legal_tuple, case_rhs, counter_cls, case_cond) =
   let rname =
     if legal_tuple = [] then "Environment"
     else String.concat "_" (List.map term_to_name legal_tuple) in
@@ -1374,7 +1375,7 @@
     if legal_tuple = [] then precond    (* Environment rule *)
     else nonterminal :: precond in
   let precond =
-    if updates = [] then precond
+    if counter_cls = [] then precond
     else Formula.Rel (counter_n, [|`FO counter_n|]) :: precond in
   (* {{{ log entry *)
   if !debug_level > 2 then (
@@ -1396,7 +1397,7 @@
         s_subterms)
     case_rhs in
   let rhs_add = synch_postcond @ rhs_add in
-  (* let rhs_add = if updates = [] then rhs_add else  *)
+  (* let rhs_add = if counter_cls = [] 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
@@ -1404,7 +1405,7 @@
     (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
+    if counter_cls = [] 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)
     (Formula.And precond) in
@@ -1423,9 +1424,9 @@
     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
+    (fun (f, cond_updates) -> (f, counter_n),
+      transl_cond_updates transl_data num_functions cond_updates)
+    counter_cls in
   let rule =
     ContinuousRule.make_rule signat [] discrete
       [] updates ~pre:discrete.DiscreteRule.pre () in
@@ -1568,24 +1569,42 @@
 
 (* We assume that clauses for different goal values are disjoint, for
    non-disjoint we sum each component. *)
-let compute_payoffs transl_data players clauses =
-  (* TODO: we should expand non-constant value expressions... *)
+let compute_payoffs transl_data num_functors num_functions counters
+    players clauses =
   let goal_cls = Aux.map_some
     (function (("goal",[|player; value|]), body) ->
       Some (player,(value,body)) | _ -> None) clauses in
+  let goal_w_counters_cls, goal_cls = Aux.partition_map
+    (function
+      | p, (Var _ as arg,body) as g_cl ->
+        (let try path, rem_body =
+           counter_path_partition num_functors counters (arg, body) in
+         if Aux.Strings.is_empty (Aux.Strings.inter (literals_vars path)
+                                 (literals_vars rem_body))
+         then Aux.Left (p, (rem_body, path))
+         else Aux.Right g_cl
+         with Not_found -> Aux.Right g_cl)
+      | g_cl -> Aux.Right g_cl)
+    goal_cls in
   let goal_cls =
     List.map (fun (player, goal_brs) -> player, Aux.collect goal_brs)
       (Aux.collect goal_cls) in
+  let goal_w_counters_cls = Aux.collect goal_w_counters_cls in
   let player_goals = Array.map
     (fun player ->
-      try List.assoc player goal_cls
-      with Not_found -> failwith
-        ("TranslateGame.compute_payoffs: no goal provided for player "
-         ^ term_to_name player))
+      let num_goal_cls =
+        try List.assoc player goal_cls with Not_found -> [] in
+      let counter_goal_cls =
+        try List.assoc player goal_w_counters_cls with Not_found -> [] in
+      if num_goal_cls = [] && counter_goal_cls = [] then
+        failwith
+          ("TranslateGame.compute_payoffs: no goal provided for player "
+           ^ term_to_name player)
+      else num_goal_cls, counter_goal_cls)
     players in
   (* Translate the goal conditions. *)
-  let payoffs = Array.map
-    (fun goals -> List.map
+  let transl_payoffs (num_goal_cls, counter_goal_cls) =
+    let num_payoff = List.map
       (fun (score, disjs) ->
         let score =
           match score with
@@ -1600,42 +1619,50 @@
         score,
         if phi_vars = [] then goal_phi
         else Formula.Ex (phi_vars, goal_phi))
-      goals)
-    player_goals in
-  (* Offset the values to remove the most inconvenient goal
-     condition. *)
-  let payoffs = Array.map
-    (fun payoff ->
-      let sized =
-        List.map (fun (score,phi) -> GameSimpl.niceness phi, score)
-          payoff in
+      num_goal_cls in
+      (* Offset the values to remove the most inconvenient goal
+         condition. *)
+    let sized =
+      List.map (fun (score,phi) -> GameSimpl.niceness phi, score)
+        num_payoff in
       (* Sort in increasing niceness -- to remove the least nice. *)
-      let base_score =
-        match List.sort Pervasives.compare sized with [] -> 0.
-          | (_, score)::_ -> score in
-      match payoff with
-        | [score, guard] ->
-          Formula.Times (
-            Formula.Const score, Formula.Char guard)
-        | scores ->
-          List.fold_left (fun sum (score, guard) ->
-            if score = base_score then (
+    let base_score =
+      match List.sort Pervasives.compare sized with [] -> 0.
+        | (_, score)::_ -> score in
+    let num_payoff =
+    match num_payoff with
+      | [] -> Formula.Const 0.
+      | [score, guard] ->
+        Formula.Times (
+          Formula.Const score, Formula.Char guard)
+      | scores ->
+        List.fold_left (fun sum (score, guard) ->
+          if score = base_score then (
               (* {{{ log entry *)
-              if !debug_level > 2 then (
-                Printf.printf
-                  "translate_game: (8) dropping score %f guard:\n%s\n\n%!"
-                  score (Formula.sprint guard)
-              );
+            if !debug_level > 2 then (
+              Printf.printf
+                "translate_game: (8) dropping score %f guard:\n%s\n\n%!"
+                score (Formula.sprint guard)
+            );
               (* }}} *)
-              sum)
-            else
-              let guarded = Formula.Times (
-                Formula.Const (score -. base_score), Formula.Char guard) in
-              if sum = Formula.Const 0. then guarded
-              else Formula.Plus (sum, guarded))
-            (Formula.Const base_score) scores
-    ) payoffs in
-  payoffs
+            sum)
+          else
+            let guarded = Formula.Times (
+              Formula.Const (score -. base_score), Formula.Char guard) in
+            if sum = Formula.Const 0. then guarded
+            else Formula.Plus (sum, guarded))
+          (Formula.Const base_score) scores in
+    let counter_payoff =
+      match counter_goal_cls with
+        | [] -> Formula.Const 0.
+        | cond_upds ->
+          transl_cond_updates transl_data num_functions cond_upds in
+    if num_payoff = Formula.Const 0.
+    then counter_payoff
+    else if counter_payoff = Formula.Const 0.
+    then num_payoff
+    else Formula.Plus (counter_payoff, num_payoff) in
+  Array.map transl_payoffs player_goals
 
 
 let transl_argpath_no_side defined_rels init_state program
@@ -1673,10 +1700,22 @@
 (* Representing rule candidates as (rule) clauses. *)
 let encode_rule_cands_in_clauses rule_cands clauses =
   let rule_cl_i = ref 0 in
+  let rule_upd_j = ref 0 in
   let more_cls = ref [] in
+  let proc_update i (cond, update) =
+    let j = !rule_upd_j in
+    incr rule_upd_j;
+    more_cls := (("update clause", [|Const (string_of_int i);
+                                     Const (string_of_int j)|]), cond)::
+      !more_cls;
+    update, j in
+  let proc_counter_upds i (counter, updates) =
+    let updates = List.map (proc_update i) updates in
+    counter, updates in
   let proc_cand (legal_tup, rhs_tup, updates, cond) =
     let i = !rule_cl_i in
-    incr rule_cl_i;
+    incr rule_cl_i; rule_upd_j := 0;
+    let updates = List.map (proc_counter_upds i) updates in
     more_cls := (("rule clause", [|Const (string_of_int i)|]), cond)::
       !more_cls;
     legal_tup, rhs_tup, updates, i in
@@ -1696,8 +1735,20 @@
         Aux.Left (int_of_string i, cond)
       | cl -> Aux.Right cl)
     clauses in
-  let proc_cand (legal_tup, rhs_tup, updates, cond_i) =
-    legal_tup, rhs_tup, updates, List.assoc cond_i rule_cls in
+  let update_cls, clauses = Aux.partition_map
+    (function
+      | ("update clause", [|Const i; Const j|]), cond ->
+        Aux.Left ((int_of_string i, int_of_string j), cond)
+      | cl -> Aux.Right cl)
+    clauses in
+  let proc_update i (update, j) =
+    List.assoc (i,j) update_cls, update in
+  let proc_counter_upds i (counter, updates) =
+    let updates = List.map (proc_update i) updates in
+    counter, updates in
+  let proc_cand (legal_tup, rhs_tup, updates, i) =
+    legal_tup, rhs_tup, List.map (proc_counter_upds i) updates,
+    List.assoc i rule_cls in
   let rule_cands =
     match rule_cands with
       | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
@@ -2022,7 +2073,9 @@
     decode_rule_cands_of_clauses rule_cands clauses in
   (* possibly update the structure with a control element and predicate *)
   let rule_names = ref Aux.Strings.empty in
-  let payoffs = compute_payoffs transl_data players clauses in
+  let payoffs =
+    compute_payoffs transl_data num_functors num_functions counters
+      players clauses in
   let player_names = Array.to_list
     (Array.mapi (fun i p -> term_to_name p, i)
        (if turn_data = None then Array.append [|env_player|] players

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-09-10 13:02:00 UTC (rev 1562)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-11 18:47:06 UTC (rev 1563)
@@ -361,7 +361,7 @@
   (* 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";
-  failwith "generated";
+  (* failwith "generated"; *)
   ()
 
 let exec () =

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-09-10 13:02:00 UTC (rev 1562)
+++ trunk/Toss/www/reference/reference.tex	2011-09-11 18:47:06 UTC (rev 1563)
@@ -1927,7 +1927,10 @@
 according to the partition, form the separation condition. Currently,
 we do not consider atoms under disjunction (mostly for simplicity
 considerations; would this cause problems, the definition can be
-extended to include disjunctions in making the partition).
+extended to include disjunctions in making the partition). We remove
+from the separation condition negations of atoms that contain ``local
+variables'': variables not appearing in positive atoms of the whole
+condition.
 
 We filter the rule candidates by checking for satisfiability (in the
 same GDL model as used for building the initial Toss structure) of the

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