Project

General

Profile

Bug #73 ยป TriplexSignalMonitorSpec.lus

Hamza Bourbouh, 03/28/2019 08:19 PM

 
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 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
node abs(x:real)
63
returns(y:real);
64
let
65
	y = if x >= 0.0 then x else - x;
66
tel
67

    
68
(*@contract TriplexSignalMonitorSpec(Tlevel:real; ia:real; ib:real; ic:real; PCLimit: int; ) returns (FC: int; set_val: real; TC: int; PC: int);
69

    
70
--Block Path: triplex_12B
71

    
72
let
73

    
74
  var FTP:bool = true -> false;
75
  var C1:bool = abs(ia - ib) > Tlevel;
76
  var C2:bool = abs(ib - ic) > Tlevel;
77
  var C3:bool = abs(ia - ic) > Tlevel;
78
  var miscompare : bool = (not C1 and C2 and C3)  or (C1 and not C2 and C3) or (C1 and C2 and not C3);
79

    
80
  var prePC: int = 0 -> pre PC;
81
  var pre_set_val : real = (0.0 -> pre set_val);
82
  var  failure_in_progress : bool = miscompare  and prePC <= PCLimit and PC > 0;
83
  var  failure_must_be_latched : bool = miscompare  and prePC  > PCLimit;
84
  var  no_fail : bool = (FC =0);
85
  var  pre_no_fail : bool = (true  -> pre  no_fail);
86

    
87
  var  single_fail_reported : bool = (FC=1) or (FC=2) or (FC=4);
88
  var mid_value : real =  if ((ia <= ib and ib <= ic) 
89
                              or (ic <= ib and ib <= ia))
90
                              then ib 
91
                          else if ((ib <= ia and ia <= ic) 
92
                              or (ic <= ia and ia <= ib))
93
                              then ia
94
                          else ic;
95
  -- Assumptions
96
  assume PCLimit > 0 ;
97

    
98
  -- In the no-fail state, a miscompare, which shall be characterized by one branch
99
  -- differing  with  the  other  two  branches  by  a  unique  trip  level  that  lasts  for
100
  -- more than the persistence limit, shall be reported to failure management as
101
  -- a failure.
102
  guarantee "TSM -001" S((( pre_no_fail  and failure_must_be_latched)   => single_fail_reported) and FTP , (( pre_no_fail  and  failure_must_be_latched) => single_fail_reported));
103

    
104
  -- In the no-fail state, the mid-value shall be the selected value. Note: a first failure in progress will not affect the method for determining the selected value.
105
  guarantee "TSM -002" S((( no_fail => set_val = mid_value) and  FTP),(no_fail => set_val = mid_value));
106

    
107
  -- In the single fail state, a good channel average of the remaining two good branches shall be used to determine the selected value.
108
  guarantee "TSM-003a"  S( ((FC = 1 => set_val = 0.5 * ( ia + ib )) and FTP),  (FC = 1 => set_val = 0.5 * ( ia + ib ))); 
109
  guarantee "TSM-003b"  S(((FC = 2 => set_val = 0.5 * ( ia + ic )) and FTP),  (FC = 2 => set_val = 0.5 * ( ia + ic ))); 
110
  guarantee "TSM-003c"  S(((FC = 4 => set_val = 0.5 * ( ib + ic )) and FTP), (FC = 4 => set_val = 0.5 * ( ib + ic ))); 
111

    
112
  -- If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.
113
  guarantee "TSM-004"  S( ((single_fail_reported and failure_in_progress => set_val = pre_set_val) and FTP),  (single_fail_reported and failure_in_progress => set_val = pre_set_val)); 
114
tel
115
*)
    (1-1/1)