[Toss-devel-svn] SF.net SVN: toss:[1513] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1513] trunk/Toss
|
From: <luk...@us...> - 2011-07-14 22:56:50
|
Revision: 1513
http://toss.svn.sourceforge.net/toss/?rev=1513&view=rev
Author: lukstafi
Date: 2011-07-14 22:56:38 +0000 (Thu, 14 Jul 2011)
Log Message:
-----------
GDL translation work in progress. Does not compile yet.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/GGP/TranslateGame.ml
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-07-14 15:51:48 UTC (rev 1512)
+++ trunk/Toss/Formula/Aux.ml 2011-07-14 22:56:38 UTC (rev 1513)
@@ -441,6 +441,15 @@
done;
true
with Not_found -> false
+
+let array_for_alli f a =
+ try
+ for i = 0 to Array.length a - 1 do
+ if not (f i (Array.unsafe_get a i)) then
+ raise Not_found
+ done;
+ true
+ with Not_found -> false
let array_for_all2 f a b =
let len = Array.length a in
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-07-14 15:51:48 UTC (rev 1512)
+++ trunk/Toss/Formula/Aux.mli 2011-07-14 22:56:38 UTC (rev 1513)
@@ -216,6 +216,9 @@
(** Find if a predicate holds for all elements. *)
val array_for_all : ('a -> bool) -> 'a array -> bool
+(** Find if a position-dependent predicate holds for all elements. *)
+val array_for_alli : (int -> 'a -> bool) -> 'a array -> bool
+
(** Find if a predicate holds for all elements of two arrays
pointwise. Raises [Invalid_argument "Aux.array_for_all2"] if
arrays are of different lengths. *)
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-07-14 15:51:48 UTC (rev 1512)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-07-14 22:56:38 UTC (rev 1513)
@@ -22,6 +22,7 @@
(** Use "true" atoms while computing rule cases. *)
let split_on_state_atoms = ref false
+let env_player = Const "ENVIRONMENT"
type tossrule_data = {
lead_legal : term;
@@ -51,6 +52,9 @@
masks : term list;
tossrule_data : tossrule_data Aux.StrMap.t;
(* rule name to rule translation data *)
+ turnbased_noops : term array array option;
+ (* in case of a turn-based translation, for each location and each
+ player, the player's noop move (if any) for the location *)
}
(* [most_similar c ts] finds a term from [ts] most similar to [c], and
@@ -230,8 +234,11 @@
(* Find the rule clauses $\ol{\calC},\ol{\calN}$. Do not remove the
- "does" atoms from clauses. *)
-let move_tuples used_vars next_cls legal_tuples =
+ "does" atoms from clauses. Also handles as special cases:
+ "concurrent" case with selecting clauses for only one player, and
+ "environment" case for selecting clauses not dependent on any
+ player. *)
+let move_tuples used_vars next_cls mode players legal_tuples =
(* computing the $d_i(\calN)$ for each $\calN$ *)
let fresh_x_f () =
let x_f = Aux.not_conflicting_name !used_vars "x_f" in
@@ -246,14 +253,24 @@
let sb = unify_all sb djs in
let d =
match djs with
- | [] -> fresh_x_f ()
+ | [] ->
+ if mode = `Concurrent then raise Not_found
+ else fresh_x_f ()
| d::_ -> subst sb d in
sb, d::dis
) players ([], []) in
let next_cls =
- Aux.map_try (fun cl ->
- let sb, ds = does_facts cl in
- subst_clause sb cl, ds) next_cls in
+ if mode = `Environment
+ then
+ List.map_some (fun (_,body as cl) ->
+ if List.mem (function Does _ -> true | _ -> false) body
+ then None
+ else Some (cl, [])
+ ) next_cls
+ else
+ Aux.map_try (fun cl ->
+ let sb, ds = does_facts cl in
+ subst_clause sb cl, ds) next_cls in
(* selecting $\ol{\calC},\ol{\calN}$ clauses with
$\sigma_{\ol{\calC},\ol{\calN}}$ applied *)
let tup_unifies ts1 ts2 =
@@ -416,8 +433,15 @@
let general_int_rule_cases (legal_tup, next_cls) =
failwith "General Interaction Games not implemented yet"
-(* The candidates need to be filtered before finishing the
- translation of Toss rules. *)
+(* 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).
+
+ 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 first
+ player is the environment, [env_player]. *)
let create_rule_cands is_turn_based used_vars next_cls clauses =
let players = (* Array.of_list *)
Aux.map_some (function
@@ -442,22 +466,26 @@
| ("legal",[lp; l]), body when lp = p -> Some (l, body)
| _ -> None) legal_cls
) players in
- let process_rule_cands legal_tuples =
- let move_tups = move_tuples used_vars next_cls legal_tuples in
+ let process_rule_cands mode players legal_tuples =
let move_tups =
+ move_tuples used_vars next_cls mode players legal_tuples in
+ let move_tups =
List.map (fun (sb, legal_tup, n_cls) ->
List.map (subst sb) legal_tup,
List.map (subst_clause sb) n_cls) move_tups in
List.map add_erasure_clauses move_tups in
let concurrent_rule_cands player legal_cls =
let legal_tuples = List.map (fun cl -> [cl]) legal_cls in
- let move_tups = process_rule_cands legal_tuples in
- player, Aux.concat_map nonint_rule_cases move_tups
+ let move_tups =
+ process_rule_cands `Concurrent [player] legal_tuples in
+ player, Aux.concat_map nonint_rule_cases (move_tups @ env_tups)
if is_concurrent then
- Right (List.map2 concurrent_rule_cands players legal_by_player)
+ let env_tups =
+ env_player, process_rule_cands `Environment [] [[]] in
+ Right (env_tups @ List.map2 concurrent_rule_cands players legal_by_player)
else
let legal_tuples = Aux.product legal_by_player in
- let move_tups = process_rule_cands legal_tuples in
+ let move_tups = process_rule_cands `General players legal_tuples in
if is_turn_based then
Left (Aux.concat_map nonint_rule_cases move_tups)
else
@@ -556,27 +584,140 @@
loc_players, loc_noops
+let build_toss_rule transl_data rule_names struc fluents
+ synch_precond synch_postcond (legal_tup, case_rhs, case_cond) =
+ let rname =
+ Aux.not_conflicting_name rule_names
+ (String.concat "_" (List.map term_to_name legal_tup)) in
+ rule_names := Aux.Strings.add rname !rule_names;
+ let label =
+ {Arena.rule = rname; time_in = 0.1, 0.1; parameters_in = []} in
+ let precond =
+ synch_precond @ TranslateFormula.translate transl_data case_cond in
+ let rhs_pos = Aux.concat_map
+ (function _, [sterm] ->
+ let s_subterms =
+ map_paths (fun path subt -> subt, path) transl_data.f_paths sterm in
+ let s_subterms = List.filter
+ (fun (subt, _) -> subt <> blank) s_subterms in
+ let vartup = [|var_of_term data sterm|] in
+ List.map (fun (subt, path) ->
+ pred_on_path_subterm path subt, vartup)
+ s_subterms
+ | _ -> assert false)
+ case_rhs in
+ let rhs_pos = synch_postcond @ rhs_pos in
+ let signat = Structure.rel_signature struc in
+ let discrete =
+ DiscreteRule.translate_from_precond ~precond
+ ~add:rhs_pos ~emb_rels:fluents ~signat ~struc_elems in
+ let rule =
+ ContinuousRule.make_rule signature [] discrete
+ [] [] ~pre:discrete.DiscreteRule.pre () in
+ label, (rname, rule)
+
+
let loc_graph_turn_based player_nums
- player_payoffs loc_players loc_noops rule_cands =
+ player_payoffs loc_players loc_noops build_rule rule_cands =
+ let rules = ref [] in
+ let loc_n = Array.length loc_players in
+ let player_rules = Aux.collect player_rules in
let graph = Array.mapi
(fun loc player ->
let player_num = List.assoc (term_to_name player) player_nums in
+ (* 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) ->
+ let legal_tup = Array.of_list legal_tup in
+ if Array.for_alli
+ (fun pl noop -> pl = player_num ||
+ Some legal_tup.(pl) = noop)
+ loc_noops.(loc)
+ then Some (build_rule rcand)
+ else None
+ ) rule_cands in
+ let labels, loc_rules = List.split loc_rules in
+ rules := !rules @ loc_rules;
let pl_moves =
+ List.map (fun l -> l, (loc + 1) mod loc_n) labels in
Array.mapi
(fun pl_num payoff ->
{Arena.payoff = payoff;
view = [];
heur = [];
moves = if pl_num = player_num then pl_moves else []})
- players)
+ player_payoffs)
loc_players in
+ graph, !rules
+
+let sControl = "CONTROL__"
let loc_graph_general_int =
failwith "GDL: General Interaction Games not implemented yet"
-let loc_graph_concurrent =
-()
+(* Remember that "environment" is the 0th player -- also in payoffs
+ list. [rule_cands] is a player-indexed array. [players] are all
+ player terms, excluding "environment". *)
+let loc_graph_concurrent players
+ player_payoffs struc build_rule rule_cands =
+ (* finding or creating the control predicate *)
+ let control_pred, control_e, struc =
+ try
+ let control_pred, _ =
+ List.find (fun (rel, ar) -> ar = 1 &&
+ Structure.Tuples.cardinal (Structure.find_rel rel struc) = 1)
+ (Structure.rel_signature struc) in
+ let etup = Structure.Tuples.choose_elem
+ (Structure.find_rel control_pred struc) in
+ control_pred, etup.(0), struc
+ with Not_found ->
+ let struc, control_e =
+ Structure.add_new_elem struc ~name:sControl () in
+ let struc = Structure.add_rel struc [|control_e|] in
+ sControl, control_e, struc in
+ (* adding synchronization to rules and putting it all together *)
+ let player_pred pl = term_to_name pl ^ "__SYNC" in
+ let struc = List.fold_left
+ (fun struc player ->
+ Structure.add_rel_name (player_pred player) 1) players in
+ let control_v =
+ Formula.fo_var_of_string (Structure.elem_name struc control_e) in
+ let player_marker pl =
+ [player_pred pl, [|control_v|]; control_pred, [|control_v|]] in
+ let all_players_precond =
+ (List.map (fun (rel,tup) -> Formula.Rel (rel,tup)))
+ (Aux.concat_map player_marker players) in
+ let rules = ref [] in
+ let player_moves = Array.mapi
+ (fun pl_num (pl, p_rules) ->
+ let p_rules = List.map
+ (fun rcand ->
+ if pl_num = 0 then (* environment *)
+ build_rule struc fluents all_players_precond [] rcand
+ else
+ build_rule struc fluents [] (player_marker pl) rcand)
+ p_rules in
+ (* we need to build first before adding [player_cond] because
+ of how formula translation works *)
+ let labels, p_rules = List.split p_rules in
+ rules := !rules @ p_rules;
+ List.map (fun l -> l, (loc + 1) mod loc_n))
+ rule_cands in
+ let graph =
+ [|
+ Aux.array_map2
+ (fun payoff moves ->
+ {Arena.payoff = payoff;
+ view = [];
+ heur = [];
+ moves = moves})
+ player_payoffs player_moves
+ |] in
+ (graph, !rules), struc
+
+
let translate_game clauses =
let clauses = expand_players clauses in
let used_vars, clauses = rename_clauses clauses in
@@ -610,14 +751,21 @@
) clauses) in
let player_names = Array.to_list
(Array.mapi (fun i p -> term_to_name p, i) players) in
- let graph (*: player_loc array array*) =
+ (* possibly update the structure with a control element and predicate *)
+ let (graph, rules), struc =
match turn_data, rule_cands with
| Some (loc_players, loc_noops), Left cands ->
- loc_graph_turn_based players loc_players loc_noops cands
+ let build_rule =
+ build_toss_rule transl_data rule_names struc fluents [] [] in
+ loc_graph_turn_based players loc_players loc_noops build_rule
+ cands, struc
| None, Left cands ->
loc_graph_general_int
| None, Right cands
- loc_graph_concurrent
+ let build_rule =
+ build_toss_rule transl_data rule_names in
+ loc_graph_concurrent players player_payoffs struc build_rule
+ rule_cands
| _ -> assert false
in
let game = {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
