Project

General

Profile

Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/misc/_6counter.lus

View differences:

regression_tests/lustre_files/success/kind_fmcad08/misc/_6counter.lus
1 1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2 2
-- property is that it should never reach 6 or 7
3 3

  
4
--@ ensures OK;
5 4
node top (x:bool) returns (OK:bool);
5
--@ contract guarantees OK;
6 6
var a,b,c:bool;
7 7
let
8 8
  a = false -> not pre(a);

Also available in: Unified diff