From bc9ad2280839677bb46acfd846ff05bb37719b6e Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 9 Jul 2014 15:32:28 +0200
Subject: Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!

---
 tests/source/two_counters.scade | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'tests')

diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
index 7970aab..6468523 100644
--- a/tests/source/two_counters.scade
+++ b/tests/source/two_counters.scade
@@ -1,5 +1,5 @@
-const n1: int = 10;
-const n2: int = 6;
+const n1: int = 100;
+const n2: int = 60;
 
 
 node top(a,b,c : bool) returns (ok, r1, r2 : bool)
@@ -7,12 +7,12 @@ var
   x, y, pre_x, pre_y: int;
   o1, o2: bool;
 
-  m: bool;
+  m, n, lb: bool;
 let
   x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
   y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
-  o1= x = n1;
-  o2= y = n2;
+  o1= x >= n1;
+  o2= y >= n2;
   ok= if o1 then o2 else true;
   r1 = 0<=x and x<=n1;
   r2 = 0<=y and y<=n2;
@@ -20,6 +20,8 @@ let
   pre_y = 0 -> pre(y);
 
   m = true -> pre o2;
+  n = true -> pre o1;
+  lb = true -> pre b;
 
   guarantee g1: ok;
   guarantee g2: r1;
-- 
cgit v1.2.3