Project

General

Profile

Download (422 Bytes) Statistics
| Branch: | Tag: | Revision:
1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2
-- invalid property is that it should never reach 5 or 7
3

    
4
node top (x:bool) returns (OK:bool);
5
--@ contract guarantees OK;
6
var a,b,c:bool;
7
let
8
  a = false -> not pre(a);
9
  b = false -> (not pre(c) and not pre(b) and pre(a)) or 
10
           (pre(b) and not pre(a));
11
  c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a));
12
  OK= (c and a);
13
  --%PROPERTY OK;
14
tel
(3-3/554)