Commit abecc460 authored by Philipp Meyer's avatar Philipp Meyer

Added original example for Lamport's algorithm

parent a68e024c
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
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment