[Toss-devel-svn] SF.net SVN: toss:[1610] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1610] trunk/Toss
|
From: <luk...@us...> - 2011-10-21 22:00:46
|
Revision: 1610
http://toss.svn.sourceforge.net/toss/?rev=1610&view=rev
Author: lukstafi
Date: 2011-10-21 22:00:39 +0000 (Fri, 21 Oct 2011)
Log Message:
-----------
GameSimpl: bug fix. GDL translation: setting the counter element by Sum guard.
Modified Paths:
--------------
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/GGP/TranslateFormula.ml
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGameTest.ml
trunk/Toss/GGP/tests/pacman3p-raw.toss
trunk/Toss/GGP/tests/pacman3p-simpl.toss
trunk/Toss/Server/ReqHandler.ml
trunk/Toss/Solver/RealQuantElim/Poly.ml
trunk/Toss/Solver/Solver.ml
Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/GameSimpl.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -190,8 +190,15 @@
List.filter (fun v -> not (List.mem_assoc (var_str v) sb)) vs in
let phi = FormulaSubst.subst_vars sb (And (more_conj @ conj)) in
if vs = [] then phi else Ex (vs, phi)
- | phi -> phi} in
- FormulaMap.map_formula f_map phi
+ | phi -> Ex (vs, phi)} in
+ let res = FormulaMap.map_formula f_map phi in
+ (* {{{ log entry *)
+ if !debug_level > 3 && phi <> res then (
+ Printf.printf "remove_exist:\nphi=%s\nres=%s\n%!"
+ (Formula.str phi) (Formula.str res)
+ );
+ (* }}} *)
+ res
(* A heuristic measure of how easy a formula is to solve or provide a
good heuristic. Very crude for now, not using the structure yet. *)
Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/TranslateFormula.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -204,15 +204,20 @@
if sign then Formula.EQZero else Formula.NEQZero in
let cc = Formula.Fun (c, counter_v) and ct = transl_c t in
if cc = ct then []
- else [Formula.RealExpr (minus cc ct, sign_op)] in
+ else [Formula.RealExpr (
+ Formula.Sum ([counter_v], Formula.Rel (counter_n, [|counter_v|]),
+ minus cc ct)
+ , sign_op)] in
let transl_numfun_rel sign rel t1 t2 =
let sign_op =
if sign then Formula.EQZero else Formula.NEQZero in
let f_result =
FormulaSubst.subst_real [":x", transl_c t1]
(List.assoc rel data.num_functions) in
- [Formula.RealExpr
- (minus f_result (transl_c t2), sign_op)] in
+ [Formula.RealExpr (
+ Formula.Sum ([counter_v], Formula.Rel (counter_n, [|counter_v|]),
+ minus f_result (transl_c t2))
+ , sign_op)] in
let rec aux = function
| Pos (True (Func (c, [|t|])))
when List.mem c data.counters &&
@@ -368,22 +373,12 @@
if pos_vars = [] then base_part
else Formula.Ex ((pos_vars :> Formula.var list), base_part)
-let has_counter t =
- FormulaMap.fold_formula
- {FormulaMap.make_fold ( || ) false with
- FormulaMap.fold_Fun = (fun _ v -> v = counter_v)} t
-
(* Translate a disjunction of conjunctions of literals (and disjs of lits). *)
let translate data disj =
let disj = separate_disj data.counters disj in
- let res =
- Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) ->
- transl_disjunct data rels_phi pos_state neg_state []
- ) disj) in
- if has_counter res
- then Formula.Ex
- ([counter_v], Formula.And [Formula.Rel (counter_n, [|counter_v|]); res])
- else res
+ Formula.Or (List.map (fun (rels_phi, pos_state, neg_state) ->
+ transl_disjunct data rels_phi pos_state neg_state []
+ ) disj)
(* **************************************** *)
(* {3 Build defined relations.} *)
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -2166,7 +2166,13 @@
~add:rhs_add ~nondistinct ~emb_rels:fluents ~signat ~struc_elems in
let updates = List.map
(fun (f, cond_updates) -> (f, counter_n),
- transl_cond_updates transl_data num_functions cond_updates)
+ (* a trick to force instantiating the counter variable -- note
+ that variable with the same name is also part of the
+ precondition *)
+ Formula.Sum (
+ [`FO counter_n],
+ Formula.Rel (counter_n, [|`FO counter_n|]),
+ transl_cond_updates transl_data num_functions cond_updates))
counter_cls in
let rule =
ContinuousRule.make_rule signat [] discrete
Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/TranslateGameTest.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -361,14 +361,24 @@
let a () =
set_debug_level 4;
- simult_test_case ~game_name:"2player_normal_form_joint" ~player:"row"
+ simult_test_case ~game_name:"pacman3p" ~player:"pacman"
~plnum:1 (* 0 is environment! *)
- ~moves:[|"r1"; "c1"|]
+ ~moves:[|"(move east)"; "(move nowhere)"; "(move nowhere)"|]
~rules_and_embs:[|
- "m", ["did__BLANK__m", "did__BLANK__r1";
- "synch_control_", "synch_control_"];
- "m2", ["did__BLANK__m2", "did__BLANK__c1";
- "synch_control_", "synch_control_"] |];
+ "move_east", [
+ "gdl__counter", "gdl__counter";
+ "location__BLANK__x10_y10", "location__BLANK__6_3";
+ "location__BLANK__x9_y9", "location__BLANK__5_3";
+ "location__BLANK__x_y", "location__BLANK__5_3";
+ "synch_control_", "synch_control_"];
+ "move_nowhere0", [
+ "location__BLANK__x11_y11", "location__BLANK__4_6";
+ "location__BLANK__x12_y12", "location__BLANK__4_6";
+ "synch_control_", "synch_control_"];
+ "move_nowhere1", [
+ "location__BLANK__x13_y13", "location__BLANK__5_6";
+ "location__BLANK__x14_y14", "location__BLANK__5_6";
+ "synch_control_", "synch_control_"]|];
(* failwith "tested"; *)
()
@@ -414,7 +424,7 @@
(* regenerate ~debug:false ~game_name:"connect4" ~player:"white"; *)
(* regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row"; *)
(* regenerate ~debug:false ~game_name:"2player_normal_form_joint" ~player:"row"; *)
- (* regenerate ~debug:true ~game_name:"pacman3p" ~player:"pacman"; *)
+ (* regenerate ~debug:false ~game_name:"pacman3p" ~player:"pacman"; *)
(* failwith "generated"; *)
()
Modified: trunk/Toss/GGP/tests/pacman3p-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/pacman3p-raw.toss 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/tests/pacman3p-raw.toss 2011-10-21 22:00:39 UTC (rev 1610)
@@ -187,14 +187,15 @@
location__BLANK___BLANK___BLANK_(location__BLANK__xnew0_y20) and
location__BLANK___BLANK___BLANK_(location__BLANK__x20_y20)))
REL nopellets() =
- ex gdl__counter
- (gdl__counter(gdl__counter) and
- (:collected(gdl__counter) - 35. = 0) and true)
+ ((Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :collected(gdl__counter) - 35.) = 0) and
+ true)
REL terminal() =
(captured() and true) or (nopellets() and true) or (timeout() and true)
REL timeout() =
- ex gdl__counter
- (gdl__counter(gdl__counter) and (:step(gdl__counter) - 100. = 0) and true)
+ ((Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :step(gdl__counter) - 100.) = 0) and
+ true)
PLAYERS environment, pacman, blinky, inky
RULE move_east:
[gdl__counter, location__BLANK__x10_y10, location__BLANK__x9_y9,
@@ -257,25 +258,27 @@
location_0pellet
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__east(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__east(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -343,25 +346,27 @@
location_0pellet
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__north(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__north(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -429,25 +434,27 @@
location_0pellet
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__south(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__south(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -515,25 +522,27 @@
location_0pellet
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__west(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__west(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -594,25 +603,28 @@
location_0pellet
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__nowhere(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__nowhere(location__BLANK__x5_y5,
+ location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__nowhere(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
not
@@ -1271,7 +1283,8 @@
location_0pellet
update
:step(gdl__counter) =
- :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.)
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.))
RULE environment0:
[gdl__counter, control__BLANK_, synch_control_ |
_opt_blinky__SYNC {gdl__counter; control__BLANK_};
@@ -1297,7 +1310,8 @@
location_0pellet
update
:step(gdl__counter) =
- :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.)
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.))
LOC 0 {
PLAYER environment { PAYOFF 0.
Modified: trunk/Toss/GGP/tests/pacman3p-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/pacman3p-simpl.toss 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/GGP/tests/pacman3p-simpl.toss 2011-10-21 22:00:39 UTC (rev 1610)
@@ -58,12 +58,12 @@
location__BLANK___BLANK___BLANK_(location__BLANK__xnew0_y20) and
not blocked(v0, location__BLANK__xnew0_y20))
REL nopellets() =
- ex gdl__counter
- (gdl__counter(gdl__counter) and (:collected(gdl__counter) - 35. = 0))
+ (Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :collected(gdl__counter) - 35.) = 0)
REL terminal() = captured() or nopellets() or timeout()
REL timeout() =
- ex gdl__counter
- (gdl__counter(gdl__counter) and (:step(gdl__counter) - 100. = 0))
+ (Sum (gdl__counter | gdl__counter(gdl__counter) : :step(gdl__counter) - 100.
+ ) = 0)
PLAYERS environment, pacman, blinky, inky
DATA R0: EQ___location_1__location_1__AND__c43c43__location_2__location_2,
R: EQ___location_2__location_2__AND__c43c43__location_1__location_1
@@ -128,25 +128,27 @@
pacman__SYNC
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__east(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__east(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__east(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -213,25 +215,27 @@
pacman__SYNC
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__north(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__north(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__north(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -298,25 +302,27 @@
pacman__SYNC
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__south(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__south(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__south(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -383,25 +389,27 @@
pacman__SYNC
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__west(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__west(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__west(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
(not terminal() and
ex val__pacman, control__BLANK_
@@ -461,27 +469,30 @@
pacman__SYNC
update
:collected(gdl__counter) =
- :(
- ex location__BLANK__x6_y6, location__BLANK__x5_y5
- (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
- location_0pacman(location__BLANK__x5_y5) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
- not
- (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
- location_0pellet(location__BLANK__x6_y6) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
- ) * :collected(gdl__counter) +
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
:(
- ex location__BLANK__x3_y3, location__BLANK__x4_y4
- (nextcell__nowhere(location__BLANK__x3_y3, location__BLANK__x4_y4) and
- location_0pacman(location__BLANK__x3_y3) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
- location_0pellet(location__BLANK__x4_y4) and
- location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
- ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ ex location__BLANK__x6_y6, location__BLANK__x5_y5
+ (nextcell__nowhere(location__BLANK__x5_y5, location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6) and
+ location_0pacman(location__BLANK__x5_y5) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x5_y5) and
+ not
+ (nextcell__nowhere(location__BLANK__x5_y5,
+ location__BLANK__x6_y6) and
+ location_0pellet(location__BLANK__x6_y6) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x6_y6)))
+ ) * :collected(gdl__counter) +
+ :(
+ ex location__BLANK__x3_y3, location__BLANK__x4_y4
+ (nextcell__nowhere(location__BLANK__x3_y3, location__BLANK__x4_y4) and
+ location_0pacman(location__BLANK__x3_y3) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x3_y3) and
+ location_0pellet(location__BLANK__x4_y4) and
+ location__BLANK___BLANK___BLANK_(location__BLANK__x4_y4))
+ ) * (1. * (:collected(gdl__counter) - 98.) + 99.)
+ )
pre
- (val__0pacman(val__pacman) and not terminal() and
+ (not terminal() and ex val__pacman val__0pacman(val__pacman) and
not
ex control__BLANK_
(control__BLANK_(control__BLANK_) and control_0pacman(control__BLANK_)))
@@ -785,7 +796,7 @@
location_0blinky, location_0inky, location_0pacman, location_0pellet,
pacman__SYNC
pre
- (val__0blinky(val__blinky) and not terminal() and
+ (not terminal() and ex val__blinky val__0blinky(val__blinky) and
not
ex control__BLANK_
(control__BLANK_(control__BLANK_) and control_0ghosts(control__BLANK_)))
@@ -1084,7 +1095,7 @@
location_0blinky, location_0inky, location_0pacman, location_0pellet,
pacman__SYNC
pre
- (val__0inky(val__inky) and not terminal() and
+ (not terminal() and ex val__inky val__0inky(val__inky) and
not
ex control__BLANK_
(control__BLANK_(control__BLANK_) and control_0ghosts(control__BLANK_)))
@@ -1113,7 +1124,8 @@
pacman__SYNC
update
:step(gdl__counter) =
- :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.)
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.))
RULE environment0:
[gdl__counter, control__BLANK_, synch_control_ |
_opt_blinky__SYNC {gdl__counter; control__BLANK_};
@@ -1139,7 +1151,8 @@
pacman__SYNC
update
:step(gdl__counter) =
- :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.)
+ Sum (gdl__counter | gdl__counter(gdl__counter) :
+ :((true and true)) * (1. * (:step(gdl__counter) - 98.) + 99.))
LOC 0 {
PLAYER environment { PAYOFF 0.
Modified: trunk/Toss/Server/ReqHandler.ml
===================================================================
--- trunk/Toss/Server/ReqHandler.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/Server/ReqHandler.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -154,7 +154,7 @@
if rewrites = [] || TranslateGame.is_turnbased gdl_transl
then state
else failwith
- "ReqHandler: implement performing a move by player Environment" in
+ "ReqHandler: implement performing a move by player \"environment\"" in
let resp =
if (match rq with
| Aux.Right (GDL.Stop (_, actions)) -> true
Modified: trunk/Toss/Solver/RealQuantElim/Poly.ml
===================================================================
--- trunk/Toss/Solver/RealQuantElim/Poly.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/Solver/RealQuantElim/Poly.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -74,7 +74,8 @@
let scale = 1000000 in
let f_scaled = f *. (float_of_int scale) in
let num_scale = Num.num_of_int scale in
- let num_f_scaled = Num.num_of_string (Printf.sprintf "%.0f" f_scaled) in
+ let num_f_scaled =
+ Num.num_of_int (int_of_float f_scaled) in
Num.div_num num_f_scaled num_scale
(* List variables in the given polynomial. *)
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2011-10-21 14:16:20 UTC (rev 1609)
+++ trunk/Toss/Solver/Solver.ml 2011-10-21 22:00:39 UTC (rev 1610)
@@ -240,7 +240,10 @@
let e = List.assoc v assgn in
Poly.Const (Structure.fun_val model s e)
with Not_found ->
- (* TODO: handling partial functions, remove this comment if OK *)
+ (*failwith (
+ "Solver.assignment_of_real_expr: partial function " ^
+ s ^ "(" ^ Formula.var_str v ^ ")")*)
+ (* TODO: handling partial functions *)
Poly.Const nan)
| Char phi -> (
let make_fo_asg asg (v, e) = FO (v, [(e, asg)]) in
@@ -252,6 +255,8 @@
| Sum (_, guard, r) -> (* FIXME; TODO; for many vars is that ok? *)
let make_fo_asg asg (v, e) = FO (v, [(e, asg)]) in
let fo_aset = List.fold_left make_fo_asg Any assgn in
+ (* TODO: problems with partial functions whose domain is
+ given by the guard. *)
let r_a = assignment_of_real_expr fp ~check:false model elems (r,sgn) in
let asg = join (eval fp model elems fo_aset guard) r_a in
sum_polys asg (* Note: above "sgn" is irrelevant! *)
@@ -455,11 +460,15 @@
when r="#" -> (
match Poly.simp_const p with
Poly.Const x -> x
- | _ -> failwith "get_real_val on expr with free vars"
+ | _ -> (* nan *)
+ failwith ("get_real_val on expr with free vars: " ^
+ Formula.real_str expr)
)
- | ev_assgn ->
+ | ev_assgn -> (* nan *)
failwith (
- "get_real_val on expression with free variables" ^
+ "get_real_val on expression with free variables: expr=" ^
+ Formula.real_str expr ^
+ "; assgn=" ^
AssignmentSet.str ev_assgn) in
get_rval (join asg (evaluate_real "#" expr struc))
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
