Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / regression_tests / stateful_assert.lus @ e41592cf

History | View | Annotate | Download (334 Bytes)

1

    
2
node top
3
  (TS, OSPF : bool;
4
   Primary_Side : bool)
5

    
6
returns 
7
  (PFS : bool);
8

    
9
var
10
  PFSL_PFS : bool;
11
  riseTS_O : bool;
12
  riseOSPF_O : bool;
13
  
14
let
15
assert Primary_Side = (Primary_Side -> pre(Primary_Side));
16
  PFSL_PFS = riseTS_O or  riseOSPF_O or Primary_Side;
17
  
18
  riseTS_O = true;
19

    
20
  riseOSPF_O = false;
21

    
22
  PFS = PFSL_PFS;
23

    
24
tel;