[Toss-devel-svn] SF.net SVN: toss:[1565] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1565] trunk/Toss
|
From: <luk...@us...> - 2011-09-12 22:25:17
|
Revision: 1565
http://toss.svn.sourceforge.net/toss/?rev=1565&view=rev
Author: lukaszkaiser
Date: 2011-09-12 22:25:10 +0000 (Mon, 12 Sep 2011)
Log Message:
-----------
Adapting update and dynamics syntax to real_expr, correcting tests.
Modified Paths:
--------------
trunk/Toss/Arena/ArenaTest.ml
trunk/Toss/Arena/ContinuousRuleTest.ml
trunk/Toss/Arena/Term.ml
trunk/Toss/Arena/TermParser.mly
trunk/Toss/Arena/TermTest.ml
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/examples/bounce.toss
trunk/Toss/examples/rewriting_example.toss
Modified: trunk/Toss/Arena/ArenaTest.ml
===================================================================
--- trunk/Toss/Arena/ArenaTest.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Arena/ArenaTest.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -36,11 +36,11 @@
rule_e msg;
let rule_1 =
- "[ 1 | | vx { 1->0. }; vy { 1->0. }; x { 1->-15.4 }; y { 1->-50.6 } ] -> [ 1, 2 | | vx { 1->0., 2->0. }; vy { 1->0., 2->0. }; x { 1->-14.3, 2->6.6 }; y { 1->-77., 2->2.2 } ] with [1 <- 1] update x(1) = 1 pre true inv true post true "in
+ "[ 1 | | vx { 1->0. }; vy { 1->0. }; x { 1->-15.4 }; y { 1->-50.6 } ] -> [ 1, 2 | | vx { 1->0., 2->0. }; vy { 1->0., 2->0. }; x { 1->-14.3, 2->6.6 }; y { 1->-77., 2->2.2 } ] with [1 <- 1] update :x(1) = 1 pre true inv true post true "in
let rule_1_res =
"[1 | | vx {1->0.}; vy {1->0.}; x {1->-15.4}; y {1->-50.6}] -> [1, 2 | | vx {1->0., 2->0.}; vy {1->0., 2->0.}; x {1->-14.3, 2->6.6}; y {1->-77., 2->2.2}] with [1 <- 1]
update
- x(1) = 1.
+ :x(1) = 1.
pre true inv true post true" in
let s = "SET RULE 1 " ^ rule_1 in
let (gs,_) = Arena.handle_request Arena.empty_state (req_of_str s) in
Modified: trunk/Toss/Arena/ContinuousRuleTest.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRuleTest.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Arena/ContinuousRuleTest.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -29,18 +29,18 @@
let r = rule_of_str s signat [] "rule1" in
assert_equal ~msg:"1. no continuous" ~printer:(fun x->x) s (str r);
- let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
+ let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\nupdate\n" ^ upd_eq ^ " pre true inv true post true" in
let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (str r);
- let dyn_eq = " f(a)' = (2. * f(a)) + t;\n f(b)' = f(b)" in
+ let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ " pre true inv true post true" in
let r = rule_of_str s signat [] "rule3" in
assert_equal ~msg:"3. dynamics" ~printer:(fun x->x) s (str r);
- let dyn_eq = " f(a)' = (2. * f(a)) + t;\n f(b)' = f(b)" in
- let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
+ let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
+ let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" pre true inv true post true" in
let r = rule_of_str s signat [] "rule4" in
@@ -56,15 +56,15 @@
let r = rule_of_str s signat [] "rule1" in
assert_equal ~msg:"1. no continuous" ~printer:(fun x->x) s (sprint r);
- let upd_eq1 = " f(c) = 2. * f(a);"
- and upd_eq2 = " f(d) = f(b)" in
+ let upd_eq1 = " :f(c) = 2. * :f(a);"
+ and upd_eq2 = " :f(d) = :f(b)" in
let upd_eq = upd_eq1 ^ upd_eq2 in
let s = discr ^ "\n update" ^ upd_eq in
let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (sprint r);
- let dyn_eq1 = " f(a)' = 2. * f(a) + t;"
- and dyn_eq2 = " f(b)' = f(b)" in
+ let dyn_eq1 = " :f(a)' = 2. * :f(a) + t;"
+ and dyn_eq2 = " :f(b)' = :f(b)" in
let dyn_eq = dyn_eq1 ^ dyn_eq2 in
let s = discr ^ "\n dynamics" ^ dyn_eq in
let r = rule_of_str s signat [] "rule3" in
@@ -88,8 +88,8 @@
let dr =
"[| P { (a) } | ] -> [| P:1{}; Q { (b) } | ] emb P with [b<-a]" in
let signat = ["P", 1; "Q", 1] in
- let dyn_eq = "x(a)' = x(a) + t" in
- let upd_eq = "x(b) = x(a)" in
+ let dyn_eq = ":x(a)' = :x(a) + t" in
+ let upd_eq = ":x(b) = :x(a)" in
let s = dr ^ " dynamics " ^ dyn_eq ^ " update " ^ upd_eq ^
" pre true inv true post true " in
let struc = struc_of_str "[ | P {a}; Q:1{} | x { a -> 0.0 } ]" in
@@ -107,8 +107,8 @@
(fun () ->
let dr =
"[| P { (a) } | ] -> [| P:1{}; Q { (b) } | ] emb P with [b<-a]" in
- let dyn_eq = "x(a)' = x(a) + t" in
- let upd_eq = "x(b) = x(a)" in
+ let dyn_eq = ":x(a)' = :x(a) + t" in
+ let upd_eq = ":x(b) = :x(a)" in
let s = dr ^ " dynamics " ^ dyn_eq ^ " update " ^ upd_eq ^
" pre true inv true post true " in
let signat = ["P", 1; "Q", 1] in
@@ -140,22 +140,22 @@
(true,"equal")
(ContinuousRule.compare_diff r1 r2);
- let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
+ let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\nupdate\n" ^ upd_eq ^ " pre true inv true post true" in
let r1 = rule_of_str s signat [] "rule2" in
- let upd_eq = " f(c) = 3. * f(a);\n f(d) = f(b)\n" in
+ let upd_eq = " :f(c) = 3. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\nupdate\n" ^ upd_eq ^ " pre true inv true post true" in
let r2 = rule_of_str s signat [] "rule3" in
assert_equal ~printer:(fun (_,x)->x) ~msg:"2. update"
(false,"Rule update functions differ")
(ContinuousRule.compare_diff r1 r2);
- let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
- let dyn_eq = " f(a)' = (2. * f(a)) + t;\n f(b)' = f(b)" in
+ let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
+ let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" pre true inv true post true" in
let r1 = rule_of_str s signat [] "rule4" in
- let dyn_eq = " f(a)' = (3. * f(a)) + t;\n f(b)' = f(b)" in
+ let dyn_eq = " :f(a)' = (3. * :f(a)) + t;\n :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" pre true inv true post true" in
let r2 = rule_of_str s signat [] "rule5" in
Modified: trunk/Toss/Arena/Term.ml
===================================================================
--- trunk/Toss/Arena/Term.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Arena/Term.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -21,8 +21,8 @@
(* Print a term as a string. *)
let rec str = function
- Var s -> s
- | FVar (f, a) -> f ^ "(" ^ a ^ ")"
+ | Var s -> s
+ | FVar (f, a) -> ":" ^ f ^ "(" ^ a ^ ")"
| Const n -> string_of_float n
| Times (p, q) -> term_pair_str " * " p q
| Plus (p, Times (Const c, q)) when c = -1. -> term_pair_str " - " p q
@@ -41,7 +41,7 @@
(* Print an equation system as a string. *)
-let eq_str ?(diff=false) eqs =
+let eq_str ?(diff=true) eqs =
let sing_str ((f, a), t) =
let mid_str = if diff then "' = " else " = " in
let l_str = str (FVar (f, a)) in
@@ -52,7 +52,7 @@
(* Bracket-savvy precedences: + 0, - 1, * 2, / 3 *)
let rec fprint ?(prec=0) ppf = function
| Var s -> Format.pp_print_string ppf s
- | FVar (f, a) -> Format.fprintf ppf "%s(%s)" f a
+ | FVar (f, a) -> Format.fprintf ppf ":%s(%s)" f a
| Const n -> Format.fprintf ppf "%F" n
| Times (p, q) ->
let lb, rb =
@@ -87,7 +87,7 @@
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@]@]"
+ Format.fprintf ppf "@[<1>:%s(%s)%s@ =@ @[<1>%a@]@]"
f a mid_str (fprint ~prec:0) t in
Format.fprintf ppf "@[<hv>%a@]" (Aux.fprint_sep_list ";" sing) eqs
Modified: trunk/Toss/Arena/TermParser.mly
===================================================================
--- trunk/Toss/Arena/TermParser.mly 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Arena/TermParser.mly 2011-09-12 22:25:10 UTC (rev 1565)
@@ -18,8 +18,8 @@
| INT { Term.Const (float_of_int $1) }
| FLOAT { Term.Const ($1) }
| ID { Term.Var ($1) }
- | ID OPEN ID CLOSE { Term.FVar ($1, $3) }
- | ID OPEN INT CLOSE { Term.FVar ($1, string_of_int $3) }
+ | COLON ID OPEN ID CLOSE { Term.FVar ($2, $4) }
+ | COLON ID OPEN INT CLOSE { Term.FVar ($2, string_of_int $4) }
| term_expr FLOAT { Term.Plus ($1, Term.Const $2) } /* in x-1, "-1" is int */
| term_expr INT { Term.Plus ($1, Term.Const (float_of_int $2)) }
| term_expr PLUS term_expr { Term.Plus ($1, $3) }
@@ -29,11 +29,11 @@
| term_expr POW INT { Term.pow $1 $3 }
| OPEN term_expr CLOSE { $2 }
-eq_expr: /* we do not distinguish standard and differential equations here */
- | ID OPEN ID CLOSE EQ term_expr { (($1, $3), $6) }
- | ID OPEN INT CLOSE EQ term_expr { (($1, string_of_int $3), $6) }
- | ID OPEN ID CLOSE APOSTROPHE EQ term_expr { (($1, $3), $7) }
- | ID OPEN INT CLOSE APOSTROPHE EQ term_expr { (($1, string_of_int $3), $7) }
+eq_expr: /* differential equations only */
+ | COLON ID OPEN ID CLOSE APOSTROPHE EQ term_expr
+ { (($2, $4), $8) }
+ | COLON ID OPEN INT CLOSE APOSTROPHE EQ term_expr
+ { (($2, string_of_int $4), $8) }
%public eq_sys:
| eq_expr { [$1] }
Modified: trunk/Toss/Arena/TermTest.ml
===================================================================
--- trunk/Toss/Arena/TermTest.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Arena/TermTest.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -17,10 +17,10 @@
let s = "(x - 0.2) / ((z * y) - 3.)" in
assert_equal ~printer:(fun x->x) s (str (term_of_string s));
- let t0s = "f(a) + t" in
+ let t0s = ":f(a) + t" in
assert_equal ~printer:(fun x->x) t0s (str (term_of_string t0s));
- let eqs = " f(a)' = f(a) + t" in
+ let eqs = " :f(a)' = :f(a) + t" in
assert_equal ~printer:(fun x->x) eqs
(eq_str ~diff:true (eqs_of_string eqs));
@@ -31,10 +31,10 @@
let s = "(x - 0.2) / (z * y - 3.)" in
assert_equal ~printer:(fun x->x) s (sprint (term_of_string s));
- let t0s = "f(a) + t" in
+ let t0s = ":f(a) + t" in
assert_equal ~printer:(fun x->x) t0s (sprint (term_of_string t0s));
- let eqs = "f(a)' = f(a) + t" in
+ let eqs = ":f(a)' = :f(a) + t" in
assert_equal ~printer:(fun x->x) eqs
(sprint_eqs ~diff:true (eqs_of_string eqs));
@@ -42,9 +42,9 @@
"substitute" >::
(fun () ->
- let t0 = term_of_string "f(a) + t" in
+ let t0 = term_of_string ":f(a) + t" in
let t1 = subst ("t", (Const 2.)) t0 in
- assert_equal ~printer:(fun x->x) "f(a) + 2." (str t1);
+ assert_equal ~printer:(fun x->x) ":f(a) + 2." (str t1);
assert_equal ~printer:(fun x->x) "5."
(str (List.hd (subst_simp_f ["f", "a"] [Const 3.] [t1])));
@@ -52,14 +52,14 @@
"rk4" >::
(fun () ->
- let t0 = term_of_string "f(a) + t" in
+ let t0 = term_of_string ":f(a) + t" in
assert_equal ~printer:(fun x->x) "0.005"
(String.sub (str (List.hd (
rk4_step "t" (Const 0.) (Const 0.1)
[("f", "a"), t0] [Const 0.]))) 0 5);
- let eqs = eqs_of_string "f(a)' = f(a) + t" in
+ let eqs = eqs_of_string ":f(a)' = :f(a) + t" in
assert_equal ~printer:(fun x->x) "0.005"
(String.sub (str (List.hd (
rk4_step "t" (Const 0.) (Const 0.1) eqs [Const 0.]))) 0 5);
Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Formula/Formula.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -222,6 +222,10 @@
and fprint_real_prec prec f = function
| RVar s -> Format.fprintf f "%s" s
| Const fl -> Format.fprintf f "%F" fl
+ | Plus (r1, Times (Const fl, r2)) when fl = -1. -> (* r1 - r2 short *)
+ let lb, rb = if prec > 0 then "(", ")" else "", "" in
+ Format.fprintf f "@[<1>%s%a@ -@ %a%s@]" lb
+ (fprint_real_prec 0) r1 (fprint_real_prec 0) r2 rb
| Times (r1, r2) ->
let lb, rb =
if prec > 2 then "(", ")" else "", "" in
@@ -265,7 +269,7 @@
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@]@]"
+ 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
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Formula/FormulaParser.mly 2011-09-12 22:25:10 UTC (rev 1565)
@@ -44,6 +44,7 @@
| FLOAT { Const ($1) }
| COLON ID { RVar (":" ^ $2) }
| COLON ID OPEN ID CLOSE { Fun ($2, fo_var_of_s $4) }
+ | COLON ID OPEN INT CLOSE { Fun ($2, fo_var_of_s (string_of_int $4)) }
| real_expr FLOAT { Plus ($1, Const $2) } /* in x-1, "-1" is int */
| real_expr INT { Plus ($1, Const (float_of_int $2)) }
| real_expr PLUS real_expr { Plus ($1, $3) }
@@ -123,11 +124,9 @@
{ 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) }
+expr_eq_expr: /* only standard equations here for now (no differentials) */
+ | COLON ID OPEN ID CLOSE EQ real_expr { (($2, $4), $7) }
+ | COLON ID OPEN INT CLOSE EQ real_expr { (($2, string_of_int $4), $7) }
%public expr_eq_sys:
| expr_eq_expr { [$1] }
Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/Play/HeuristicTest.ml 2011-09-12 22:25:10 UTC (rev 1565)
@@ -199,7 +199,7 @@
"of_payoff: tic-tac-toe non monotonic" >::
(fun () ->
assert_eq_str ~msg:"adv_ratio=1.5"
- "Sum (x | P(x) : 0.64 + Sum (y | (R(x, y) and P(y)) : 0.96 + Sum (z | (R(y, z) and P(z)) : 1.44)) + Sum (y | (C(x, y) and P(y)) : 0.96 + Sum (z | (C(y, z) and P(z)) : 1.44)) + Sum (v0 | R(x, v0) : 0.29 + Sum (y | (C(v0, y) and P(y)) : 0.44 + Sum (u0 | R(y, u0) : 0.66 + Sum (z | (C(u0, z) and P(z)) : 1.))) ) + Sum (v | R(x, v) : 0.29 + Sum (y | (C(y, v) and P(y)) : 0.44 + Sum (u | R(y, u) : 0.66 + Sum (z | (C(z, u) and P(z)) : 1.))) ) ) + -1. * Sum (x | Q(x) : 0.64 + Sum (y | (R(x, y) and Q(y)) : 0.96 + Sum (z | (R(y, z) and Q(z)) : 1.44)) + Sum (y | (C(x, y) and Q(y)) : 0.96 + Sum (z | (C(y, z) and Q(z)) : 1.44)) + Sum (v0 | R(x, v0) : 0.29 + Sum (y | (C(v0, y) and Q(y)) : 0.44 + Sum (u0 | R(y, u0) : 0.66 + Sum (z | (C(u0, z) and Q(z)) : 1.)) ) ) + Sum (v | R(x, v) : 0.29 + Sum (y | (C(y, v) and Q(y)) : 0.44 + Sum (u | R(y, u) : 0.66 + Sum (z | (C(z, u) and Q(z)) : 1.))) ) )"
+ "Sum (x | P(x) : 0.64 + Sum (y | (R(x, y) and P(y)) : 0.96 + Sum (z | (R(y, z) and P(z)) : 1.44)) + Sum (y | (C(x, y) and P(y)) : 0.96 + Sum (z | (C(y, z) and P(z)) : 1.44)) + Sum (v0 | R(x, v0) : 0.29 + Sum (y | (C(v0, y) and P(y)) : 0.44 + Sum (u0 | R(y, u0) : 0.66 + Sum (z | (C(u0, z) and P(z)) : 1.))) ) + Sum (v | R(x, v) : 0.29 + Sum (y | (C(y, v) and P(y)) : 0.44 + Sum (u | R(y, u) : 0.66 + Sum (z | (C(z, u) and P(z)) : 1.))) ) ) - Sum (x | Q(x) : 0.64 + Sum (y | (R(x, y) and Q(y)) : 0.96 + Sum (z | (R(y, z) and Q(z)) : 1.44)) + Sum (y | (C(x, y) and Q(y)) : 0.96 + Sum (z | (C(y, z) and Q(z)) : 1.44)) + Sum (v0 | R(x, v0) : 0.29 + Sum (y | (C(v0, y) and Q(y)) : 0.44 + Sum (u0 | R(y, u0) : 0.66 + Sum (z | (C(u0, z) and Q(z)) : 1.))) ) + Sum (v | R(x, v) : 0.29 + Sum (y | (C(y, v) and Q(y)) : 0.44 + Sum (u | R(y, u) : 0.66 + Sum (z | (C(z, u) and Q(z)) : 1.))) ) )"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(Heuristic.of_payoff 1.5
@@ -207,7 +207,7 @@
(real_of_str (":("^winPxyz^") - :("^winQxyz^")")))));
assert_eq_str ~msg:"adv_ratio=10"
- "Sum (x | P(x) : 0.0101 + Sum (y | (R(x, y) and P(y)) : 0.101 + Sum (z | (R(y, z) and P(z)) : 1.01)) + Sum (y | (C(x, y) and P(y)) : 0.101 + Sum (z | (C(y, z) and P(z)) : 1.01)) + Sum (v0 | R(x, v0) : 0.001 + Sum (y | (C(v0, y) and P(y)) : 0.01 + Sum (u0 | R(y, u0) : 0.1 + Sum (z | (C(u0, z) and P(z)) : 1.))) ) + Sum (v | R(x, v) : 0.001 + Sum (y | (C(y, v) and P(y)) : 0.01 + Sum (u | R(y, u) : 0.1 + Sum (z | (C(z, u) and P(z)) : 1.))) ) ) + -1. * Sum (x | Q(x) : 0.0101 + Sum (y | (R(x, y) and Q(y)) : 0.101 + Sum (z | (R(y, z) and Q(z)) : 1.01) ) + Sum (y | (C(x, y) and Q(y)) : 0.101 + Sum (z | (C(y, z) and Q(z)) : 1.01) ) + Sum (v0 | R(x, v0) : 0.001 + Sum (y | (C(v0, y) and Q(y)) : 0.01 + Sum (u0 | R(y, u0) : 0.1 + Sum (z | (C(u0, z) and Q(z)) : 1.))) ) + Sum (v | R(x, v) : 0.001 + Sum (y | (C(y, v) and Q(y)) : 0.01 + Sum (u | R(y, u) : 0.1 + Sum (z | (C(z, u) and Q(z)) : 1.))) ) )"
+ "Sum (x | P(x) : 0.0101 + Sum (y | (R(x, y) and P(y)) : 0.101 + Sum (z | (R(y, z) and P(z)) : 1.01)) + Sum (y | (C(x, y) and P(y)) : 0.101 + Sum (z | (C(y, z) and P(z)) : 1.01)) + Sum (v0 | R(x, v0) : 0.001 + Sum (y | (C(v0, y) and P(y)) : 0.01 + Sum (u0 | R(y, u0) : 0.1 + Sum (z | (C(u0, z) and P(z)) : 1.))) ) + Sum (v | R(x, v) : 0.001 + Sum (y | (C(y, v) and P(y)) : 0.01 + Sum (u | R(y, u) : 0.1 + Sum (z | (C(z, u) and P(z)) : 1.))) ) ) - Sum (x | Q(x) : 0.0101 + Sum (y | (R(x, y) and Q(y)) : 0.101 + Sum (z | (R(y, z) and Q(z)) : 1.01)) + Sum (y | (C(x, y) and Q(y)) : 0.101 + Sum (z | (C(y, z) and Q(z)) : 1.01)) + Sum (v0 | R(x, v0) : 0.001 + Sum (y | (C(v0, y) and Q(y)) : 0.01 + Sum (u0 | R(y, u0) : 0.1 + Sum (z | (C(u0, z) and Q(z)) : 1.))) ) + Sum (v | R(x, v) : 0.001 + Sum (y | (C(y, v) and Q(y)) : 0.01 + Sum (u | R(y, u) : 0.1 + Sum (z | (C(z, u) and Q(z)) : 1.))) ) )"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.10000.))/.10000.)
(Heuristic.of_payoff 10.
@@ -219,7 +219,7 @@
"of_payoff: breakthrough expanded" >::
(fun () ->
assert_eq_str
- "Sum (y8 | W(y8) : 0.05 + Sum (y7 | C(y7, y8) : 0.08 + Sum (y6 | C(y6, y7) : 0.13 + Sum (y5 | C(y5, y6) : 0.19 + Sum (y4 | C(y4, y5) : 0.29 + Sum (y3 | C(y3, y4) : 0.44 + Sum (y2 | C(y2, y3) : 0.66 + Sum (y1 | C(y1, y2) : 1.))) ) ) ) ) ) + -1. * Sum (y1 | B(y1) : 0.05 + Sum (y2 | C(y1, y2) : 0.08 + Sum (y3 | C(y2, y3) : 0.13 + Sum (y4 | C(y3, y4) : 0.19 + Sum (y5 | C(y4, y5) : 0.29 + Sum (y6 | C(y5, y6) : 0.44 + Sum (y7 | C(y6, y7) : 0.66 + Sum (y8 | C(y7, y8) : 1.))) ) ) ) ) )"
+ "Sum (y8 | W(y8) : 0.05 + Sum (y7 | C(y7, y8) : 0.08 + Sum (y6 | C(y6, y7) : 0.13 + Sum (y5 | C(y5, y6) : 0.19 + Sum (y4 | C(y4, y5) : 0.29 + Sum (y3 | C(y3, y4) : 0.44 + Sum (y2 | C(y2, y3) : 0.66 + Sum (y1 | C(y1, y2) : 1.))) ) ) ) ) ) - Sum (y1 | B(y1) : 0.05 + Sum (y2 | C(y1, y2) : 0.08 + Sum (y3 | C(y2, y3) : 0.13 + Sum (y4 | C(y3, y4) : 0.19 + Sum (y5 | C(y4, y5) : 0.29 + Sum (y6 | C(y5, y6) : 0.44 + Sum (y7 | C(y6, y7) : 0.66 + Sum (y8 | C(y7, y8) : 1.))) ) ) ) ) )"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(Heuristic.of_payoff 1.5
@@ -227,7 +227,7 @@
(real_of_str (":("^breakW^") - :("^breakB^")")))));
assert_eq_str
- "Sum (y8 | W(y8) : 1e-07 + Sum (y7 | C(y7, y8) : 1e-06 + Sum (y6 | C(y6, y7) : 1e-05 + Sum (y5 | C(y5, y6) : 0.0001 + Sum (y4 | C(y4, y5) : 0.001 + Sum (y3 | C(y3, y4) : 0.01 + Sum (y2 | C(y2, y3) : 0.1 + Sum (y1 | C(y1, y2) : 1.))) ) ) ) ) ) + -1. * Sum (y1 | B(y1) : 1e-07 + Sum (y2 | C(y1, y2) : 1e-06 + Sum (y3 | C(y2, y3) : 1e-05 + Sum (y4 | C(y3, y4) : 0.0001 + Sum (y5 | C(y4, y5) : 0.001 + Sum (y6 | C(y5, y6) : 0.01 + Sum (y7 | C(y6, y7) : 0.1 + Sum (y8 | C(y7, y8) : 1.))) ) ) ) ) )"
+ "Sum (y8 | W(y8) : 1e-07 + Sum (y7 | C(y7, y8) : 1e-06 + Sum (y6 | C(y6, y7) : 1e-05 + Sum (y5 | C(y5, y6) : 0.0001 + Sum (y4 | C(y4, y5) : 0.001 + Sum (y3 | C(y3, y4) : 0.01 + Sum (y2 | C(y2, y3) : 0.1 + Sum (y1 | C(y1, y2) : 1.))) ) ) ) ) ) - Sum (y1 | B(y1) : 1e-07 + Sum (y2 | C(y1, y2) : 1e-06 + Sum (y3 | C(y2, y3) : 1e-05 + Sum (y4 | C(y3, y4) : 0.0001 + Sum (y5 | C(y4, y5) : 0.001 + Sum (y6 | C(y5, y6) : 0.01 + Sum (y7 | C(y6, y7) : 0.1 + Sum (y8 | C(y7, y8) : 1.))) ) ) ) ) )"
(Formula.real_str
(Heuristic.of_payoff 10.
(Aux.strings_of_list ["B"; "W"])
@@ -257,7 +257,7 @@
W..W W..W W..W W..W
\"" in
assert_eq_str
- "Sum (x | W(x) : 1e-07 + Sum (y | C(y, x) : 1e-06 + Sum (y0 | C(y0, y) : 1e-05 + Sum (y1 | C(y1, y0) : 0.0001 + Sum (y2 | C(y2, y1) : 0.001 + Sum (y3 | C(y3, y2) : 0.01 + Sum (y4 | C(y4, y3) : 0.1 + Sum (y5 | C(y5, y4) : 1.))) ) ) ) ) ) + -1. * Sum (x | B(x) : 1e-07 + Sum (y | C(x, y) : 1e-06 + Sum (y0 | C(y, y0) : 1e-05 + Sum (y1 | C(y0, y1) : 0.0001 + Sum (y2 | C(y1, y2) : 0.001 + Sum (y3 | C(y2, y3) : 0.01 + Sum (y4 | C(y3, y4) : 0.1 + Sum (y5 | C(y4, y5) : 1.))) ) ) ) ) )"
+ "Sum (x | W(x) : 1e-07 + Sum (y | C(y, x) : 1e-06 + Sum (y0 | C(y0, y) : 1e-05 + Sum (y1 | C(y1, y0) : 0.0001 + Sum (y2 | C(y2, y1) : 0.001 + Sum (y3 | C(y3, y2) : 0.01 + Sum (y4 | C(y4, y3) : 0.1 + Sum (y5 | C(y5, y4) : 1.))) ) ) ) ) ) - Sum (x | B(x) : 1e-07 + Sum (y | C(x, y) : 1e-06 + Sum (y0 | C(y, y0) : 1e-05 + Sum (y1 | C(y0, y1) : 0.0001 + Sum (y2 | C(y1, y2) : 0.001 + Sum (y3 | C(y2, y3) : 0.01 + Sum (y4 | C(y3, y4) : 0.1 + Sum (y5 | C(y4, y5) : 1.))) ) ) ) ) )"
(Formula.real_str
(Heuristic.of_payoff ~struc:state 10.
(Aux.strings_of_list ["B"; "W"])
@@ -274,14 +274,14 @@
"[a | P:1 {}; Q:1 {} | ] -> [ | P:1 {}; Q(a) | ] emb P, Q"] in
assert_eq_str
- "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * 0.33) + -1. * Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.33)"
+ "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * 0.33) - Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.33)"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(default_heuristic 1. rules
(real_of_str (":("^winPxyz^") - :("^winQxyz^")")))));
assert_eq_str
- "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * (:(P(x)) + :(P(y)) + :(P(z))) * 0.11) + -1. * Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.11)"
+ "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * (:(P(x)) + :(P(y)) + :(P(z))) * 0.11) - Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.11)"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(default_heuristic 2. rules
@@ -297,14 +297,14 @@
"[a | P:1 {}; Q:1 {} | ] -> [ | P:1 {}; Q(a) | ] emb P, Q"] in
assert_eq_str
- "Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.04 ) + -1. * Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.04 )"
+ "Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.04 ) - Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.04 )"
(Formula.real_str
((* Heuristic.map_constants (fun c->(floor (c*.100.))/.100.) *)
(default_heuristic 2. rules
(real_of_str (":("^winPvwxyz^") - :("^winQvwxyz^")")))));
assert_eq_str
- "Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.008 ) + -1. * Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.008 )"
+ "Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.008 ) - Sum (z, y, x, w, v | (((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u (C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)) or ex r, s, t, u (R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.008 )"
(Formula.real_str
((* Heuristic.map_constants (fun c->(floor (c*.1000.))/.1000.) *)
(default_heuristic 3. rules
@@ -333,7 +333,7 @@
(* non-monotonic *)
assert_eq_str
- "Sum (x | P(x) : 0.015625 + Sum (y | (R(x, y) and P(y)) : 0.0625 + Sum (z | (R(y, z) and P(z)) : 0.25 + Sum (v | (R(z, v) and P(v)) : 1.)) ) + Sum (y | (C(x, y) and P(y)) : 0.0625 + Sum (z | (C(y, z) and P(z)) : 0.25 + Sum (v | (C(z, v) and P(v)) : 1.)) ) + Sum (y | (DiagA(x, y) and P(y)) : 0.0625 + Sum (z | (DiagA(y, z) and P(z)) : 0.25 + Sum (v | (DiagA(z, v) and P(v)) : 1.)) ) + Sum (y | (DiagB(x, y) and P(y)) : 0.0625 + Sum (z | (DiagB(y, z) and P(z)) : 0.25 + Sum (v | (DiagB(z, v) and P(v)) : 1.)) ) ) + -1. * Sum (x | Q(x) : 0.015625 + Sum (y | (R(x, y) and Q(y)) : 0.0625 + Sum (z | (R(y, z) and Q(z)) : 0.25 + Sum (v | (R(z, v) and Q(v)) : 1.)) ) + Sum (y | (C(x, y) and Q(y)) : 0.0625 + Sum (z | (C(y, z) and Q(z)) : 0.25 + Sum (v | (C(z, v) and Q(v)) : 1.)) ) + Sum (y | (DiagA(x, y) and Q(y)) : 0.0625 + Sum (z | (DiagA(y, z) and Q(z)) : 0.25 + Sum (v | (DiagA(z, v) and Q(v)) : 1.)) ) + Sum (y | (DiagB(x, y) and Q(y)) : 0.0625 + Sum (z | (DiagB(y, z) and Q(z)) : 0.25 + Sum (v | (DiagB(z, v) and Q(v)) : 1.)) ) )"
+ "Sum (x | P(x) : 0.015625 + Sum (y | (R(x, y) and P(y)) : 0.0625 + Sum (z | (R(y, z) and P(z)) : 0.25 + Sum (v | (R(z, v) and P(v)) : 1.)) ) + Sum (y | (C(x, y) and P(y)) : 0.0625 + Sum (z | (C(y, z) and P(z)) : 0.25 + Sum (v | (C(z, v) and P(v)) : 1.)) ) + Sum (y | (DiagA(x, y) and P(y)) : 0.0625 + Sum (z | (DiagA(y, z) and P(z)) : 0.25 + Sum (v | (DiagA(z, v) and P(v)) : 1.)) ) + Sum (y | (DiagB(x, y) and P(y)) : 0.0625 + Sum (z | (DiagB(y, z) and P(z)) : 0.25 + Sum (v | (DiagB(z, v) and P(v)) : 1.)) ) ) - Sum (x | Q(x) : 0.015625 + Sum (y | (R(x, y) and Q(y)) : 0.0625 + Sum (z | (R(y, z) and Q(z)) : 0.25 + Sum (v | (R(z, v) and Q(v)) : 1.)) ) + Sum (y | (C(x, y) and Q(y)) : 0.0625 + Sum (z | (C(y, z) and Q(z)) : 0.25 + Sum (v | (C(z, v) and Q(v)) : 1.)) ) + Sum (y | (DiagA(x, y) and Q(y)) : 0.0625 + Sum (z | (DiagA(y, z) and Q(z)) : 0.25 + Sum (v | (DiagA(z, v) and Q(v)) : 1.)) ) + Sum (y | (DiagB(x, y) and Q(y)) : 0.0625 + Sum (z | (DiagB(y, z) and Q(z)) : 0.25 + Sum (v | (DiagB(z, v) and Q(v)) : 1.)) ) )"
(Formula.real_str loc_heurs.(0).(0));
);
Modified: trunk/Toss/examples/bounce.toss
===================================================================
--- trunk/Toss/examples/bounce.toss 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/examples/bounce.toss 2011-09-12 22:25:10 UTC (rev 1565)
@@ -4,15 +4,15 @@
->
[ 1 | | vx { 1->0. }; vy { 1->0. }; x { 1->-14.3 }; y { 1->-34.1 } ]
dynamics
- vy(1)' = 50.;
- vx(1)' = 0.;
- y(1)' = vy(1);
- x(1)' = vx(1)
+ :vy(1)' = 50.;
+ :vx(1)' = 0.;
+ :y(1)' = :vy(1);
+ :x(1)' = :vx(1)
update
- vy(1) = (-1.)*(vy(1));
- vx(1) = vx(1);
- y(1) = y(1);
- x(1) = x(1)
+ :vy(1) = (-1.) * :vy(1);
+ :vx(1) = :vx(1);
+ :y(1) = :y(1);
+ :x(1) = :x(1)
pre true
inv ex x ((_lhs_1(x) and ((((:y(x) + (-1. * 0.)) +
(-1. * 0.)) + (-1. * 0.)) < 0)))
Modified: trunk/Toss/examples/rewriting_example.toss
===================================================================
--- trunk/Toss/examples/rewriting_example.toss 2011-09-12 14:56:02 UTC (rev 1564)
+++ trunk/Toss/examples/rewriting_example.toss 2011-09-12 22:25:10 UTC (rev 1565)
@@ -10,31 +10,31 @@
y {4->14.3, 3->-29.7, 2->-30.8, 1->-28.6}
] emb R with [3 <- 2, 2 <- 2, 1 <- 1]
dynamics
- vy(2)' = 0.;
- vy(1)' = 0.;
- vx(2)' = 0.;
- vx(1)' = 0.;
- y(2)' = 0.;
- y(1)' = 0.;
- x(2)' = 0.;
- x(1)' = 0.
+ :vy(2)' = 0.;
+ :vy(1)' = 0.;
+ :vx(2)' = 0.;
+ :vx(1)' = 0.;
+ :y(2)' = 0.;
+ :y(1)' = 0.;
+ :x(2)' = 0.;
+ :x(1)' = 0.
update
- vy(4) = 0.;
- vy(3) = 0.;
- vy(2) = 0.;
- vy(1) = 0.;
- vx(4) = 0.;
- vx(3) = 0.;
- vx(2) = 0.;
- vx(1) = 0.;
- y(4) = 0.5 * y(2);
- y(3) = y(2);
- y(2) = y(2);
- y(1) = y(1);
- x(4) = x(2);
- x(3) = 2. * x(2) - x(1);
- x(2) = x(2);
- x(1) = x(1)
+ :vy(4) = 0.;
+ :vy(3) = 0.;
+ :vy(2) = 0.;
+ :vy(1) = 0.;
+ :vx(4) = 0.;
+ :vx(3) = 0.;
+ :vx(2) = 0.;
+ :vx(1) = 0.;
+ :y(4) = 0.5 * :y(2);
+ :y(3) = :y(2);
+ :y(2) = :y(2);
+ :y(1) = :y(1);
+ :x(4) = :x(2);
+ :x(3) = 2. * :x(2) - :x(1);
+ :x(2) = :x(2);
+ :x(1) = :x(1)
LOC 0 {
PLAYER 1 { PAYOFF 0. MOVES [Rewrite, t: 1. -- 1. -> 0] }
PLAYER 2 { PAYOFF 0. }
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
