BD10.net 5.38 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
#place Mutex  mk(<..>)
#place Idle0 mk(<..>)
#place Wait0
#place Update0
#place Mess0
#place Ack0
#place Idle1 mk(<..>)
#place Wait1
#place Update1
#place Mess1
#place Ack1
#place Idle2 mk(<..>)
#place Wait2
#place Update2
#place Mess2
#place Ack2
#place Idle3 mk(<..>)
#place Wait3
#place Update3
#place Mess3
#place Ack3
#place Idle4 mk(<..>)
#place Wait4
#place Update4
#place Mess4
#place Ack4
#place Idle5 mk(<..>)
#place Wait5
#place Update5
#place Mess5
#place Ack5
#place Idle6 mk(<..>)
#place Wait6
#place Update6
#place Mess6
#place Ack6
#place Idle7 mk(<..>)
#place Wait7
#place Update7
#place Mess7
#place Ack7
#place Idle8 mk(<..>)
#place Wait8
#place Update8
#place Mess8
#place Ack8
#place Idle9 mk(<..>)
#place Wait9
#place Update9
#place Mess9
#place Ack9
#trans T1_0
in {Idle0:<..>;Mutex:<..>;}
out {Wait0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_0
in {Wait0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle0:<..>;Mutex:<..>;}
#endtr
#trans T3_0
in {Idle0:<..>;Mess0:<..>;}
out {Update0:<..>;}
#endtr
#trans T4_0
in {Update0:<..>;}
out {Idle0:<..>;Ack0:<..>;}
#endtr
#trans T1_1
in {Idle1:<..>;Mutex:<..>;}
out {Wait1:<..>;Mess0:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_1
in {Wait1:<..>;Ack0:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle1:<..>;Mutex:<..>;}
#endtr
#trans T3_1
in {Idle1:<..>;Mess1:<..>;}
out {Update1:<..>;}
#endtr
#trans T4_1
in {Update1:<..>;}
out {Idle1:<..>;Ack1:<..>;}
#endtr
#trans T1_2
in {Idle2:<..>;Mutex:<..>;}
out {Wait2:<..>;Mess0:<..>;Mess1:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_2
in {Wait2:<..>;Ack0:<..>;Ack1:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle2:<..>;Mutex:<..>;}
#endtr
#trans T3_2
in {Idle2:<..>;Mess2:<..>;}
out {Update2:<..>;}
#endtr
#trans T4_2
in {Update2:<..>;}
out {Idle2:<..>;Ack2:<..>;}
#endtr
#trans T1_3
in {Idle3:<..>;Mutex:<..>;}
out {Wait3:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_3
in {Wait3:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle3:<..>;Mutex:<..>;}
#endtr
#trans T3_3
in {Idle3:<..>;Mess3:<..>;}
out {Update3:<..>;}
#endtr
#trans T4_3
in {Update3:<..>;}
out {Idle3:<..>;Ack3:<..>;}
#endtr
#trans T1_4
in {Idle4:<..>;Mutex:<..>;}
out {Wait4:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_4
in {Wait4:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle4:<..>;Mutex:<..>;}
#endtr
#trans T3_4
in {Idle4:<..>;Mess4:<..>;}
out {Update4:<..>;}
#endtr
#trans T4_4
in {Update4:<..>;}
out {Idle4:<..>;Ack4:<..>;}
#endtr
#trans T1_5
in {Idle5:<..>;Mutex:<..>;}
out {Wait5:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_5
in {Wait5:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle5:<..>;Mutex:<..>;}
#endtr
#trans T3_5
in {Idle5:<..>;Mess5:<..>;}
out {Update5:<..>;}
#endtr
#trans T4_5
in {Update5:<..>;}
out {Idle5:<..>;Ack5:<..>;}
#endtr
#trans T1_6
in {Idle6:<..>;Mutex:<..>;}
out {Wait6:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_6
in {Wait6:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle6:<..>;Mutex:<..>;}
#endtr
#trans T3_6
in {Idle6:<..>;Mess6:<..>;}
out {Update6:<..>;}
#endtr
#trans T4_6
in {Update6:<..>;}
out {Idle6:<..>;Ack6:<..>;}
#endtr
#trans T1_7
in {Idle7:<..>;Mutex:<..>;}
out {Wait7:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess8:<..>;Mess9:<..>;}
#endtr
#trans T2_7
in {Wait7:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack8:<..>;Ack9:<..>;}
out {Idle7:<..>;Mutex:<..>;}
#endtr
#trans T3_7
in {Idle7:<..>;Mess7:<..>;}
out {Update7:<..>;}
#endtr
#trans T4_7
in {Update7:<..>;}
out {Idle7:<..>;Ack7:<..>;}
#endtr
#trans T1_8
in {Idle8:<..>;Mutex:<..>;}
out {Wait8:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess9:<..>;}
#endtr
#trans T2_8
in {Wait8:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack9:<..>;}
out {Idle8:<..>;Mutex:<..>;}
#endtr
#trans T3_8
in {Idle8:<..>;Mess8:<..>;}
out {Update8:<..>;}
#endtr
#trans T4_8
in {Update8:<..>;}
out {Idle8:<..>;Ack8:<..>;}
#endtr
#trans T1_9
in {Idle9:<..>;Mutex:<..>;}
out {Wait9:<..>;Mess0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;}
#endtr
#trans T2_9
in {Wait9:<..>;Ack0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;}
out {Idle9:<..>;Mutex:<..>;}
#endtr
#trans T3_9
in {Idle9:<..>;Mess9:<..>;}
out {Update9:<..>;}
#endtr
#trans T4_9
in {Update9:<..>;}
out {Idle9:<..>;Ack9:<..>;}
#endtr