Commit 9c2720f2 authored by Philipp Meyer's avatar Philipp Meyer

Added examples

parent ddea4d17
/*
Consider the following asynchronous program:
x = true;
h() {
if (x) {
post h();
post g();
}
}
g() {
x = false;
}
init: h()
The Petri net in this file emulates the execution of the program.
*/
petri net "asynchronous program" {
places {
// State
x not_x
// Scheduler
scheduler
// Handlers
h g
// Pending instances
pending_h pending_g
}
transitions {
dh dg ht hf gt gf
}
arcs {
// Dispatch h
{ scheduler, pending_h } -> dh -> h
// Dispatch g
{ scheduler, pending_g } -> dg -> g
// Exit h if x == true
{ h, x } -> ht -> { x, pending_h, pending_g, scheduler }
// Exit h if x == false
{ h, not_x } -> hf -> { not_x, scheduler }
// Exit g if x == true
{ g, x } -> gt -> { not_x, scheduler }
// Exit g if x == false
{ g, not_x } -> gf -> { not_x, scheduler }
}
initial {
// Initially, x is true, there's one pending instance of h(),
// and the scheduler has control.
x pending_h scheduler
}
}
safety property {
x >= 1 && not_x >= 1
}
liveness property "fair termination" {
dh >= 1 && dg >= 1
}
petri net "Lamport's algorithm" {
places {
p1 p2 p3 b1 nb1
q1 q2 q3 q4 q5 b2 nb2
}
transitions {
s1 s2 s3 s4
t1 t2 t3 t4 t5 t6 t7
}
arcs {
{ p1, nb1 } -> s1 -> { p2, b1 }
{ p2, b2 } -> s2 -> { p2, b2 }
{ p2, nb2 } -> s3 -> { p3, nb2 }
{ p3, b1 } -> s4 -> { p1, nb1 }
{ q1, nb2 } -> t1 -> { q2, b2 }
{ q2, b1 } -> t2 -> { q3, b1 }
{ q3, b2 } -> t3 -> { q4, nb2 }
{ q4, nb1 } -> t4 -> { q1, nb1 }
{ q4, b1 } -> t5 -> { q4, b1 }
{ q2, nb1 } -> t6 -> { q5, nb1 }
{ q5, b2 } -> t7 -> { q1, nb2 }
}
initial {
p1 q1 nb1 nb2
}
}
liveness property "fairness for first process" {
s1 + s2 > 0 && s3 = 0 && t6 >= 1
}
liveness property "fairness for second process" {
t1 + t2 + t3 + t4 > 0 && t6 = 0 && s3 >= 1
}
safety property "mutual exclusion" {
p3 >= 1 && q5 >= 1
}
petri net {
places { s1 s2 s3 s4 }
transitions { t1 t2 t3 t4 }
arcs {
s1 -> t1 -> s2 -> t2 -> s1
s3 -> t3 -> s4 -> t4 -> s3
s1 -> t4 -> s1
s2 -> t3 -> s2
}
initial { s1 s3 }
}
liveness property {
t3 > 0 && t4 > 0 && t1 = 0 && t2 = 0
}
petri net "Peterson's algorithm" {
places {
p1 p2 p3 p4
q1 q2 q3 q4
m1f m1t m2f m2t
hold1 hold2
}
transitions {
u1 u2 u3 u4 u5 u6 u7
v1 v2 v3 v4 v5 v6 v7
}
arcs {
{ p1 m1f } -> u1 -> { p2 m1t }
{ p2 hold2 } -> u2 -> { p3 hold1 }
{ p2 hold1 } -> u3 -> { p3 hold1 }
{ p3 m2f } -> u4 -> { p4 m2f }
{ p3 hold2 } -> u5 -> { p4 hold2 }
{ p3 hold1 m2t } -> u6 -> { p3 hold1 m2t }
{ p4 m1t } -> u7 -> { p1 m1f }
{ q1 m2f } -> v1 -> { q2 m2t }
{ q2 hold2 } -> v2 -> { q3 hold2 }
{ q2 hold1 } -> v3 -> { q3 hold2 }
{ q3 m1f } -> v4 -> { q4 m1f }
{ q3 hold1 } -> v5 -> { q4 hold1 }
{ q3 hold2 m1t } -> v6 -> { q3 hold2 m1t }
{ q4 m2t } -> v7 -> { q1 m2f }
}
initial {
p1 q1 m1f m2f hold1
}
}
liveness property "fairness for first process" {
u6 > 0 && u4 + u5 = 0 && v4 + v5 > 0
}
liveness property "fairness for second process" {
v6 > 0 && v4 + v5 = 0 && u4 + u5 > 0
}
safety property "mutual exclusion" {
p4 >= 1 && q4 >= 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