Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (712 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
--requires assert to be true
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(level = level1) else true;
22
--  assert not(set and treset);
23
  --%PROPERTY OK=true;
24
tel