Project

General

Profile

Download (898 Bytes) Statistics
| Branch: | Tag: | Revision:
1 0cbf0839 ploc
2
3
--A messed up counter:
4
--x = 0: 0,1,2,3,4,3,4,...
5
--x = 1: 0,1,2,3,4,5,2,3,4,5,...
6
--A is MSB, C is LSB
7
--property: never reach state 6 or 7
8
9
node loop6counter (x:bool) returns (out:bool);
10
var a,b,c:bool;
11
let
12
  a = false -> (pre(b) and pre(c)) or
13
               (pre(x) and pre(a) and not pre(c));
14
  b = false -> (not pre(b) and pre(c)) or
15
               (pre(b) and not pre(c)) or
16
               (not pre(x) and pre(a));
17
  c = false -> not pre(c);
18
  out = a and c;
19
tel
20
21
node intloop6counter (x:bool) returns (out:bool);
22
var time: int;
23
let
24
  time = 0 -> if pre(time) = 5 then 2
25
            else if pre(time) = 4 then
26
              if not pre(x) then 3 
27
              else 5
28
            else pre time + 1;
29
  out = (time = 5);
30
tel
31
32
33 3e36d4e0 ploc
--@ ensures OK;
34 0cbf0839 ploc
node top (x:bool) returns (OK:bool);
35
var b,d:bool;
36
let
37
  b = loop6counter(x);
38
  d = intloop6counter(x);
39
  OK = not x or b = d;
40
  --%PROPERTY OK;
41
tel