diff --git a/snippets/COORDINATE/Synchronized_Coordination.mp b/snippets/COORDINATE/Synchronized_Coordination.mp new file mode 100644 index 0000000000000000000000000000000000000000..c308e6bbdd0ec4638a7f89a4c4d4a6032d91c2d0 --- /dev/null +++ b/snippets/COORDINATE/Synchronized_Coordination.mp @@ -0,0 +1,17 @@ +/* Synchronized coordination for iteration cycles adding + precedence relation only for events that appear in the + same cycle (MP Manual section 4.8) + SCHEMA S2 + ROOT R1: (+ (A | B) C +); + ROOT R2: (+ (D | E) F +); */ + +COORDINATE $a: (A | B) FROM R1, + $d: (D | E) FROM R2 +DO + IF $a IS A AND $d IS D OR $a IS B AND $d IS E THEN + /* This pair is selected from the same cycle,since the + default event sequence is used for coordination threads */ + ADD $a PRECEDES $d; + ELSE REJECT; /* otherwise reject the trace under derivation */ + FI; +OD;