author  wenzelm 
Fri, 20 Aug 1999 16:16:16 +0200  
changeset 7310  298b0dcadf2e 
parent 7299  743b22579a2f 
permissions  rwrr 
7299  1 

6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

2 
val aut_simps = [Greater_def,one_leader_def, 
7299  3 
one_leader_asig_def,one_leader_trans_def,one_leader_initial_def, 
4 
ring_def,aut0_asig_def,aut0_trans_def,aut0_initial_def,aut0_def, 

5 
aut1_asig_def,aut1_trans_def,aut1_initial_def,aut1_def, 

6 
aut2_asig_def,aut2_trans_def,aut2_initial_def,aut2_def]; 

6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

7 

08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

8 
(* property to prove: at most one (of 3) members of the ring will 
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

9 
declare itself to leader *) 
7299  10 
Goal "ring =< one_leader"; 
11 
by (is_sim_tac aut_simps 1); 

6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

12 
by Auto_tac; 
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset

13 
qed"at_most_one_leader"; 