From abecc460fb0a1f14d326808ff32d6071bd259c82 Mon Sep 17 00:00:00 2001
From: Philipp Meyer <philipp.j.meyer@gmail.com>
Date: Thu, 20 Nov 2014 10:23:04 +0100
Subject: [PATCH] Added original example for Lamport's algorithm

---
 examples/lamport_orig.pnet | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 examples/lamport_orig.pnet

diff --git a/examples/lamport_orig.pnet b/examples/lamport_orig.pnet
new file mode 100644
index 00000000..d7e6288f
--- /dev/null
+++ b/examples/lamport_orig.pnet
@@ -0,0 +1,29 @@
+petri net "Lamport's algorithm" {
+    places {
+        p1 p2 p3       b1 nb1
+        q1 q2 q3 q4 q5    nb2
+    }
+    transitions {
+        s1 s2 s3
+        t1 t2 t3 t4 t5 t6
+    }
+    arcs {
+        { p1, nb1 } -> s1 -> { p2,  b1 }
+        { p2, nb2 } -> s2 -> { p3, nb2 }
+        { p3,  b1 } -> s3 -> { p1, nb1 }
+
+        { q1, nb2 } -> t1 -> { q2,     }
+        { q2,  b1 } -> t2 -> { q3,  b1 }
+        { q3,     } -> t3 -> { q4, nb2 }
+        { q4, nb1 } -> t4 -> { q1, nb1 }
+        { q2, nb1 } -> t5 -> { q5, nb1 }
+        { q5,     } -> t6 -> { q1, nb2 }
+    }
+    initial {
+        p1 q1 nb1 nb2
+    }
+}
+safety property "mutual exclusion" {
+    p3 >= 1 && q5 >= 1
+}
+
-- 
GitLab