Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / FSMSpec.lus @ f470cec6

History | View | Annotate | Download (1.55 KB)

1
--Historically
2
node H(X:bool) returns (Y:bool);
3
let
4
    Y = X -> (X and (pre Y));
5
tel
6

    
7
--Y since inclusive X
8
node SI(X,Y: bool) returns (Z:bool);
9
let
10
Z = Y and (X or (false -> pre Z));
11
tel
12

    
13
--Y since X
14
node S(X,Y: bool) returns (Z:bool);
15
let
16
Z = X or (Y and (false -> pre Z));
17
tel
18

    
19
--Once
20
node O(X:bool) returns (Y:bool);
21
let
22
 Y = X or (false -> pre Y);
23
tel
24

    
25
node First( X : bool ) returns ( Y : bool );
26
let
27
  Y = X -> pre Y;
28
tel
29

    
30
--Timed Once: less than or equal to N
31
node OTlore(const N: int; X: bool; ) returns (Y: bool);
32
    var C:int;
33
let
34
    C = if X then 0
35
        else (-1 -> pre C + (if pre C <0 then 0 else 1));
36

    
37
    Y = First(X)
38
        ->
39
        (if pre C < 0  then false
40
         else C <= N
41
        );
42
tel
43

    
44
-- Timed Historically: less than or equal to N
45
node HTlore(const N: int; X: bool) returns (Y: bool);
46
let
47
  Y = not OTlore(N, not X);
48
tel
49

    
50
-- Timed Since: less than or equal to N
51
node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
52
let
53
  Z = S(X, Y) and OTlore(N, X);
54
tel
55

    
56
-- Timed Since Inclusive: less than or equal to N
57
node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
58
let
59
  Z = SI(X,Y) and OTlore(N, X);
60
tel
61

    
62
contract FSMSpec(apfail:bool; limits:bool; standby:bool; supported:bool; ) returns (pullup: bool; );
63

    
64
--Block Path: fsm_12B
65

    
66
let
67

    
68
var FTP:bool = true -> false;
69

    
70
--guarantee "FSM001" S( (((limits and not standby and not apfail and supported) => (pullup)) and FTP), ((limits and not standby and not apfail and supported) => (pullup)) );
71
guarantee "FSM001V2" limits and not standby and not apfail and supported => pullup;
72

    
73
tel
74