O 24
P 43
S 1 state
S 1 message
S 1 number_
S 1 queuetype
S 1 process
S 1 queue-state
S 1 number
S 1 queue
S 1 proctype
S 1 transition
S 1 object
S 2 is-a-queue
S 2 is-a-process
S 4 trans
S 3 writes
S 3 reads
S 3 queue-next
S 2 trans-msg
S 2 inc
S 2 dec
S 2 queue-max
S 1 is-zero
S 1 is-not-zero
S 2 is-max
S 2 is-not-max
S 2 =
F 2 at-process
F 2 enabled
F 1 pending
F 2 activate
F 2 queue-head
F 2 queue-tail
F 1 advance-tail
F 1 advance-head
F 1 settled
F 3 queue-msg
F 2 queue-head-msg
F 2 queue-tail-msg
F 2 queue-size
D 1 blocked
D 2 blocked-trans
D 0 axiom_0
D 3 axiom_1
N 0
SI 112
10 0
4 0
10 1
4 1
10 2
4 2
10 3
4 3
10 4
7 4
10 5
7 5
10 6
7 6
10 7
7 7
10 8
3 8
10 9
5 9
10 10
1 10
10 11
1 11
10 12
2 12
10 13
2 13
10 14
8 14
10 15
0 15
10 16
0 16
10 17
0 17
10 18
0 18
10 19
0 19
10 20
9 20
10 21
9 21
10 22
9 22
10 23
9 23
16 8 9 9
24 8 12
23 8 13
12 0 14
12 1 14
12 2 14
12 3 14
21 12
19 13 12
18 12 13
22 13
11 4 8
11 5 8
11 6 8
11 7 8
14 0 4 20
17 20 11
15 0 4 21
17 21 11
15 0 5 22
17 22 11
14 0 5 23
17 23 11
14 1 5 20
15 1 5 21
15 1 6 22
14 1 6 23
14 2 6 20
15 2 6 21
15 2 7 22
14 2 7 23
14 3 7 20
15 3 7 21
15 3 4 22
14 3 4 23
13 14 20 15 16
13 14 21 16 17
13 14 22 17 18
13 14 20 18 19
13 14 23 19 16
25 0 0
25 1 1
25 2 2
25 3 3
25 4 4
25 5 5
25 6 6
25 7 7
25 8 8
25 9 9
25 10 10
25 11 11
25 12 12
25 13 13
25 14 14
25 15 15
25 16 16
25 17 17
25 18 18
25 19 19
25 20 20
25 21 21
25 22 22
25 23 23
FI 28
28 0
26 0 15
28 1
26 1 15
28 2
26 2 15
28 3
26 3 15
30 4 9
31 4 9
36 4 10
38 4 12
34 4
30 5 9
31 5 9
36 5 10
38 5 12
34 5
30 6 9
31 6 9
36 6 10
38 6 12
34 6
30 7 9
31 7 9
36 7 10
38 7 12
34 7
NI 0
G 4
39 1 0
39 1 1
39 1 2
39 1 3
NG 0
M none
A 7
queue-read 4
L 13
10 1 0
4 1 0
10 1 1
9 1 1
10 1 2
7 1 2
10 1 3
1 1 3
15 1 0 2 1
17 1 1 3
29 1 0 1
34 1 2
36 1 2 3
NC 0
E 1
0
L 0
NC 0
F 4
29 0 0 1
33 1 2
34 0 2
27 1 0 1
NE 0
NA -
queue-write 4
L 12
10 1 0
4 1 0
10 1 1
9 1 1
10 1 2
7 1 2
10 1 3
1 1 3
17 1 1 3
14 1 0 2 1
29 1 0 1
34 1 2
NC 0
E 1
0
L 0
NC 0
F 5
29 0 0 1
34 0 2
27 1 0 1
32 1 2
37 1 2 3
NE 0
NA -
advance-queue-head 7
L 21
10 1 0
7 1 0
10 1 4
1 1 4
10 1 1
3 1 1
10 1 2
5 1 2
10 1 3
5 1 3
10 1 5
2 1 5
10 1 6
2 1 6
11 1 0 1
16 1 1 2 3
19 1 5 6
33 1 0
30 1 0 2
35 1 0 3 4
38 1 0 5
NC 0
E 1
0
L 0
NC 0
F 7
34 1 0
36 1 0 4
30 1 0 3
33 0 0
30 0 0 2
38 0 0 5
38 1 0 6
NE 0
NA -
advance-empty-queue-tail 8
L 25
10 1 0
7 1 0
10 1 4
1 1 4
10 1 1
3 1 1
10 1 2
5 1 2
10 1 3
5 1 3
11 1 0 1
16 1 1 2 3
10 1 6
2 1 6
10 1 7
2 1 7
10 1 5
1 1 5
18 1 6 7
21 1 6
32 1 0
37 1 0 4
38 1 0 6
31 1 0 2
36 1 0 5
NC 0
E 1
0
L 0
NC 0
F 9
35 1 0 3 4
34 1 0
36 1 0 4
38 0 0 6
38 1 0 7
32 0 0
31 1 0 3
31 0 0 2
36 0 0 5
NE 0
NA -
advance-non-empty-queue-tail 7
L 22
10 1 0
7 1 0
10 1 4
1 1 4
10 1 1
3 1 1
10 1 2
5 1 2
10 1 3
5 1 3
10 1 5
2 1 5
10 1 6
2 1 6
11 1 0 1
16 1 1 2 3
18 1 5 6
22 1 5
38 1 0 5
32 1 0
37 1 0 4
31 1 0 2
NC 0
E 1
0
L 0
NC 0
F 7
35 1 0 3 4
34 1 0
38 0 0 5
38 1 0 6
32 0 0
31 1 0 3
31 0 0 2
NE 0
NA -
perform-trans 5
L 15
10 1 0
4 1 0
10 1 2
9 1 2
10 1 1
8 1 1
10 1 3
0 1 3
10 1 4
0 1 4
13 1 1 2 3 4
27 1 0 2
26 1 0 3
41 0
41 0
NC 0
E 1
0
L 0
NC 0
F 4
26 1 0 4
26 0 0 3
27 0 0 2
28 1 0
NE 0
NA -
activate-trans 5
L 16
10 1 0
4 1 0
10 1 2
9 1 2
10 1 1
8 1 1
10 1 3
0 1 3
10 1 4
0 1 4
13 1 1 2 3 4
12 1 0 1
26 1 0 3
28 1 0
41 0
41 0
NC 0
E 1
0
L 0
NC 0
F 2
29 1 0 2
28 0 0
NE 0
NA -
X 6
41 1
H
L 3
10 1 0
7 1 0
34 0 0
NC 0
42 5
H 0 1 2
L 12
10 1 0
4 1 0
10 1 4
0 1 4
10 1 3
9 1 3
10 1 2
8 1 2
10 1 1
0 1 1
13 1 2 3 1 4
40 0 0 3
NC 0
39 3
H 0
L 9
10 1 0
4 1 0
10 1 2
8 1 2
10 1 1
0 1 1
12 1 0 2
26 1 0 1
42 0 0 1 2
NC 0
40 5
H 0 1
L 16
10 1 0
4 1 0
10 1 1
9 1 1
10 1 2
7 1 2
10 1 3
1 1 3
15 1 0 2 1
17 1 1 3
10 1 4
2 1 4
21 1 4
29 1 0 1
34 1 2
38 1 2 4
NC 0
40 6
H 0 1
L 19
10 1 0
4 1 0
10 1 1
9 1 1
10 1 2
7 1 2
10 1 3
1 1 3
17 1 1 3
14 1 0 2 1
10 1 4
3 1 4
11 1 2 4
10 1 5
2 1 5
23 1 4 5
29 1 0 1
34 1 2
38 1 2 5
NC 0
40 5
H 0 1
L 16
10 1 0
4 1 0
10 1 1
9 1 1
10 1 2
7 1 2
10 1 3
1 1 3
15 1 0 2 1
17 1 1 3
10 1 4
1 1 4
25 0 3 4
29 1 0 1
34 1 2
36 1 2 4
NC 0
