src/HOLCF/IOA/Modelcheck/Ring3.ML
author wenzelm
Fri, 20 Aug 1999 16:16:16 +0200
changeset 7310 298b0dcadf2e
parent 7299 743b22579a2f
permissions -rw-r--r--
activate example;
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 = [Greater_def,one_leader_def,
7299
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
     3
  one_leader_asig_def,one_leader_trans_def,one_leader_initial_def,
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
     4
  ring_def,aut0_asig_def,aut0_trans_def,aut0_initial_def,aut0_def,
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
     5
  aut1_asig_def,aut1_trans_def,aut1_initial_def,aut1_def,
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
     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
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
    10
Goal "ring =<| one_leader";
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset
    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";