Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/Modelcheck/Cockpit.ML
author wenzelm
Thu, 07 Apr 2005 09:25:33 +0200
changeset 15661 9ef583b08647
parent 10127 86269867de34
permissions -rw-r--r--
reverted renaming of Some/None in comments and strings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7299
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset 
     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






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    13


Goal "cockpit =<| Info_while_Al";













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    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






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    17


(* to prove that before any alarm arrives (and after each acknowledgment),








15661






9ef583b08647
reverted renaming of Some/None in comments and strings;



wenzelm


parents: 
10127

diff
changeset




    18


   info remains at None *)








7299






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    19


Goal "cockpit =<| Info_before_Al";













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    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






743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    23


(* to prove that before any alarm would be acknowledged, it must be arrived *)













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    24


Goal "cockpit_hide =<| Al_before_Ack";













743b22579a2f
quite a lot of tuning and cleanup;



wenzelm


parents: 
6471

diff
changeset




    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";















isabelle