Project

General

Profile

Download (469 Bytes) Statistics
| Branch: | Tag: | Revision:
1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2
-- property is that it should never reach 6 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 = true -> pre(true -> pre b) = not b;
13
--  --%PROPERTY not (c and b);
14
--%PROPERTY OK;
15
tel
(1-1/554)