Commit 75c351a1 authored by Jaime Arias's avatar Jaime Arias
Browse files

Add several examples

parent 6adae9a2
4
T1_0 T2_0 T3_0 T4_0
40
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5 T1_6 T2_6 T3_6 T4_6 T1_7 T2_7 T3_7 T4_7 T1_8 T2_8 T3_8 T4_8 T1_9 T2_9 T3_9 T4_9
\ No newline at end of file
8
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1
80
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5 T1_6 T2_6 T3_6 T4_6 T1_7 T2_7 T3_7 T4_7 T1_8 T2_8 T3_8 T4_8 T1_9 T2_9 T3_9 T4_9 T1_10 T2_10 T3_10 T4_10 T1_11 T2_11 T3_11 T4_11 T1_12 T2_12 T3_12 T4_12 T1_13 T2_13 T3_13 T4_13 T1_14 T2_14 T3_14 T4_14 T1_15 T2_15 T3_15 T4_15 T1_16 T2_16 T3_16 T4_16 T1_17 T2_17 T3_17 T4_17 T1_18 T2_18 T3_18 T4_18 T1_19 T2_19 T3_19 T4_19
\ No newline at end of file
12
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2
\ No newline at end of file
16
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3
20
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4
24
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5
28
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5 T1_6 T2_6 T3_6 T4_6
32
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5 T1_6 T2_6 T3_6 T4_6 T1_7 T2_7 T3_7 T4_7
36
T1_0 T2_0 T3_0 T4_0 T1_1 T2_1 T3_1 T4_1 T1_2 T2_2 T3_2 T4_2 T1_3 T2_3 T3_3 T4_3 T1_4 T2_4 T3_4 T4_4 T1_5 T2_5 T3_5 T4_5 T1_6 T2_6 T3_6 T4_6 T1_7 T2_7 T3_7 T4_7 T1_8 T2_8 T3_8 T4_8
\ No newline at end of file
12
start_0 start_1 bc_0_1_0 bc_0_1_1 bc_1_1_0 bc_1_1_1 ccs_1_0_0 ccs_0_1_0 ccsturn_0_1_1 ccsturn_1_0_0 csinit_0 csinit_1
69
start_0 start_1 start_2 ab_0_2 ab_1_2 ab_2_2 bc_0_1_0 bc_0_2_0 bc_0_1_1 bc_0_2_1 bc_0_1_2 bc_0_2_2 bc_1_1_0 bc_1_2_0 bc_1_1_1 bc_1_2_1 bc_1_1_2 bc_1_2_2 bc_2_1_0 bc_2_2_0 bc_2_1_1 bc_2_2_1 bc_2_1_2 bc_2_2_2 cc_0_1_1_0 cc_0_2_1_0 cc_0_2_1_1 cc_1_1_2_0 cc_1_2_2_0 cc_1_2_2_1 cc_2_1_0_0 cc_2_2_0_0 cc_2_2_0_1 cc_1_1_0_0 cc_2_1_1_0 cc_0_1_2_0 ccs_1_0_0 ccs_1_0_1 ccs_2_1_0 ccs_2_1_1 ccs_0_2_0 ccs_0_2_1 caturn_0_1_1_1 caturn_0_1_1_2 caturn_0_1_2_1 caturn_0_1_2_2 caturn_1_1_0_0 caturn_1_1_0_2 caturn_1_1_2_0 caturn_1_1_2_2 caturn_2_1_0_0 caturn_2_1_0_1 caturn_2_1_1_0 caturn_2_1_1_1 ccsturn_0_1_1 ccsturn_0_1_2 ccsturn_0_2_1 ccsturn_0_2_2 ccsturn_1_0_0 ccsturn_1_0_2 ccsturn_1_2_0 ccsturn_1_2_2 ccsturn_2_0_0 ccsturn_2_0_1 ccsturn_2_1_0 ccsturn_2_1_1 csinit_0 csinit_1 csinit_2
\ No newline at end of file
244
start_0
start_1
start_2
start_3
ab_0_2
ab_0_3
ab_1_2
ab_1_3
ab_2_2
ab_2_3
ab_3_2
ab_3_3
bc_0_1_0
bc_0_2_0
bc_0_3_0
bc_0_1_1
bc_0_2_1
bc_0_3_1
bc_0_1_2
bc_0_2_2
bc_0_3_2
bc_0_1_3
bc_0_2_3
bc_0_3_3
bc_1_1_0
bc_1_2_0
bc_1_3_0
bc_1_1_1
bc_1_2_1
bc_1_3_1
bc_1_1_2
bc_1_2_2
bc_1_3_2
bc_1_1_3
bc_1_2_3
bc_1_3_3
bc_2_1_0
bc_2_2_0
bc_2_3_0
bc_2_1_1
bc_2_2_1
bc_2_3_1
bc_2_1_2
bc_2_2_2
bc_2_3_2
bc_2_1_3
bc_2_2_3
bc_2_3_3
bc_3_1_0
bc_3_2_0
bc_3_3_0
bc_3_1_1
bc_3_2_1
bc_3_3_1
bc_3_1_2
bc_3_2_2
bc_3_3_2
bc_3_1_3
bc_3_2_3
bc_3_3_3
cc_0_1_1_0
cc_0_2_1_0
cc_0_2_1_1
cc_0_3_1_0
cc_0_3_1_1
cc_0_3_1_2
cc_0_1_2_0
cc_0_2_2_0
cc_0_2_2_1
cc_0_3_2_0
cc_0_3_2_1
cc_0_3_2_2
cc_1_1_2_0
cc_1_2_2_0
cc_1_2_2_1
cc_1_3_2_0
cc_1_3_2_1
cc_1_3_2_2
cc_1_1_3_0
cc_1_2_3_0
cc_1_2_3_1
cc_1_3_3_0
cc_1_3_3_1
cc_1_3_3_2
cc_2_1_0_0
cc_2_2_0_0
cc_2_2_0_1
cc_2_3_0_0
cc_2_3_0_1
cc_2_3_0_2
cc_2_1_3_0
cc_2_2_3_0
cc_2_2_3_1
cc_2_3_3_0
cc_2_3_3_1
cc_2_3_3_2
cc_3_1_0_0
cc_3_2_0_0
cc_3_2_0_1
cc_3_3_0_0
cc_3_3_0_1
cc_3_3_0_2
cc_3_1_1_0
cc_3_2_1_0
cc_3_2_1_1
cc_3_3_1_0
cc_3_3_1_1
cc_3_3_1_2
cc_1_1_0_0
cc_1_2_0_0
cc_1_2_0_1
cc_2_1_1_0
cc_2_2_1_0
cc_2_2_1_1
cc_3_1_2_0
cc_3_2_2_0
cc_3_2_2_1
cc_0_1_3_0
cc_0_2_3_0
cc_0_2_3_1
ccs_1_0_0
ccs_1_0_1
ccs_1_0_2
ccs_2_1_0
ccs_2_1_1
ccs_2_1_2
ccs_3_2_0
ccs_3_2_1
ccs_3_2_2
ccs_0_3_0
ccs_0_3_1
ccs_0_3_2
caturn_0_1_1_1
caturn_0_1_1_2
caturn_0_1_1_3
caturn_0_2_1_1
caturn_0_2_1_2
caturn_0_2_1_3
caturn_0_1_2_1
caturn_0_1_2_2
caturn_0_1_2_3
caturn_0_2_2_1
caturn_0_2_2_2
caturn_0_2_2_3
caturn_0_1_3_1
caturn_0_1_3_2
caturn_0_1_3_3
caturn_0_2_3_1
caturn_0_2_3_2
caturn_0_2_3_3
caturn_1_1_0_0
caturn_1_1_0_2
caturn_1_1_0_3
caturn_1_2_0_0
caturn_1_2_0_2
caturn_1_2_0_3
caturn_1_1_2_0
caturn_1_1_2_2
caturn_1_1_2_3
caturn_1_2_2_0
caturn_1_2_2_2
caturn_1_2_2_3
caturn_1_1_3_0
caturn_1_1_3_2
caturn_1_1_3_3
caturn_1_2_3_0
caturn_1_2_3_2
caturn_1_2_3_3
caturn_2_1_0_0
caturn_2_1_0_1
caturn_2_1_0_3
caturn_2_2_0_0
caturn_2_2_0_1
caturn_2_2_0_3
caturn_2_1_1_0
caturn_2_1_1_1
caturn_2_1_1_3
caturn_2_2_1_0
caturn_2_2_1_1
caturn_2_2_1_3
caturn_2_1_3_0
caturn_2_1_3_1
caturn_2_1_3_3
caturn_2_2_3_0
caturn_2_2_3_1
caturn_2_2_3_3
caturn_3_1_0_0
caturn_3_1_0_1
caturn_3_1_0_2
caturn_3_2_0_0
caturn_3_2_0_1
caturn_3_2_0_2
caturn_3_1_1_0
caturn_3_1_1_1
caturn_3_1_1_2
caturn_3_2_1_0
caturn_3_2_1_1
caturn_3_2_1_2
caturn_3_1_2_0
caturn_3_1_2_1
caturn_3_1_2_2
caturn_3_2_2_0
caturn_3_2_2_1
caturn_3_2_2_2
ccsturn_0_1_1
ccsturn_0_1_2
ccsturn_0_1_3
ccsturn_0_2_1
ccsturn_0_2_2
ccsturn_0_2_3
ccsturn_0_3_1
ccsturn_0_3_2
ccsturn_0_3_3
ccsturn_1_0_0
ccsturn_1_0_2
ccsturn_1_0_3
ccsturn_1_2_0
ccsturn_1_2_2
ccsturn_1_2_3
ccsturn_1_3_0
ccsturn_1_3_2
ccsturn_1_3_3
ccsturn_2_0_0
ccsturn_2_0_1
ccsturn_2_0_3
ccsturn_2_1_0
ccsturn_2_1_1
ccsturn_2_1_3
ccsturn_2_3_0
ccsturn_2_3_1
ccsturn_2_3_3
ccsturn_3_0_0
ccsturn_3_0_1
ccsturn_3_0_2
ccsturn_3_1_0
ccsturn_3_1_1
ccsturn_3_1_2
ccsturn_3_2_0
ccsturn_3_2_1
ccsturn_3_2_2
csinit_0
csinit_1
csinit_2
csinit_3
\ No newline at end of file
#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
#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
#trans T1_0
in {Idle0:<..>;Mutex:<..>;}
out {Wait0:<..>;Mess1:<..>;}
#endtr
#trans T2_0
in {Wait0:<..>;Ack1:<..>;}
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:<..>;}
#endtr
#trans T2_1
in {Wait1:<..>;Ack0:<..>;}
out {Idle1:<..>;Mutex:<..>;}
#endtr
#trans T3_1
in {Idle1:<..>;Mess1:<..>;}
out {Update1:<..>;}
#endtr
#trans T4_1
in {Update1:<..>;}
out {Idle1:<..>;Ack1:<..>;}
#endtr
#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
#place Idle10 mk(<..>)
#place Wait10
#place Update10
#place Mess10
#place Ack10
#place Idle11 mk(<..>)
#place Wait11
#place Update11
#place Mess11
#place Ack11
#place Idle12 mk(<..>)
#place Wait12
#place Update12
#place Mess12
#place Ack12
#place Idle13 mk(<..>)
#place Wait13
#place Update13
#place Mess13
#place Ack13
#place Idle14 mk(<..>)
#place Wait14
#place Update14
#place Mess14
#place Ack14
#place Idle15 mk(<..>)
#place Wait15
#place Update15
#place Mess15
#place Ack15
#place Idle16 mk(<..>)
#place Wait16
#place Update16
#place Mess16
#place Ack16
#place Idle17 mk(<..>)
#place Wait17
#place Update17
#place Mess17
#place Ack17
#place Idle18 mk(<..>)
#place Wait18
#place Update18
#place Mess18
#place Ack18
#place Idle19 mk(<..>)
#place Wait19
#place Update19
#place Mess19
#place Ack19
#trans T1_0
in {Idle0:<..>;Mutex:<..>;}
out {Wait0:<..>;Mess1:<..>;Mess2:<..>;Mess3:<..>;Mess4:<..>;Mess5:<..>;Mess6:<..>;Mess7:<..>;Mess8:<..>;Mess9:<..>;Mess10:<..>;Mess11:<..>;Mess12:<..>;Mess13:<..>;Mess14:<..>;Mess15:<..>;Mess16:<..>;Mess17:<..>;Mess18:<..>;Mess19:<..>;}
#endtr
#trans T2_0
in {Wait0:<..>;Ack1:<..>;Ack2:<..>;Ack3:<..>;Ack4:<..>;Ack5:<..>;Ack6:<..>;Ack7:<..>;Ack8:<..>;Ack9:<..>;Ack10:<..>;Ack11:<..>;Ack12:<..>;Ack13:<..>;Ack14:<..>;Ack15:<..>;Ack16:<..>;Ack17:<..>;Ack18:<..>;Ack19:<..>;}
out {Idle0:<..>;Mutex:<..>;}
#endtr
#trans T3_0
in {Idle0:<..>;Mess0:<..>;}
out {Update0:<..>;}
#endtr
#trans T4_0
in {Update0:<..>;}
out {Idle0:<..>;Ack0:<..>;}