1 theory Ring3 |
|
2 imports MuIOAOracle |
|
3 begin |
|
4 |
|
5 datatype token = Leader | id0 | id1 | id2 | id3 | id4 |
|
6 |
|
7 datatype Comm = |
|
8 Zero_One token | One_Two token | Two_Zero token | |
|
9 Leader_Zero | Leader_One | Leader_Two |
|
10 |
|
11 definition |
|
12 Greater :: "[token, token] => bool" where |
|
13 "Greater x y = |
|
14 (x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) | |
|
15 (x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)" |
|
16 |
|
17 |
|
18 (*the ring is the composition of aut0, aut1 and aut2*) |
|
19 |
|
20 automaton aut0 = |
|
21 signature |
|
22 actions Comm |
|
23 inputs "Two_Zero t" |
|
24 outputs "Zero_One t","Leader_Zero" |
|
25 states |
|
26 idf :: token |
|
27 initially "idf=id0 | idf = id3" |
|
28 transitions |
|
29 "Two_Zero t" |
|
30 transrel |
|
31 "if (t=id0 | t=id3) then (idf'=Leader) else |
|
32 (if (Greater t idf) then (idf'=t) else (idf'=idf))" |
|
33 "Zero_One t" |
|
34 pre "t=idf" |
|
35 "Leader_Zero" |
|
36 pre "idf=Leader" |
|
37 |
|
38 automaton aut1 = |
|
39 signature |
|
40 actions Comm |
|
41 inputs "Zero_One t" |
|
42 outputs "One_Two t","Leader_One" |
|
43 states |
|
44 idf :: token |
|
45 initially "idf=id1 | idf=id4" |
|
46 transitions |
|
47 "Zero_One t" |
|
48 transrel |
|
49 "if (t=id1 | t=id4) then (idf'=Leader) else |
|
50 (if (Greater t idf) then (idf'=t) else (idf'=idf))" |
|
51 "One_Two t" |
|
52 pre "t=idf" |
|
53 "Leader_One" |
|
54 pre "idf=Leader" |
|
55 |
|
56 automaton aut2 = |
|
57 signature |
|
58 actions Comm |
|
59 inputs "One_Two t" |
|
60 outputs "Two_Zero t","Leader_Two" |
|
61 states |
|
62 idf :: token |
|
63 initially "idf=id2" |
|
64 transitions |
|
65 "One_Two t" |
|
66 transrel |
|
67 "if (t=id2) then (idf'=Leader) else |
|
68 (if (Greater t idf) then (idf'=t) else (idf'=idf))" |
|
69 "Two_Zero t" |
|
70 pre "t=idf" |
|
71 "Leader_Two" |
|
72 pre "idf=Leader" |
|
73 |
|
74 automaton ring = compose aut0, aut1, aut2 |
|
75 |
|
76 |
|
77 (*one_leader expresses property that at most one component declares |
|
78 itself to leader*) |
|
79 |
|
80 automaton one_leader = |
|
81 signature |
|
82 actions Comm |
|
83 outputs "Zero_One t","One_Two t","Two_Zero t","Leader_Zero","Leader_One","Leader_Two" |
|
84 states |
|
85 leader :: token |
|
86 initially "leader=Leader" |
|
87 transitions |
|
88 "Zero_One t" |
|
89 pre "True" |
|
90 "One_Two t" |
|
91 pre "True" |
|
92 "Two_Zero t" |
|
93 pre "True" |
|
94 "Leader_Zero" |
|
95 pre "leader=id0 | leader=Leader" |
|
96 post leader:="id0" |
|
97 "Leader_One" |
|
98 pre "leader=id1 | leader=Leader" |
|
99 post leader:="id1" |
|
100 "Leader_Two" |
|
101 pre "leader=id2 | leader=Leader" |
|
102 post leader:="id2" |
|
103 |
|
104 lemmas aut_simps = |
|
105 Greater_def one_leader_def |
|
106 one_leader_asig_def one_leader_trans_def one_leader_initial_def |
|
107 ring_def aut0_asig_def aut0_trans_def aut0_initial_def aut0_def |
|
108 aut1_asig_def aut1_trans_def aut1_initial_def aut1_def |
|
109 aut2_asig_def aut2_trans_def aut2_initial_def aut2_def |
|
110 |
|
111 (* property to prove: at most one (of 3) members of the ring will |
|
112 declare itself to leader *) |
|
113 lemma at_most_one_leader: "ring =<| one_leader" |
|
114 apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *}) |
|
115 apply auto |
|
116 done |
|
117 |
|
118 end |
|