author | wenzelm |
Mon, 02 Oct 2000 14:58:39 +0200 | |
changeset 10127 | 86269867de34 |
parent 8733 | 3213613a775a |
child 17244 | 0b2ff9541727 |
permissions | -rw-r--r-- |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
1 |
|
7299 | 2 |
Cockpit = MuIOAOracle + |
3 |
||
4 |
datatype 'a action = Alarm 'a | Info 'a | Ack 'a |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
5 |
datatype event = NONE | PonR | Eng | Fue |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
6 |
|
7299 | 7 |
|
8 |
(*This cockpit automaton is a deeply simplified version of the |
|
9 |
control component of a helicopter alarm system considered in a study |
|
10 |
of ESG. Some properties will be proved by using model checker |
|
11 |
mucke.*) |
|
12 |
||
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
13 |
automaton cockpit = |
7299 | 14 |
signature |
15 |
actions event action |
|
16 |
inputs "Alarm a" |
|
17 |
outputs "Ack a","Info a" |
|
18 |
states |
|
19 |
APonR_incl :: bool |
|
20 |
info :: event |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
21 |
initially "info=NONE & ~APonR_incl" |
7299 | 22 |
transitions |
23 |
"Alarm a" |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
24 |
post info:="if (a=NONE) then info else a", |
7299 | 25 |
APonR_incl:="if (a=PonR) then True else APonR_incl" |
26 |
"Info a" |
|
27 |
pre "(a=info)" |
|
28 |
"Ack a" |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
29 |
pre "(a=PonR --> APonR_incl) & (a=NONE --> ~APonR_incl)" |
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
30 |
post info:="NONE",APonR_incl:="if (a=PonR) then False else APonR_incl" |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
31 |
|
8733 | 32 |
automaton cockpit_hide = hide_action "Info a" in cockpit |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
33 |
|
7299 | 34 |
|
35 |
(*Subsequent automata express the properties to be proved, see also |
|
36 |
Cockpit.ML*) |
|
37 |
||
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
38 |
automaton Al_before_Ack = |
7299 | 39 |
signature |
40 |
actions event action |
|
41 |
inputs "Alarm a" |
|
42 |
outputs "Ack a" |
|
43 |
states |
|
44 |
APonR_incl :: bool |
|
45 |
initially "~APonR_incl" |
|
46 |
transitions |
|
47 |
"Alarm a" |
|
48 |
post APonR_incl:="if (a=PonR) then True else APonR_incl" |
|
49 |
"Ack a" |
|
50 |
pre "(a=PonR --> APonR_incl)" |
|
51 |
post APonR_incl:="if (a=PonR) then False else APonR_incl" |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
52 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
53 |
automaton Info_while_Al = |
7299 | 54 |
signature |
55 |
actions event action |
|
56 |
inputs "Alarm a" |
|
57 |
outputs "Ack a", "Info i" |
|
58 |
states |
|
59 |
info_at_Pon :: bool |
|
60 |
initially "~info_at_Pon" |
|
61 |
transitions |
|
62 |
"Alarm a" |
|
63 |
post |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
64 |
info_at_Pon:="if (a=PonR) then True else (if (a=NONE) then info_at_Pon else False)" |
7299 | 65 |
"Info a" |
66 |
pre "(a=PonR) --> info_at_Pon" |
|
67 |
"Ack a" |
|
68 |
post info_at_Pon:="False" |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
69 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
70 |
automaton Info_before_Al = |
7299 | 71 |
signature |
72 |
actions event action |
|
73 |
inputs "Alarm a" |
|
74 |
outputs "Ack a", "Info i" |
|
75 |
states |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
76 |
info_at_NONE :: bool |
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
77 |
initially "info_at_NONE" |
7299 | 78 |
transitions |
79 |
"Alarm a" |
|
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
80 |
post info_at_NONE:="if (a=NONE) then info_at_NONE else False" |
7299 | 81 |
"Info a" |
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
82 |
pre "(a=NONE) --> info_at_NONE" |
7299 | 83 |
"Ack a" |
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
8733
diff
changeset
|
84 |
post info_at_NONE:="True" |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
85 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
86 |
end |