Commit ccadabd9 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Updated examples

parent 737a3931
......@@ -66,3 +66,6 @@ safety property {
liveness property "fair termination" {
dh >= 1 && dg >= 1
}
liveness property "h dispatched" {
dh = 0
}
......@@ -9,8 +9,8 @@ petri net "Lamport's algorithm" {
}
arcs {
{ p1, nb1 } -> s1 -> { p2, b1 }
{ p2, b2 } -> s2 -> { p2, b2 }
{ p2, nb2 } -> s3 -> { p3, nb2 }
{ p2, nb2 } -> s2 -> { p3, nb2 }
{ p2, b2 } -> s3 -> { p2, b2 }
{ p3, b1 } -> s4 -> { p1, nb1 }
{ q1, nb2 } -> t1 -> { q2, b2 }
......@@ -26,10 +26,13 @@ petri net "Lamport's algorithm" {
}
}
liveness property "fairness for first process" {
s1 + s2 > 0 && s3 = 0 && t1 + t2 + t3 + t4 + t5 + t6 + t7 > 0
s1 + s2 + s3 + s4 > 0 && s2 = 0 && t1 + t2 + t3 + t4 + t5 + t6 + t7 > 0
// && (s3 + t1 = 0 || t5 = 0 || t3 + t4 + t7 > 1) // [b2], [q4] for X = [s3,t5]
// && (t4 + t6 = 0 || s3 = 0 || s1 + s2 + s4 > 0) // [nb1], [p2,p3] for X = [s3,t1(2),t2,t3,t4,t5,t6,t7]
// && (s4 + t4 + t6 = 0 || s3 = 0 || s1 + s2 > 0) // [nb1], [p2] for X = [s3,t1(2),t2,t3,t4,t5,t6,t7]
}
liveness property "fairness for second process" {
t1 + t2 + t3 + t4 > 0 && t6 = 0 && s3 >= 1
s1 + s2 + s3 + s4 > 0 && t6 = 0 && t1 + t2 + t3 + t4 + t5 + t6 + t7 > 0
}
safety property "mutual exclusion" {
p3 >= 1 && q5 >= 1
......
petri net "simple liveness property test" {
places {
p1 p2 p3
}
transitions {
t1 t2 t3
}
arcs {
p1 -> t1 -> p1
p2 -> t1 -> p2
p1 -> t2 -> p2
p2 -> t3 -> p1
p3 -> t2
p3 -> t3
}
initial {
p1 p3
}
}
liveness property "termination" {
true
}
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