author | wenzelm |
Mon, 02 Oct 2000 14:58:39 +0200 | |
changeset 10127 | 86269867de34 |
parent 7299 | 743b22579a2f |
child 15661 | 9ef583b08647 |
permissions | -rw-r--r-- |
7299 | 1 |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
2 |
val aut_simps = [cockpit_def,cockpit_asig_def,cockpit_trans_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
3 |
cockpit_initial_def,cockpit_hide_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
4 |
Al_before_Ack_def,Al_before_Ack_asig_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
5 |
Al_before_Ack_initial_def,Al_before_Ack_trans_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
6 |
Info_while_Al_def,Info_while_Al_asig_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
7 |
Info_while_Al_initial_def,Info_while_Al_trans_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
8 |
Info_before_Al_def,Info_before_Al_asig_def, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
9 |
Info_before_Al_initial_def,Info_before_Al_trans_def]; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
10 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
11 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
12 |
(* to prove, that info is always set at the recent alarm *) |
7299 | 13 |
Goal "cockpit =<| Info_while_Al"; |
14 |
by (is_sim_tac aut_simps 1); |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
15 |
qed"cockpit_implements_Info_while_Al"; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
16 |
|
7299 | 17 |
(* to prove that before any alarm arrives (and after each acknowledgment), |
10127
86269867de34
renamed "None" to "NONE" (avoid clash with option type);
wenzelm
parents:
7299
diff
changeset
|
18 |
info remains at NONE *) |
7299 | 19 |
Goal "cockpit =<| Info_before_Al"; |
20 |
by (is_sim_tac aut_simps 1); |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
21 |
qed"cockpit_implements_Info_before_Al"; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
22 |
|
7299 | 23 |
(* to prove that before any alarm would be acknowledged, it must be arrived *) |
24 |
Goal "cockpit_hide =<| Al_before_Ack"; |
|
25 |
by (is_sim_tac aut_simps 1); |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
26 |
by Auto_tac; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
27 |
qed"cockpit_implements_Al_before_Ack"; |