11.3.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 64a250c5 authored by Philipp Meyer's avatar Philipp Meyer

Fixed example for leader election in nlogn

parent 0a3b470d
petri net "leader election nlogn 2" {
petri net "improved leader election 2" {
places {
a0 a1 a2 aH aP
amax_1 amax_2
aleft_0 aleft_1 aleft_2
am_1_n am_1_1 am_1_2 am_2_n am_2_1 am_2_2
b0 b1 b2 bH bP
bmax_1 bmax_2
bleft_0 bleft_1 bleft_2
bm_1_n bm_1_1 bm_1_2 bm_2_n bm_2_1 bm_2_2
aD bD
s1a0 s1a1 s1a2 s1aH s1aP s1aD
s1max1 s1max2
s1left0 s1left1 s1left2
s1m1_n s1m1_1 s1m1_2
s1m2_n s1m2_1 s1m2_2
s2a0 s2a1 s2a2 s2aH s2aP s2aD
s2max1 s2max2
s2left0 s2left1 s2left2
s2m1_n s2m1_1 s2m1_2
s2m2_n s2m2_1 s2m2_2
}
transitions {
a0send1
a0send2
a1rec1max1
a1rec2max2
a1rec2max1left0
a1rec1max2left0
a1rec2max1left1
a1rec1max2left1
a1rec2max1left2
a1rec1max2left2
a2rec1left0
a2rec2left0
a2rec1left1
a2rec2left1
a2rec2left2
a2rec1max1left2
a2rec1max2left2
aPrec1_1
aPrec1_2
aPrec2_1
aPrec2_2
b0send1
b0send2
b1rec1max1
b1rec2max2
b1rec2max1left0
b1rec1max2left0
b1rec2max1left1
b1rec1max2left1
b1rec2max1left2
b1rec1max2left2
b2rec1left0
b2rec2left0
b2rec1left1
b2rec2left1
b2rec2left2
b2rec1max1left2
b2rec1max2left2
bPrec1_1
bPrec1_2
bPrec2_1
bPrec2_2
aDone
bDone
aDmax1left0
aDmax2left0
aDmax1left1
aDmax2left1
aDmax1left2
aDmax2left2
bDmax1left0
bDmax2left0
bDmax1left1
bDmax2left1
bDmax1left2
bDmax2left2
s1a0send1 s1a0send2
s1a1rec1max1 s1a1rec1max2left0 s1a1rec1max2left1 s1a1rec1max2left2
s1a1rec2max1left0 s1a1rec2max1left1 s1a1rec2max1left2 s1a1rec2max2
s1a2rec1left0 s1a2rec1left1 s1a2rec1max1left2 s1a2rec1max2left2
s1a2rec2left0 s1a2rec2left1 s1a2rec2left2
s1aPrec1_1 s1aPrec2_1 s1aPrec1_2 s1aPrec2_2
s1aDmax1left0 s1aDmax1left1 s1aDmax1left2 s1aDmax2left0 s1aDmax2left1 s1aDmax2left2
s2a0send1 s2a0send2
s2a1rec1max1 s2a1rec1max2left0 s2a1rec1max2left1 s2a1rec1max2left2
s2a1rec2max1left0 s2a1rec2max1left1 s2a1rec2max1left2 s2a1rec2max2
s2a2rec1left0 s2a2rec1left1 s2a2rec1max1left2 s2a2rec1max2left2
s2a2rec2left0 s2a2rec2left1 s2a2rec2left2
s2aPrec1_1 s2aPrec2_1 s2aPrec1_2 s2aPrec2_2
s2aDmax1left0 s2aDmax1left1 s2aDmax1left2 s2aDmax2left0 s2aDmax2left1 s2aDmax2left2
s1done s2done
}
arcs {
{ a0 amax_1 am_1_n } -> a0send1 -> { a1 amax_1 am_1_1 }
{ a0 amax_2 am_1_n } -> a0send2 -> { a1 amax_1 am_1_2 }
{ a1 amax_1 bm_1_1 am_2_n } -> a1rec1max1 -> { aH amax_1 bm_1_n }
{ a1 amax_2 bm_1_2 am_2_n } -> a1rec2max2 -> { aH amax_2 bm_1_n }
{ a1 amax_2 aleft_0 bm_1_1 am_2_n } -> a1rec1max2left0 -> { a2 amax_2 aleft_1 bm_1_n am_2_1 }
{ a1 amax_1 aleft_0 bm_1_2 am_2_n } -> a1rec2max1left0 -> { a2 amax_1 aleft_2 bm_1_n am_2_2 }
{ a1 amax_2 aleft_1 bm_1_1 am_2_n } -> a1rec1max2left1 -> { a2 amax_2 aleft_1 bm_1_n am_2_1 }
{ a1 amax_1 aleft_1 bm_1_2 am_2_n } -> a1rec2max1left1 -> { a2 amax_1 aleft_2 bm_1_n am_2_2 }
{ a1 amax_2 aleft_2 bm_1_1 am_2_n } -> a1rec1max2left2 -> { a2 amax_2 aleft_1 bm_1_n am_2_1 }
{ a1 amax_1 aleft_2 bm_1_2 am_2_n } -> a1rec2max1left2 -> { a2 amax_1 aleft_2 bm_1_n am_2_2 }
{ a2 aleft_0 bm_2_1 } -> a2rec1left0 -> { aP aleft_0 bm_2_n }
{ a2 aleft_0 bm_2_2 } -> a2rec2left0 -> { aP aleft_0 bm_2_n }
{ a2 aleft_1 bm_2_1 } -> a2rec1left1 -> { aP aleft_1 bm_2_n }
{ a2 aleft_1 bm_2_2 } -> a2rec2left1 -> { aP aleft_1 bm_2_n }
{ a2 aleft_2 bm_2_2 } -> a2rec2left2 -> { aP aleft_2 bm_2_n }
{ a2 amax_1 aleft_2 bm_2_2 am_1_n } -> a2rec1max1left2 -> { a1 amax_2 aleft_2 bm_1_n am_1_1 }
{ a2 amax_2 aleft_2 bm_2_1 } -> a2rec1max2left2 -> { aP amax_2 aleft_2 bm_2_n }
{ aP bm_1_1 am_1_n } -> aPrec1_1 -> { aP bm_1_n am_1_1 }
{ aP bm_1_2 am_1_n } -> aPrec1_2 -> { aP bm_1_n am_1_2 }
{ aP bm_2_1 am_2_n } -> aPrec2_1 -> { aP bm_1_n am_2_1 }
{ aP bm_2_2 am_2_n } -> aPrec2_2 -> { aP bm_1_n am_2_2 }
{ b0 bmax_1 bm_1_n } -> b0send1 -> { b1 bmax_1 bm_1_1 }
{ b0 bmax_2 bm_1_n } -> b0send2 -> { b1 bmax_1 bm_1_2 }
{ b1 bmax_1 am_1_1 bm_2_n } -> b1rec1max1 -> { bH bmax_1 am_1_n }
{ b1 bmax_2 am_1_2 bm_2_n } -> b1rec2max2 -> { bH bmax_2 am_1_n }
{ b1 bmax_2 bleft_0 am_1_1 bm_2_n } -> b1rec1max2left0 -> { b2 bmax_2 bleft_1 am_1_n bm_2_1 }
{ b1 bmax_1 bleft_0 am_1_2 bm_2_n } -> b1rec2max1left0 -> { b2 bmax_1 bleft_2 am_1_n bm_2_2 }
{ b1 bmax_2 bleft_1 am_1_1 bm_2_n } -> b1rec1max2left1 -> { b2 bmax_2 bleft_1 am_1_n bm_2_1 }
{ b1 bmax_1 bleft_1 am_1_2 bm_2_n } -> b1rec2max1left1 -> { b2 bmax_1 bleft_2 am_1_n bm_2_2 }
{ b1 bmax_2 bleft_2 am_1_1 bm_2_n } -> b1rec1max2left2 -> { b2 bmax_2 bleft_1 am_1_n bm_2_1 }
{ b1 bmax_1 bleft_2 am_1_2 bm_2_n } -> b1rec2max1left2 -> { b2 bmax_1 bleft_2 am_1_n bm_2_2 }
{ b2 bleft_0 am_2_1 } -> b2rec1left0 -> { bP bleft_0 am_2_n }
{ b2 bleft_0 am_2_2 } -> b2rec2left0 -> { bP bleft_0 am_2_n }
{ b2 bleft_1 am_2_1 } -> b2rec1left1 -> { bP bleft_1 am_2_n }
{ b2 bleft_1 am_2_2 } -> b2rec2left1 -> { bP bleft_1 am_2_n }
{ b2 bleft_2 am_2_2 } -> b2rec2left2 -> { bP bleft_2 am_2_n }
{ b2 bmax_1 bleft_2 am_2_2 bm_1_n } -> b2rec1max1left2 -> { b1 bmax_2 bleft_2 am_1_n bm_1_1 }
{ b2 bmax_2 bleft_2 am_2_1 } -> b2rec1max2left2 -> { bP bmax_2 bleft_2 am_2_n }
{ bP am_1_1 bm_1_n } -> bPrec1_1 -> { bP am_1_n bm_1_1 }
{ bP am_1_2 bm_1_n } -> bPrec1_2 -> { bP am_1_n bm_1_2 }
{ bP am_2_1 bm_2_n } -> bPrec2_1 -> { bP am_1_n bm_2_1 }
{ bP am_2_2 bm_2_n } -> bPrec2_2 -> { bP am_1_n bm_2_2 }
{ aH bP } -> aDone -> { aD bD }
{ aP bH } -> bDone -> { aD bD }
{ aD amax_1 aleft_0 } -> aDmax1left0 -> { a0 amax_1 aleft_0 }
{ aD amax_2 aleft_0 } -> aDmax2left0 -> { a0 amax_1 aleft_0 }
{ aD amax_1 aleft_1 } -> aDmax1left1 -> { a0 amax_1 aleft_0 }
{ aD amax_2 aleft_1 } -> aDmax2left1 -> { a0 amax_1 aleft_0 }
{ aD amax_1 aleft_2 } -> aDmax1left2 -> { a0 amax_1 aleft_0 }
{ aD amax_2 aleft_2 } -> aDmax2left2 -> { a0 amax_1 aleft_0 }
{ bD bmax_1 bleft_0 } -> bDmax1left0 -> { b0 bmax_1 bleft_0 }
{ bD bmax_2 bleft_0 } -> bDmax2left0 -> { b0 bmax_1 bleft_0 }
{ bD bmax_1 bleft_1 } -> bDmax1left1 -> { b0 bmax_1 bleft_0 }
{ bD bmax_2 bleft_1 } -> bDmax2left1 -> { b0 bmax_1 bleft_0 }
{ bD bmax_1 bleft_2 } -> bDmax1left2 -> { b0 bmax_1 bleft_0 }
{ bD bmax_2 bleft_2 } -> bDmax2left2 -> { b0 bmax_1 bleft_0 }
{ s1a0 s1max1 s1m1_n } -> s1a0send1 -> { s1a1 s1max1 s1m1_1 }
{ s1a0 s1max2 s1m1_n } -> s1a0send2 -> { s1a1 s1max2 s1m1_2 }
{ s1a1 s1max1 s2m1_1 } -> s1a1rec1max1 -> { s1aH s1max1 s2m1_n }
{ s1a1 s1max2 s1left0 s2m1_1 s1m2_n } -> s1a1rec1max2left0 -> { s1a2 s1max2 s1left1 s2m1_n s1m2_1 }
{ s1a1 s1max2 s1left1 s2m1_1 s1m2_n } -> s1a1rec1max2left1 -> { s1a2 s1max2 s1left1 s2m1_n s1m2_1 }
{ s1a1 s1max2 s1left2 s2m1_1 s1m2_n } -> s1a1rec1max2left2 -> { s1a2 s1max2 s1left1 s2m1_n s1m2_1 }
{ s1a1 s1max1 s1left0 s2m1_2 s1m2_n } -> s1a1rec2max1left0 -> { s1a2 s1max1 s1left2 s2m1_n s1m2_2 }
{ s1a1 s1max1 s1left1 s2m1_2 s1m2_n } -> s1a1rec2max1left1 -> { s1a2 s1max1 s1left2 s2m1_n s1m2_2 }
{ s1a1 s1max1 s1left2 s2m1_2 s1m2_n } -> s1a1rec2max1left2 -> { s1a2 s1max1 s1left2 s2m1_n s1m2_2 }
{ s1a1 s1max2 s2m1_2 } -> s1a1rec2max2 -> { s1aH s1max2 s2m1_n }
{ s1a2 s1left0 s2m2_1 } -> s1a2rec1left0 -> { s1aP s1left0 s2m2_n }
{ s1a2 s1left1 s2m2_1 } -> s1a2rec1left1 -> { s1aP s1left1 s2m2_n }
{ s1a2 s1max1 s1left2 s2m2_1 s1m1_n } -> s1a2rec1max1left2 -> { s1a1 s1max2 s1left2 s2m2_n s1m1_2 }
{ s1a2 s1max2 s1left2 s2m2_1 } -> s1a2rec1max2left2 -> { s1aP s1max2 s1left2 s2m2_n }
{ s1a2 s1left0 s2m2_2 } -> s1a2rec2left0 -> { s1aP s1left0 s2m2_n }
{ s1a2 s1left1 s2m2_2 } -> s1a2rec2left1 -> { s1aP s1left1 s2m2_n }
{ s1a2 s1left2 s2m2_2 } -> s1a2rec2left2 -> { s1aP s1left2 s2m2_n }
{ s1aP s2m1_1 s1m1_n } -> s1aPrec1_1 -> { s1aP s2m1_n s1m1_1 }
{ s1aP s2m2_1 s1m2_n } -> s1aPrec2_1 -> { s1aP s2m2_n s1m2_1 }
{ s1aP s2m1_2 s1m1_n } -> s1aPrec1_2 -> { s1aP s2m1_n s1m1_2 }
{ s1aP s2m2_2 s1m2_n } -> s1aPrec2_2 -> { s1aP s2m2_n s1m2_2 }
{ s1aD s1max1 s1left0 } -> s1aDmax1left0 -> { s1a0 s1max1 s1left0 }
{ s1aD s1max1 s1left1 } -> s1aDmax1left1 -> { s1a0 s1max1 s1left0 }
{ s1aD s1max1 s1left2 } -> s1aDmax1left2 -> { s1a0 s1max1 s1left0 }
{ s1aD s1max2 s1left0 } -> s1aDmax2left0 -> { s1a0 s1max1 s1left0 }
{ s1aD s1max2 s1left1 } -> s1aDmax2left1 -> { s1a0 s1max1 s1left0 }
{ s1aD s1max2 s1left2 } -> s1aDmax2left2 -> { s1a0 s1max1 s1left0 }
{ s2a0 s2max1 s2m1_n } -> s2a0send1 -> { s2a1 s2max1 s2m1_1 }
{ s2a0 s2max2 s2m1_n } -> s2a0send2 -> { s2a1 s2max2 s2m1_2 }
{ s2a1 s2max1 s1m1_1 } -> s2a1rec1max1 -> { s2aH s2max1 s1m1_n }
{ s2a1 s2max2 s2left0 s1m1_1 s2m2_n } -> s2a1rec1max2left0 -> { s2a2 s2max2 s2left1 s1m1_n s2m2_1 }
{ s2a1 s2max2 s2left1 s1m1_1 s2m2_n } -> s2a1rec1max2left1 -> { s2a2 s2max2 s2left1 s1m1_n s2m2_1 }
{ s2a1 s2max2 s2left2 s1m1_1 s2m2_n } -> s2a1rec1max2left2 -> { s2a2 s2max2 s2left1 s1m1_n s2m2_1 }
{ s2a1 s2max1 s2left0 s1m1_2 s2m2_n } -> s2a1rec2max1left0 -> { s2a2 s2max1 s2left2 s1m1_n s2m2_2 }
{ s2a1 s2max1 s2left1 s1m1_2 s2m2_n } -> s2a1rec2max1left1 -> { s2a2 s2max1 s2left2 s1m1_n s2m2_2 }
{ s2a1 s2max1 s2left2 s1m1_2 s2m2_n } -> s2a1rec2max1left2 -> { s2a2 s2max1 s2left2 s1m1_n s2m2_2 }
{ s2a1 s2max2 s1m1_2 } -> s2a1rec2max2 -> { s2aH s2max2 s1m1_n }
{ s2a2 s2left0 s1m2_1 } -> s2a2rec1left0 -> { s2aP s2left0 s1m2_n }
{ s2a2 s2left1 s1m2_1 } -> s2a2rec1left1 -> { s2aP s2left1 s1m2_n }
{ s2a2 s2max1 s2left2 s1m2_1 s2m1_n } -> s2a2rec1max1left2 -> { s2a1 s2max2 s2left2 s1m2_n s2m1_2 }
{ s2a2 s2max2 s2left2 s1m2_1 } -> s2a2rec1max2left2 -> { s2aP s2max2 s2left2 s1m2_n }
{ s2a2 s2left0 s1m2_2 } -> s2a2rec2left0 -> { s2aP s2left0 s1m2_n }
{ s2a2 s2left1 s1m2_2 } -> s2a2rec2left1 -> { s2aP s2left1 s1m2_n }
{ s2a2 s2left2 s1m2_2 } -> s2a2rec2left2 -> { s2aP s2left2 s1m2_n }
{ s2aP s1m1_1 s2m1_n } -> s2aPrec1_1 -> { s2aP s1m1_n s2m1_1 }
{ s2aP s1m2_1 s2m2_n } -> s2aPrec2_1 -> { s2aP s1m2_n s2m2_1 }
{ s2aP s1m1_2 s2m1_n } -> s2aPrec1_2 -> { s2aP s1m1_n s2m1_2 }
{ s2aP s1m2_2 s2m2_n } -> s2aPrec2_2 -> { s2aP s1m2_n s2m2_2 }
{ s2aD s2max1 s2left0 } -> s2aDmax1left0 -> { s2a0 s2max2 s2left0 }
{ s2aD s2max1 s2left1 } -> s2aDmax1left1 -> { s2a0 s2max2 s2left0 }
{ s2aD s2max1 s2left2 } -> s2aDmax1left2 -> { s2a0 s2max2 s2left0 }
{ s2aD s2max2 s2left0 } -> s2aDmax2left0 -> { s2a0 s2max2 s2left0 }
{ s2aD s2max2 s2left1 } -> s2aDmax2left1 -> { s2a0 s2max2 s2left0 }
{ s2aD s2max2 s2left2 } -> s2aDmax2left2 -> { s2a0 s2max2 s2left0 }
{ s1aH s2aP } -> s1done -> { s1aD s2aD }
{ s1aP s2aH } -> s2done -> { s1aD s2aD }
}
initial {
s1a0 s1max1 s1left0 s1m1_n s1m2_n
s2a0 s2max2 s2left0 s2m1_n s2m2_n
}
initial { a0 aleft_0 amax_1 am_1_n am_2_n b0 bleft_0 bmax_2 bm_1_n bm_2_n }
}
safety property "passive" {
aP >= 1 && bP >= 1
}
safety property "halt" {
aH >= 1 && bH >= 1
s1aP >= 1 && s2aP >= 1
}
liveness property {
//(aPrec1_2 + bPrec1_2 <= 1) &&
//(aPrec1_1 + bPrec1_1 <= 1) &&
aDone = 0 && bDone = 0
s1done = 0 && s2done = 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