Project

General

Profile

Revision 6ccfcb12

View differences:

tests/cocospec/TriplexSignalMonitorSpec.lus
116 116
assume true -> Tlevel = pre Tlevel;
117 117

  
118 118
-- when preFC = 0 & prePC > prePCLimit TriplexSignalMonitor shall immediately satisfy FC > 0
119
--guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) );
120
--guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0;
119
guarantee "RM001" S( (((preFC = 0 and prePC > prePCLimit) => (FC > 0)) and FTP), ((preFC = 0 and prePC > prePCLimit) => (FC > 0)) );
120
guarantee "RM001V2" is_a_miscompare and prePC > PCLimit => FC > 0;
121 121

  
122 122
-- when FC =1 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ib)
123
--guarantee "RM003a" (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )) or (S( ((set_val = 0.5 * ( ia + ib )) and ((FC = 1) and (FTP or (pre (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )))))), (set_val = 0.5 * ( ia + ib )) ));
124
--guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib);
123
guarantee "RM003a" (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )) or (S( ((set_val = 0.5 * ( ia + ib )) and ((FC = 1) and (FTP or (pre (S( (( not (FC = 1)) and FTP), ( not (FC = 1)) )))))), (set_val = 0.5 * ( ia + ib )) ));
124
guarantee "RM003aV2" FC = 1 => set_val = 0.5 * (ia +ib);
125 125

  
126 126
-- when FC =2 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ia +ic).
127
--guarantee "RM003b"  (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )) or (S( ((set_val = 0.5 * ( ia + ic )) and ((FC = 2) and (FTP or (pre (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )))))), (set_val = 0.5 * ( ia + ic )) ));
128
--guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic);
127
guarantee "RM003b"  (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )) or (S( ((set_val = 0.5 * ( ia + ic )) and ((FC = 2) and (FTP or (pre (S( (( not (FC = 2)) and FTP), ( not (FC = 2)) )))))), (set_val = 0.5 * ( ia + ic )) ));
128
guarantee "RM003bV2" FC = 2 => set_val = 0.5 * (ia +ic);
129 129

  
130 130

  
131 131
-- when FC =4 TriplexSignalMonitor shall always satisfy set_val = 0.5 * (ib +ic)
132
--guarantee "RM003c" (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )) or (S( ((set_val = 0.5 * ( ib + ic )) and ((FC = 4) and (FTP or (pre (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )))))), (set_val = 0.5 * ( ib + ic )) ));
133
--guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic);
132
guarantee "RM003c" (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )) or (S( ((set_val = 0.5 * ( ib + ic )) and ((FC = 4) and (FTP or (pre (S( (( not (FC = 4)) and FTP), ( not (FC = 4)) )))))), (set_val = 0.5 * ( ib + ic )) ));
133
guarantee "RM003cV2" FC = 4 => set_val = 0.5 * (ib +ic);
134 134

  
135 135
-- when preFC =0 TriplexSignalMonitor shall immediately satisfy set_val = mid_value
136
--guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) );
137
--guarantee "RM002V2" FC = 0 => set_val = mid_value;
136
guarantee "RM002" S( (((preFC = 0) => (set_val = mid_value)) and FTP), ((preFC = 0) => (set_val = mid_value)) );
137
guarantee "RM002V2" FC = 0 => set_val = mid_value;
138 138

  
139 139
-- when (absAB > Tlevel & absAC >Tlevel) | (absAB > Tlevel & absBC > Tlevel) | (absAC > Tlevel & absBC > Tlevel) TriplexSignalMonitor shall always satisfy set_val = prevSet_val
140
--guarantee "RM004" (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )) or (S( ((set_val = prevSet_val) and ((( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel )) and (FTP or (pre (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )))))), (set_val = prevSet_val) ));
140
guarantee "RM004" (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )) or (S( ((set_val = prevSet_val) and ((( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel )) and (FTP or (pre (S( (( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) and FTP), ( not (( absAB > Tlevel and absAC > Tlevel ) or ( absAB > Tlevel and absBC > Tlevel ) or ( absAC > Tlevel and absBC > Tlevel ))) )))))), (set_val = prevSet_val) ));
141 141

  
142 142
--Explanaton from document: 
143 143
--    -A miscompare that persists but has not yet been declared failed is known as a failure in progress.
......
146 146
--[RM-004] If a second failure is in progress, the selected value shall remain unchanged from the previous selected value.
147 147
guarantee "RM004V2"  Count(FC > 0) = 1   and is_a_miscompare and prePC > 0 and prePC < PCLimit => set_val = prevSet_val;
148 148

  
149
--guarantee true ->   Count(FC > 0) = 1  and ia <> pre ia and ib <> pre ib  and ic <> pre ic  and prePC > 0  and prePC < PCLimit => set_val   <> prevSet_val;
149
guarantee true ->   Count(FC > 0) = 1  and ia <> pre ia and ib <> pre ib  and ic <> pre ic  and prePC > 0  and prePC < PCLimit => set_val   <> prevSet_val;
150 150
tel
151 151
*)
tests/cocospec/integrator_12BWithoutModesAndInitialization.lus
77 77
guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));
78 78

  
79 79
guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;
80
--guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
80
guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
81 81

  
82 82

  
83 83
tel
tests/cocospec/regulator_12B_Spec.lus
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

  
63

  
64
contract RegulatorSpec()
65
returns (lcvdt_cmd_fcs_dps2 : real;
66
	mcvdt_cmd_fcs_dps2 : real;
67
	ncvdt_cmd_fcs_dps2 : real;
68
	xcvdt_cmd_fcs_fps2: real;
69
	hcvdt_cmd_fcs_fps2: real;);
70

  
71
-- Block path: regs_12B_PP (why do we have _PP?)
72

  
73
let
74

  
75
var FTP:bool = true -> false;
76

  
77
var airspeed_command_acceleration: real = (xcvdt_cmd_fcs_fps2 - (0.0 -> pre xcvdt_cmd_fcs_fps2)) /0.01;
78
var count_airspeed_output_exceeding_32: int = 0 -> if (xcvdt_cmd_fcs_fps2 > 32.0) then pre count_airspeed_output_exceeding_32 + 1 else 0;
79
var count_height_output_exceeding_32: int = 0 -> if (hcvdt_cmd_fcs_fps2 > 32.0) then pre count_height_output_exceeding_32 + 1 else 0;
80
var count_pitch_output_exceeding_50: int = 0 -> if (mcvdt_cmd_fcs_dps2 > 50.0) then pre count_pitch_output_exceeding_50 + 1 else 0;
81
var count_roll_output_exceeding_50: int = 0 -> if (lcvdt_cmd_fcs_dps2 > 50.0) then pre count_roll_output_exceeding_50 + 1 else 0;
82
var count_yaw_output_exceeding_50: int = 0 -> if (ncvdt_cmd_fcs_dps2 > 50.0) then pre count_yaw_output_exceeding_50 + 1 else 0;
83
var height_command_acceleration: real = 0.0 ->  (hcvdt_cmd_fcs_fps2 - pre hcvdt_cmd_fcs_fps2) /0.01;
84
var pitch_command_acceleration: real = 0.0 ->  (mcvdt_cmd_fcs_dps2 - pre mcvdt_cmd_fcs_dps2) /0.01;
85
var roll_command_acceleration: real = 0.0 ->  (lcvdt_cmd_fcs_dps2 - pre lcvdt_cmd_fcs_dps2) /0.01;
86
var yaw_command_acceleration: real = 0.0 ->  (ncvdt_cmd_fcs_dps2 - pre ncvdt_cmd_fcs_dps2) /0.01;
87

  
88
-- Regulator shall always satisfy count_airspeed_output_exceeding_32 <= 100
89
    guarantee "REG004" S( ((count_airspeed_output_exceeding_32 <= 100) and FTP), (count_airspeed_output_exceeding_32 <= 100) );
90

  
91
-- Regulator shall always satisfy count_roll_output_exceeding_50 <= 100
92
    guarantee "REG001" S( ((count_roll_output_exceeding_50 <= 100) and FTP), (count_roll_output_exceeding_50 <= 100) );
93
    guarantee count_roll_output_exceeding_50 <= 100;
94

  
95
-- Regulator shall always satisfy roll_command_acceleration <= 50.0
96
	guarantee "REG006" S( ((roll_command_acceleration <= 50.0) and FTP), (roll_command_acceleration <= 50.0) );
97

  
98
-- Regulator shall always satisfy count_height_output_exceeding_32 <= 100
99
	guarantee "REG005" S( ((count_height_output_exceeding_32 <= 100) and FTP), (count_height_output_exceeding_32 <= 100) );
100

  
101
-- Regulator shall always satisfy pitch_command_acceleration <= 50.0
102
	guarantee "REG007" S( ((pitch_command_acceleration <= 50.0) and FTP), (pitch_command_acceleration <= 50.0) );
103

  
104
-- Regulator shall always satisfy yaw_command_acceleration <= 50.0
105
	guarantee "REG008" S( ((yaw_command_acceleration <= 50.0) and FTP), (yaw_command_acceleration <= 50.0) );
106

  
107
-- Regulator shall always satisfy airspeed_command_acceleration <=32.0
108
	guarantee "REG009" S( ((airspeed_command_acceleration <= 32.0) and FTP), (airspeed_command_acceleration <= 32.0) );
109

  
110
-- Regulator shall always satisfy height_command_acceleration <= 32.0
111
	guarantee "REG010" S( ((height_command_acceleration <= 32.0) and FTP), (height_command_acceleration <= 32.0) );
112

  
113
-- Regulator shall always satisfy count_pitch_output_exceeding_50 <= 100
114
	guarantee "REG002" S( ((count_pitch_output_exceeding_50 <= 100) and FTP), (count_pitch_output_exceeding_50 <= 100) );
115

  
116
    -- Regulator shall always satisfy count_yaw_output_exceeding_50 <= 100
117
	guarantee "REG003" S( ((count_yaw_output_exceeding_50 <= 100) and FTP), (count_yaw_output_exceeding_50 <= 100) );
118

  
119
tel

Also available in: Unified diff