Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / switch.lus @ 22fe1c93

History | View | Annotate | Download (694 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
node top(set, treset, initial:bool) returns (OK:bool);
16
var level,level1:bool;
17
let
18
  level = SWITCH(set,treset,initial);
19
  level1 = SWITCH1(set,treset,initial);
20
  OK = if (not(set and treset)) then
21
    (level = level1)
22
    else true;
23
  --assert not(set and treset);
24
  --%PROPERTY OK=true;
25
tel