tests/source/two_counters.scade


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

const n1: int = 100;
const n2: int = 60;


node top(a,b,c : bool) returns (ok, r1, r2 : bool)
var
  x, y, pre_x, pre_y: int;
  o1, o2: 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;
  ok= if o1 then o2 else true;
  r1 = 0<=x and x<=n1;
  r2 = 0<=y and y<=n2;
  pre_x = 0 -> pre(x);
  pre_y = 0 -> pre(y);

  m = true -> pre o2;
  n = true -> pre o1;
  lb = true -> pre b;

  guarantee g1: ok;
  guarantee g2: r1;
  guarantee g3: r2;
tel