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
|
// Synchronize n nodes by broadcasting messages.
// For a system of n nodes, the reachability graph will have
// 2^n vertices and n*2^n edges.
int n = 8;
typedef int (1..n) node_t;
typedef struct { node_t s; node_t r; } message_t;
place idle node_t: node_t node: node;
place pending node_t;
place messages message_t;
trans initiate
in {
place idle: node;
}
out {
place pending: node;
place messages: node_t other (other != node): {node, other};
};
trans finish in {
place pending: node;
place messages: node_t other (other != node): {node, other};
}
out {
place idle: node;
};
|
