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

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

Revision: 1209
          http://toss.svn.sourceforge.net/toss/?rev=1209&view=rev
Author:   lukaszkaiser
Date:     2010-11-29 20:19:39 +0000 (Mon, 29 Nov 2010)

Log Message:
-----------
Preconditions checking and a step towards full chess definition.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/ContinuousRule.ml
    trunk/Toss/Arena/ContinuousRule.mli
    trunk/Toss/examples/Chess.toss

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2010-11-29 17:40:07 UTC (rev 1208)
+++ trunk/Toss/Arena/Arena.ml	2010-11-29 20:19:39 UTC (rev 1209)
@@ -783,7 +783,7 @@
     | GetRuleMatches (r_name) -> (
       try
         let r = List.assoc r_name state.game.rules in
-        let matches = ContinuousRule.matches struc r in
+        let matches = ContinuousRule.matches_post struc r state.time in
         (* matches are from LHS to model *)
         let name (lhs,rhs) = 
           Structure.elem_str (ContinuousRule.lhs r) lhs ^ " -> " ^ 

Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml	2010-11-29 17:40:07 UTC (rev 1208)
+++ trunk/Toss/Arena/ContinuousRule.ml	2010-11-29 20:19:39 UTC (rev 1209)
@@ -79,17 +79,6 @@
     (List.hd ids, List.map List.hd llst) :: 
       (select_pos (List.tl ids) (List.map List.tl llst))
 
-(* Helper function to add a defined relation to structure. *)
-(* let add_def_rel struc (r_name, (vars, _, reg_def)) =
-  let def_asg = SolverIntf.M.evaluate struc reg_def in
-  match def_asg with
-    | AssignmentSet.Empty -> 
-      Structure.add_rel_name r_name (List.length vars) struc
-    | _ ->
-      let tuples = AssignmentSet.tuples struc.Structure.elements vars def_asg in
-      Structure.add_rels struc r_name tuples
-*)
-
 (* For now, we rewrite only single rules. *)
 let rewrite_single struc cur_time m r t params =
   let time = ref cur_time in
@@ -187,6 +176,17 @@
   (DiscreteRule.rule_str r.discrete) ^ " " ^
     dyn_str ^ upd_str ^ pre_str ^ inv_str ^ post_str
 
+
+(* Matches which satisfy postcondition with time 1 and empty params *)
+let matches_post struc r cur_time =
+  let is_ok m = 
+    let (res_struc, _, _) = rewrite_single struc cur_time m r 1. [] in
+    SolverIntf.M.check_formula res_struc r.post_pp in
+  if r.post = Formula.And [] then matches struc r else
+    List.filter is_ok (matches struc r)
+
+
+
 let has_dynamics r = r.dynamics <> []
   (* List.exists (fun (_, t) -> t <> Term.Const 0.) r.dynamics *)
 

Modified: trunk/Toss/Arena/ContinuousRule.mli
===================================================================
--- trunk/Toss/Arena/ContinuousRule.mli	2010-11-29 17:40:07 UTC (rev 1208)
+++ trunk/Toss/Arena/ContinuousRule.mli	2010-11-29 20:19:39 UTC (rev 1209)
@@ -60,7 +60,10 @@
 (* Find all matches of [r] in [struc] which satisfy [r]'s precondition. *)
 val matches : Structure.structure -> rule -> (int * int) list list
 
+(* Matches which satisfy postcondition with time 1 and empty params *)
+val matches_post : Structure.structure -> rule -> float -> (int * int) list list
 
+
 (* --------------------------- REWRITING ------------------------------------ *)
 
 (* For now, we rewrite only single rules.

Modified: trunk/Toss/examples/Chess.toss
===================================================================
--- trunk/Toss/examples/Chess.toss	2010-11-29 17:40:07 UTC (rev 1208)
+++ trunk/Toss/examples/Chess.toss	2010-11-29 20:19:39 UTC (rev 1209)
@@ -22,6 +22,7 @@
 REL Col (x, y) = ex z (FreeC (x, z) and (z = y or (C(z, y) or C(y, z))))
 REL Row (x, y) = ex z (FreeR (x, z) and (z = y or (R(z, y) or R(y, z))))
 REL Line (x, y) = Col (x, y) or Row (x, y)
+REL Near (x, y) = C(x,y) or C(y,x) or R(x,y) or R(y,x) or D1(x, y) or D2(x, y)
 REL wPBeats (x) = ex y (wP(y) and ex z ((R(y, z) or R(z, y)) and C(z, x)))
 REL bPBeats (x) = ex y (bP(y) and ex z ((R(y, z) or R(z, y)) and C(x, z)))
 REL wDiagBeats (x) = ex y ((wQ(y) or wB(y)) and Diag(y, x))
@@ -30,8 +31,8 @@
 REL bLineBeats (x) = ex y ((bQ(y) or bR(y)) and Line(y, x))
 REL wFigBeats(x) = wDiagBeats(x) or wLineBeats(x) or ex y(wN(y) and Knight(y,x))
 REL bFigBeats(x) = bDiagBeats(x) or bLineBeats(x) or ex y(bN(y) and Knight(y,x))
-REL wBeats(x) = wFigBeats(x) or wPBeats(x)
-REL bBeats(x) = bFigBeats(x) or bPBeats(x)
+REL wBeats(x) = wFigBeats(x) or wPBeats(x) or ex y (wK(y) and Near(y, x))
+REL bBeats(x) = bFigBeats(x) or bPBeats(x) or ex y (bK(y) and Near(y, x))
 REL CheckW() = ex x (wK(x) and bBeats(x))
 REL CheckB() = ex x (bK(x) and wBeats(x))
 RULE WhitePawnMove:
@@ -202,6 +203,30 @@
 	...   
 	...?  
 " emb w, b post not CheckB()
+RULE WhitePawnPromote:
+ [ |  | ] "
+	...
+	...
+	   
+	wP 
+" -> [ |  | ] "
+	...
+	wQ.
+	   
+	.  
+" emb w, b pre IsEight(a2) post not CheckW()
+RULE BlackPawnPromote:
+ [ |  | ] "
+	...
+	bP.
+	   
+	.  
+" -> [ |  | ] "
+	...
+	...
+	   
+	bQ 
+" emb w, b pre IsFirst(a1) post not CheckB()
 RULE WhiteKnight:
  [ a, b | wN { a }; _opt_b { b } | 
      vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
@@ -258,6 +283,20 @@
  [ a, b | bQ { b } | 
      vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
  emb w, b pre (Line(a, b) or Diag(a, b)) post not CheckB()
+RULE WhiteKing:
+ [ a, b | wK { a }; _opt_b { b } | 
+     vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
+   -> 
+ [ a, b | wK { b } | 
+     vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
+ emb w, b pre Near(a, b) post not CheckW()
+RULE BlackKing:
+ [ a, b | bK { a }; _opt_w { b } | 
+     vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
+   ->
+ [ a, b | bK { b } | 
+     vx {a->0.,b->10.}; vy {a->0.,b->0.}; x {a->0.,b->10.}; y {a->0.,b->10.} ]
+ emb w, b pre Near(a, b) post not CheckB()
 LOC 0 {
  PLAYER 1
   PAYOFF {
@@ -271,10 +310,12 @@
    [WhitePawnLeftDbl -> 1];
    [WhitePawnRight -> 1];
    [WhitePawnRightDbl -> 1];
+   [WhitePawnPromote -> 1];
    [WhiteKnight -> 1];
    [WhiteBishop -> 1];
    [WhiteRook -> 1];
-   [WhiteQueen -> 1]
+   [WhiteQueen -> 1];
+   [WhiteKing -> 1]
  }
 LOC 1 {
  PLAYER 2
@@ -289,10 +330,12 @@
     [BlackPawnLeftDbl -> 0];
     [BlackPawnRight -> 0];
     [BlackPawnRightDbl -> 0];
+    [BlackPawnPromote -> 0];
     [BlackKnight -> 0];
     [BlackBishop -> 0];
     [BlackRook -> 0];
-    [BlackQueen -> 0]
+    [BlackQueen -> 0];
+    [BlackKing -> 0]
  }
 MODEL [ |  | 
  ] "


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