Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.27 KB)

1
contract FSM_SensorSpec(MODE:bool; limits:bool; prevSensState:real; request:bool; ) returns (sensState: real; );
2

    
3
--Block Path: fsm_12B/FiniteStateMachine/Sen
4

    
5
let
6
var FTP:bool = true -> false;
7

    
8

    
9
--guarantee "FSM011" S( (((prevSensState = 0.0 and not request) => (sensState = 1.0)) and FTP), ((prevSensState = 0.0 and not request) => (sensState = 1.0)) );
10
-- This requirement is not correct as they did not mention "when limits are not exceeded" which is implicitly implicated from  "FSM010" requirement. 
11
-- To rewrtie it: "11.	The sensor shall change states from NOMINAL to TRANSITION when the autopilot is not requesting support and limits are not exceeded."
12
guarantee "FSM011V2" (prevSensState = 0.0 and not request and not limits) => (sensState = 1.0);
13

    
14

    
15
--valid
16
guarantee "FSM012" S( (((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) and FTP), ((prevSensState = 2.0 and not request and not limits) => (sensState = 1.0)) );
17

    
18

    
19
--valid
20
guarantee "FSM010" S( (((prevSensState = 0.0 and limits) => (sensState = 2.0)) and FTP), ((prevSensState = 0.0 and limits) => (sensState = 2.0)) );
21

    
22

    
23
--valid
24
guarantee "FSM013" S( (((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) and FTP), ((prevSensState = 1.0 and request and MODE) => (sensState = 0.0)) );
25

    
26

    
27
tel
28