equal
deleted
inserted
replaced
1 |
1 |
2 Cockpit = MuIOAOracle + |
2 Cockpit = MuIOAOracle + |
3 |
3 |
4 datatype 'a action = Alarm 'a | Info 'a | Ack 'a |
4 datatype 'a action = Alarm 'a | Info 'a | Ack 'a |
5 datatype event = None | PonR | Eng | Fue |
5 datatype event = NONE | PonR | Eng | Fue |
6 |
6 |
7 |
7 |
8 (*This cockpit automaton is a deeply simplified version of the |
8 (*This cockpit automaton is a deeply simplified version of the |
9 control component of a helicopter alarm system considered in a study |
9 control component of a helicopter alarm system considered in a study |
10 of ESG. Some properties will be proved by using model checker |
10 of ESG. Some properties will be proved by using model checker |
16 inputs "Alarm a" |
16 inputs "Alarm a" |
17 outputs "Ack a","Info a" |
17 outputs "Ack a","Info a" |
18 states |
18 states |
19 APonR_incl :: bool |
19 APonR_incl :: bool |
20 info :: event |
20 info :: event |
21 initially "info=None & ~APonR_incl" |
21 initially "info=NONE & ~APonR_incl" |
22 transitions |
22 transitions |
23 "Alarm a" |
23 "Alarm a" |
24 post info:="if (a=None) then info else a", |
24 post info:="if (a=NONE) then info else a", |
25 APonR_incl:="if (a=PonR) then True else APonR_incl" |
25 APonR_incl:="if (a=PonR) then True else APonR_incl" |
26 "Info a" |
26 "Info a" |
27 pre "(a=info)" |
27 pre "(a=info)" |
28 "Ack a" |
28 "Ack a" |
29 pre "(a=PonR --> APonR_incl) & (a=None --> ~APonR_incl)" |
29 pre "(a=PonR --> APonR_incl) & (a=NONE --> ~APonR_incl)" |
30 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" |
31 |
31 |
32 automaton cockpit_hide = hide_action "Info a" in cockpit |
32 automaton cockpit_hide = hide_action "Info a" in cockpit |
33 |
33 |
34 |
34 |
35 (*Subsequent automata express the properties to be proved, see also |
35 (*Subsequent automata express the properties to be proved, see also |
59 info_at_Pon :: bool |
59 info_at_Pon :: bool |
60 initially "~info_at_Pon" |
60 initially "~info_at_Pon" |
61 transitions |
61 transitions |
62 "Alarm a" |
62 "Alarm a" |
63 post |
63 post |
64 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)" |
65 "Info a" |
65 "Info a" |
66 pre "(a=PonR) --> info_at_Pon" |
66 pre "(a=PonR) --> info_at_Pon" |
67 "Ack a" |
67 "Ack a" |
68 post info_at_Pon:="False" |
68 post info_at_Pon:="False" |
69 |
69 |
71 signature |
71 signature |
72 actions event action |
72 actions event action |
73 inputs "Alarm a" |
73 inputs "Alarm a" |
74 outputs "Ack a", "Info i" |
74 outputs "Ack a", "Info i" |
75 states |
75 states |
76 info_at_None :: bool |
76 info_at_NONE :: bool |
77 initially "info_at_None" |
77 initially "info_at_NONE" |
78 transitions |
78 transitions |
79 "Alarm a" |
79 "Alarm a" |
80 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" |
81 "Info a" |
81 "Info a" |
82 pre "(a=None) --> info_at_None" |
82 pre "(a=NONE) --> info_at_NONE" |
83 "Ack a" |
83 "Ack a" |
84 post info_at_None:="True" |
84 post info_at_NONE:="True" |
85 |
85 |
86 end |
86 end |