From 97f38c38fc4d56eff57a913ba62fdaca440eebd6 Mon Sep 17 00:00:00 2001
From: "Giammarco, Kristin M" <kmgiamma@nps.edu>
Date: Fri, 23 Jul 2021 01:01:07 +0000
Subject: [PATCH] Upload New File

---
 .../COORDINATE/Synchronized_Coordination.mp     | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 snippets/COORDINATE/Synchronized_Coordination.mp

diff --git a/snippets/COORDINATE/Synchronized_Coordination.mp b/snippets/COORDINATE/Synchronized_Coordination.mp
new file mode 100644
index 0000000..c308e6b
--- /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;
-- 
GitLab