Commit a7918233 authored by Philipp Meyer's avatar Philipp Meyer

Added two more examples

parent 1cd4955c
petri net "leader election 2" {
places {
s1 s1x1 s1x2
s2 s2x1 s2x2
lead
}
transitions {
s1send1 s1pass2 s1accept1
s2send2 s2discard1 s2accept2
newleader
}
arcs {
s1 -> s1send1 -> s1x1
s2 -> s2send2 -> s2x2
s1x1 -> s2discard1
s1x2 -> s2accept2 -> lead
s2x1 -> s1accept1 -> lead
s2x2 -> s1pass2 -> s1x2
lead -> newleader -> { s1 s2 }
}
initial { s1 s2 }
}
safety property {
lead >= 2
}
liveness property {
newleader > 0 || newleader = 0
}
petri net "snapshot 2" {
places {
white1 red1 received1 notreceived1 sent1 notsent1 marker1 sample1 done1
white2 red2 received2 notreceived2 sent2 notsent2 marker2 sample2 done2
}
transitions {
init1 receive_white1 receive_red1 send1
init2 receive_white2 receive_red2 send2
snapshot
reset1
reset2
}
arcs {
white1 -> init1 -> { red1, sample1 }
{ white1, notreceived1, marker2 } -> receive_white1 -> { red1, received1, sample1 }
{ red1, notreceived1, marker2 } -> receive_red1 -> { red1, received1 }
{ red1, notsent1 } -> send1 -> { red1, sent1, marker1 }
white2 -> init2 -> { red2, sample2 }
{ white2, notreceived2, marker1 } -> receive_white2 -> { red2, received2, sample2 }
{ red2, notreceived2, marker1 } -> receive_red2 -> { red2, received2 }
{ red2, notsent2 } -> send2 -> { red2, sent2, marker2 }
{ sample1, sample2 } -> snapshot -> { done1, done2 }
{ red1, done1, received1, sent1 } -> reset1 -> { white1, notreceived1, notsent1 }
{ red2, done2, received2, sent2 } -> reset2 -> { white2, notreceived2, notsent2 }
}
initial {
white1 notreceived1 notsent1
white2 notreceived2 notsent2
}
}
liveness property {
init2 = 0
}
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