blob: 334bca165a6f12127a2966c371748679fe8e6ee6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
/*
x = 10 | 9 | 8 | 7 | 6 | 5 | ... | 0 | 1 | 2 | ... | 10 | ...
y = 0 | 1 | 2 | 3 | 4 | 5 | ... | 10 | 9 | 8 | ... | 0 | ...
b1 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
b2 = t | f | f | f | f | f | ... | f | f | f | ... | t | ...
eq* = t | t | t | t | t | t | ... | t | t | t | ... | t | ...
*/
-- type t2 = subrange [0,10] of int;
const bound: int = 1000;
node counters(z: bool) returns (eq_nind : bool ; probe x, probe y : int)
var
b1, b2 : bool;
a, b : bool;
let
a = false -> (if pre a then pre x < bound else pre x <= 0);
--a = false -> pre(if a then x < bound else x <= 0);
x = bound -> (if a then pre x + 1 else pre x - 1);
b = true -> (if pre b then pre y < bound else pre y <= 0);
--b = true -> pre(if b then y < bound else y <= 0);
y = 0 -> (if b then pre y + 1 else pre y - 1);
b1 = x=bound;
b2 = y=0;
guarantee xy : x+y = bound;
guarantee bb : b1 = b2;
guarantee rp : -bound <= (x-y) and (x-y) <= bound;
tel
|
