// 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;
};