tests/kind2-examples/a_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

node top
  (x: bool)
returns
  (OK: bool)

var
  V13_b: bool;
  V14_d: bool;
  V40_a: bool;
  V41_b: bool;
  V51_time: int;

let

  V51_time = (0 -> (if ((pre V51_time) = 3) then 0 else ((pre V51_time) + 1)));
  V41_b = (false -> (pre V40_a));
  V40_a = (false -> (not (pre V41_b)));
  V14_d = (V51_time = 2);
  V13_b = (V40_a and V41_b);
  OK = (V13_b = V14_d);

  guarantee PROPERTY: OK;

tel