1 theory Cockpit |
|
2 imports MuIOAOracle |
|
3 begin |
|
4 |
|
5 datatype 'a action = Alarm 'a | Info 'a | Ack 'a |
|
6 datatype event = NONE | PonR | Eng | Fue |
|
7 |
|
8 |
|
9 text {* |
|
10 This cockpit automaton is a deeply simplified version of the |
|
11 control component of a helicopter alarm system considered in a study |
|
12 of ESG. Some properties will be proved by using model checker |
|
13 mucke. *} |
|
14 |
|
15 automaton cockpit = |
|
16 signature |
|
17 actions "event action" |
|
18 inputs "Alarm a" |
|
19 outputs "Ack a", "Info a" |
|
20 states |
|
21 APonR_incl :: bool |
|
22 info :: event |
|
23 initially "info = NONE & ~APonR_incl" |
|
24 transitions |
|
25 "Alarm a" |
|
26 post info := "if (a=NONE) then info else a", |
|
27 APonR_incl := "if (a=PonR) then True else APonR_incl" |
|
28 "Info a" |
|
29 pre "(a=info)" |
|
30 "Ack a" |
|
31 pre "(a=PonR --> APonR_incl) & (a=NONE --> ~APonR_incl)" |
|
32 post info := "NONE", |
|
33 APonR_incl := "if (a=PonR) then False else APonR_incl" |
|
34 |
|
35 automaton cockpit_hide = hide_action "Info a" in cockpit |
|
36 |
|
37 text {* |
|
38 Subsequent automata express the properties to be proved, see also |
|
39 Cockpit.ML *} |
|
40 |
|
41 automaton Al_before_Ack = |
|
42 signature |
|
43 actions "event action" |
|
44 inputs "Alarm a" |
|
45 outputs "Ack a" |
|
46 states |
|
47 APonR_incl :: bool |
|
48 initially "~APonR_incl" |
|
49 transitions |
|
50 "Alarm a" |
|
51 post APonR_incl:="if (a=PonR) then True else APonR_incl" |
|
52 "Ack a" |
|
53 pre "(a=PonR --> APonR_incl)" |
|
54 post APonR_incl:="if (a=PonR) then False else APonR_incl" |
|
55 |
|
56 automaton Info_while_Al = |
|
57 signature |
|
58 actions "event action" |
|
59 inputs "Alarm a" |
|
60 outputs "Ack a", "Info i" |
|
61 states |
|
62 info_at_Pon :: bool |
|
63 initially "~info_at_Pon" |
|
64 transitions |
|
65 "Alarm a" |
|
66 post |
|
67 info_at_Pon:="if (a=PonR) then True else (if (a=NONE) then info_at_Pon else False)" |
|
68 "Info a" |
|
69 pre "(a=PonR) --> info_at_Pon" |
|
70 "Ack a" |
|
71 post info_at_Pon:="False" |
|
72 |
|
73 automaton Info_before_Al = |
|
74 signature |
|
75 actions "event action" |
|
76 inputs "Alarm a" |
|
77 outputs "Ack a", "Info i" |
|
78 states |
|
79 info_at_NONE :: bool |
|
80 initially "info_at_NONE" |
|
81 transitions |
|
82 "Alarm a" |
|
83 post info_at_NONE:="if (a=NONE) then info_at_NONE else False" |
|
84 "Info a" |
|
85 pre "(a=NONE) --> info_at_NONE" |
|
86 "Ack a" |
|
87 post info_at_NONE:="True" |
|
88 |
|
89 lemmas aut_simps = |
|
90 cockpit_def cockpit_asig_def cockpit_trans_def |
|
91 cockpit_initial_def cockpit_hide_def |
|
92 Al_before_Ack_def Al_before_Ack_asig_def |
|
93 Al_before_Ack_initial_def Al_before_Ack_trans_def |
|
94 Info_while_Al_def Info_while_Al_asig_def |
|
95 Info_while_Al_initial_def Info_while_Al_trans_def |
|
96 Info_before_Al_def Info_before_Al_asig_def |
|
97 Info_before_Al_initial_def Info_before_Al_trans_def |
|
98 |
|
99 |
|
100 (* to prove, that info is always set at the recent alarm *) |
|
101 lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al" |
|
102 apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) |
|
103 done |
|
104 |
|
105 (* to prove that before any alarm arrives (and after each acknowledgment), |
|
106 info remains at None *) |
|
107 lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al" |
|
108 apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) |
|
109 done |
|
110 |
|
111 (* to prove that before any alarm would be acknowledged, it must be arrived *) |
|
112 lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack" |
|
113 apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) |
|
114 apply auto |
|
115 done |
|
116 |
|
117 end |
|