Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / regression_tests / stateful_assert.lus @ d50b0dc0

History | View | Annotate | Download (334 Bytes)

1 e2068500 Temesghen Kahsai
2 e41592cf Temesghen Kahsai
node top
3 e2068500 Temesghen Kahsai
  (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;