Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / switch.lus @ 65f71d05

History | View | Annotate | Download (710 Bytes)

1
node SWITCH1 (set,reset,initial:bool) returns (level:bool);
2
let
3
  level = initial -> if set then true 
4
                     else if reset then false 
5
                     else pre(level);
6
tel
7

    
8
node SWITCH (set,reset,initial:bool) returns (level:bool);
9
let
10
  level = initial -> if set and not pre(level) then true
11
                     else if reset then false
12
                     else pre(level);
13
tel
14

    
15
--@ ensures OK;
16
node top(set, treset, initial:bool) returns (OK:bool);
17
var level,level1:bool;
18
let
19
  level = SWITCH(set,treset,initial);
20
  level1 = SWITCH1(set,treset,initial);
21
  OK = if (not(set and treset)) then
22
    (level = level1)
23
    else true;
24
  --assert not(set and treset);
25
  --%PROPERTY OK=true;
26
tel