BD2.net 784 Bytes
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
#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