1 Cockpit = MuIOAOracle + |
|
2 |
1 |
3 datatype ('a)action = Alarm 'a | Info 'a | Ack 'a |
2 Cockpit = MuIOAOracle + |
|
3 |
|
4 datatype 'a action = Alarm 'a | Info 'a | Ack 'a |
4 datatype event = None | PonR | Eng | Fue |
5 datatype event = None | PonR | Eng | Fue |
5 |
6 |
6 (* this cockpit automaton is a deeply simplified version of |
7 |
7 the control component of a helicopter alarm system |
8 (*This cockpit automaton is a deeply simplified version of the |
8 considered in a study of ESG. |
9 control component of a helicopter alarm system considered in a study |
9 Some properties will be proved by using model checker mucke *) |
10 of ESG. Some properties will be proved by using model checker |
|
11 mucke.*) |
|
12 |
10 automaton cockpit = |
13 automaton cockpit = |
11 signature |
14 signature |
12 actions (event)action |
15 actions event action |
13 inputs "Alarm a" |
16 inputs "Alarm a" |
14 outputs "Ack a","Info a" |
17 outputs "Ack a","Info a" |
15 states |
18 states |
16 APonR_incl :: bool |
19 APonR_incl :: bool |
17 info :: event |
20 info :: event |
18 initially "info=None & ~APonR_incl" |
21 initially "info=None & ~APonR_incl" |
19 transitions |
22 transitions |
20 "Alarm a" |
23 "Alarm a" |
21 post info:="if (a=None) then info else a", |
24 post info:="if (a=None) then info else a", |
22 APonR_incl:="if (a=PonR) then True else APonR_incl" |
25 APonR_incl:="if (a=PonR) then True else APonR_incl" |
23 "Info a" |
26 "Info a" |
24 pre "(a=info)" |
27 pre "(a=info)" |
25 "Ack a" |
28 "Ack a" |
26 pre "(a=PonR --> APonR_incl) & (a=None --> ~APonR_incl)" |
29 pre "(a=PonR --> APonR_incl) & (a=None --> ~APonR_incl)" |
27 post info:="None",APonR_incl:="if (a=PonR) then False else APonR_incl" |
30 post info:="None",APonR_incl:="if (a=PonR) then False else APonR_incl" |
28 |
31 |
29 automaton cockpit_hide = hide "Info a" in cockpit |
32 automaton cockpit_hide = hide "Info a" in cockpit |
30 |
33 |
31 (* following automatons express the properties to be proved, see Cockpit.ML *) |
34 |
|
35 (*Subsequent automata express the properties to be proved, see also |
|
36 Cockpit.ML*) |
|
37 |
32 automaton Al_before_Ack = |
38 automaton Al_before_Ack = |
33 signature |
39 signature |
34 actions (event)action |
40 actions event action |
35 inputs "Alarm a" |
41 inputs "Alarm a" |
36 outputs "Ack a" |
42 outputs "Ack a" |
37 states |
43 states |
38 APonR_incl :: bool |
44 APonR_incl :: bool |
39 initially "~APonR_incl" |
45 initially "~APonR_incl" |
40 transitions |
46 transitions |
41 "Alarm a" |
47 "Alarm a" |
42 post APonR_incl:="if (a=PonR) then True else APonR_incl" |
48 post APonR_incl:="if (a=PonR) then True else APonR_incl" |
43 "Ack a" |
49 "Ack a" |
44 pre "(a=PonR --> APonR_incl)" |
50 pre "(a=PonR --> APonR_incl)" |
45 post APonR_incl:="if (a=PonR) then False else APonR_incl" |
51 post APonR_incl:="if (a=PonR) then False else APonR_incl" |
46 |
52 |
47 automaton Info_while_Al = |
53 automaton Info_while_Al = |
48 signature |
54 signature |
49 actions (event)action |
55 actions event action |
50 inputs "Alarm a" |
56 inputs "Alarm a" |
51 outputs "Ack a","Info i" |
57 outputs "Ack a", "Info i" |
52 states |
58 states |
53 info_at_Pon :: bool |
59 info_at_Pon :: bool |
54 initially "~info_at_Pon" |
60 initially "~info_at_Pon" |
55 transitions |
61 transitions |
56 "Alarm a" |
62 "Alarm a" |
57 post |
63 post |
58 info_at_Pon:="if (a=PonR) then True else (if (a=None) then info_at_Pon else False)" |
64 info_at_Pon:="if (a=PonR) then True else (if (a=None) then info_at_Pon else False)" |
59 "Info a" |
65 "Info a" |
60 pre "(a=PonR) --> info_at_Pon" |
66 pre "(a=PonR) --> info_at_Pon" |
61 "Ack a" |
67 "Ack a" |
62 post info_at_Pon:="False" |
68 post info_at_Pon:="False" |
63 |
69 |
64 automaton Info_before_Al = |
70 automaton Info_before_Al = |
65 signature |
71 signature |
66 actions (event)action |
72 actions event action |
67 inputs "Alarm a" |
73 inputs "Alarm a" |
68 outputs "Ack a","Info i" |
74 outputs "Ack a", "Info i" |
69 states |
75 states |
70 info_at_None :: bool |
76 info_at_None :: bool |
71 initially "info_at_None" |
77 initially "info_at_None" |
72 transitions |
78 transitions |
73 "Alarm a" |
79 "Alarm a" |
74 post info_at_None:="if (a=None) then info_at_None else False" |
80 post info_at_None:="if (a=None) then info_at_None else False" |
75 "Info a" |
81 "Info a" |
76 pre "(a=None) --> info_at_None" |
82 pre "(a=None) --> info_at_None" |
77 "Ack a" |
83 "Ack a" |
78 post info_at_None:="True" |
84 post info_at_None:="True" |
79 |
85 |
80 end |
86 end |