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