diff --git a/examples/lamport_orig.pnet b/examples/lamport_orig.pnet new file mode 100644 index 0000000000000000000000000000000000000000..d7e6288fe64a4e3457608086c089da291b7c8009 --- /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 +} +