[Toss-devel-svn] SF.net SVN: toss:[1196] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1196] trunk/Toss
|
From: <luk...@us...> - 2010-11-27 14:29:25
|
Revision: 1196
http://toss.svn.sourceforge.net/toss/?rev=1196&view=rev
Author: lukaszkaiser
Date: 2010-11-27 14:29:19 +0000 (Sat, 27 Nov 2010)
Log Message:
-----------
Transitive closure syntax.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Tokens.mly
trunk/Toss/Solver/SolverTest.ml
trunk/Toss/examples/Tic-Tac-Toe.tossstyle
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOps.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -234,7 +234,25 @@
All (nvs, rename_quant_avoiding (avs @ nvs) (subst_vars subst phi))
+(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
+(* We construct transitive closure of phi(x, y, z) over x, y as
+ "all X (x in X and (all x',y'
+ (x' in X and phi(x',y',z)-> y' in X)) -> y in X)" *)
+let make_tc x y phi =
+ let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
+ let (_, nx) = subst_name_avoiding fv xv in
+ let (_, ny) = subst_name_avoiding fv yv in
+ let (nxv, nyv) = (fo_var_of_string nx, fo_var_of_string ny) in
+ let frX = mso_var_of_string(snd(subst_name_avoiding fv(var_of_string "X"))) in
+ let nphi = subst_vars [(x, nx); (y, ny)] phi in
+ let impphi = Or [Not (And [In (nxv, frX); nphi]); In (nyv, frX)] in
+ let inphi = And [In (xv, frX); All (([nxv; nyv] :> var list), impphi)] in
+ All ([(frX :> var)], Or [Not inphi; In (yv, frX)])
+
+
+
+
(* --------- SUBSTITUTE DEFINED RELATIONS ------------ *)
(* Substitute in relations defined in [defs] by their definitions. *)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOps.mli 2010-11-27 14:29:19 UTC (rev 1196)
@@ -53,6 +53,10 @@
val assign_emptyset : string -> formula -> formula
+(* ------------------------ Transitive Closure ---------------------------- *)
+
+val make_tc : string -> string -> formula -> formula
+
(* -------------------------- Simplification ------------------------------ *)
(* Recursively simplify a formula *)
Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaOpsTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -258,6 +258,16 @@
[("R", (["x"; "y"], formula_of_string "S (x, y) and ex x S(y, x)"))]
"R (y, x)" "S(y, x) and ex x0 (S(x, x0))";
);
+
+ "transitive closure creation" >::
+ (fun () ->
+ let tc_eq x y phi1 phi2 =
+ formula_eq id phi2 (FormulaOps.make_tc x y) phi1 in
+ tc_eq "x" "y" "R(x, y)" "all X (x in X and (all x0,y0
+ (x0 in X and R(x0,y0) -> y0 in X)) -> y in X)";
+ tc_eq "x" "y" "R(x, y) and x in X" "all X0 (x in X0 and (all x0,y0
+ (x0 in X0 and (R(x0,y0) and x0 in X) -> y0 in X0)) -> y in X0)";
+ );
] ;;
let a =
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/FormulaParser.mly 2010-11-27 14:29:19 UTC (rev 1196)
@@ -76,6 +76,7 @@
| NOT formula_expr { Not ($2) }
| EX var_list formula_expr { Ex ($2, $3) }
| ALL var_list formula_expr { All ($2, $3) }
+ | TC ID COMMA ID formula_expr { FormulaOps.make_tc $2 $4 $5 }
| OPEN formula_expr CLOSE { $2 }
| formula_expr AND formula_expr { And [$1; $3] }
| formula_expr OR formula_expr { Or [$1; $3] }
Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/Lexer.mll 2010-11-27 14:29:19 UTC (rev 1196)
@@ -1,21 +1,4 @@
{
-(* Tokens for parsers: must be in the same order as the type def. below.
-%token <string> ID
-%token <int> INT
-%token <float> FLOAT
-%token <string> BOARD_STRING
-%token APOSTROPHE
-%token COLON SEMICOLON COMMA MID
-%token SUM PLUS MINUS TIMES DIV POW GR GREQ LT EQLT EQ LTGR NEQ
-%token LARR LDARR RARR RDARR LRARR LRDARR INTERV
-%token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
-%token IN AND OR XOR NOT EX ALL
-%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
-%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
-%token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
-%token MODEL_SPEC RULE_SPEC STATE_SPEC LEFT_SPEC RIGHT_SPEC EOF
-*)
-
type token =
| ID of (string)
| INT of (int)
@@ -59,6 +42,7 @@
| NOT
| EX
| ALL
+ | TC
| WITH
| EMB
| PRE
@@ -174,6 +158,8 @@
| "not" { NOT }
| "ex" { EX }
| "all" { ALL }
+ | "tc" { TC }
+ | "TC" { TC }
| "with" { WITH }
| "emb" { EMB }
| "pre" { PRE }
Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Formula/Tokens.mly 2010-11-27 14:29:19 UTC (rev 1196)
@@ -7,7 +7,7 @@
%token SUM PLUS MINUS TIMES DIV POW GR GREQ LT EQLT EQ LTGR NEQ
%token LARR LDARR RARR RDARR LRARR LRDARR INTERV
%token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
-%token IN AND OR XOR NOT EX ALL
+%token IN AND OR XOR NOT EX ALL TC
%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
%token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-27 14:29:19 UTC (rev 1196)
@@ -112,8 +112,7 @@
"eval: mso with quantifiers" >::
(fun () ->
- let reach_f =
- "all X (x in X and (all z,v (z in X and R(z,v)-> v in X))-> y in X)" in
+ let reach_f = "tc x, y R(x, y)" in
eval_eq "[ | R { (a, b); (a, c) } | ]" reach_f
"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 } }";
eval_eq "[ | R { (a, b); (b, c) } | ]" reach_f
Modified: trunk/Toss/examples/Tic-Tac-Toe.tossstyle
===================================================================
--- trunk/Toss/examples/Tic-Tac-Toe.tossstyle 2010-11-24 00:34:10 UTC (rev 1195)
+++ trunk/Toss/examples/Tic-Tac-Toe.tossstyle 2010-11-27 14:29:19 UTC (rev 1196)
@@ -1,6 +1,6 @@
nocolor ;
elOPACITY: 30 ;
relOPACITY: 150 ;
-arrLENscale: 0.1 ;
+arrLENscale: 0 ;
P: ~/greencircle.svg;
Q: ~/cross.svg;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
