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

Commit 527ea2e8 authored by Philipp Meyer's avatar Philipp Meyer

Added more variants of leader election and snapshot examples

parent 5388fd54
petri net "leader election 2" {
places {
s1 s1x1 s1x2
s2 s2x1 s2x2
s1 s1m1 s1m2
s2 s2m1 s2m2
lead
}
transitions {
......@@ -10,12 +10,12 @@ petri net "leader election 2" {
newleader
}
arcs {
s1 -> s1send1 -> s1x1
s2 -> s2send2 -> s2x2
s1x1 -> s2discard1
s1x2 -> s2accept2 -> lead
s2x1 -> s1accept1 -> lead
s2x2 -> s1pass2 -> s1x2
s1 -> s1send1 -> s1m1
s2 -> s2send2 -> s2m2
s1m1 -> s2discard1
s1m2 -> s2accept2 -> lead
s2m1 -> s1accept1 -> lead
s2m2 -> s1pass2 -> s1m2
lead -> newleader -> { s1 s2 }
}
initial { s1 s2 }
......
petri net "leader election nlogn 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
}
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
}
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 }
}
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
}
liveness property {
//(aPrec1_2 + bPrec1_2 <= 1) &&
//(aPrec1_1 + bPrec1_1 <= 1) &&
aDone = 0 && bDone = 0
}
petri net "snapshot 2" {
places {
white1 red1 sent1 notsent1 sample1 nosample1
white2 red2 sent2 notsent2 sample2 nosample2
}
transitions {
init1 send1white2 send1red2 comm1red // comm1white
init2 send2white1 send2red1 comm2red // comm2white
snapshot nosnapshot1 nosnapshot2
}
arcs {
// white1 -> comm1white -> white1
{ red1, sent1 } -> comm1red -> { red1, sent1 }
{ white1, nosample1 } -> init1 -> { red1, sample1 }
{ red1, notsent1, white2, nosample2 } -> send1white2 -> { red1, sent1, red2, sample2 }
{ red1, notsent1, red2 } -> send1red2 -> { red1, sent1, red2 }
// white2 -> comm2white -> white2
{ red2, sent2 } -> comm2red -> { red2, sent2 }
{ white2, nosample2 } -> init2 -> { red2, sample2 }
{ red2, notsent2, white2, nosample1 } -> send2white1 -> { red2, sent2, red1, sample1 }
{ red2, notsent2, red1 } -> send2red1 -> { red2, sent2, red1 }
{ sample1, sample2, red1, red2, sent1, sent2 } -> snapshot -> { white1, white2, notsent1, notsent2, nosample1, nosample2 }
nosample1 -> nosnapshot1 -> nosample1
nosample2 -> nosnapshot2 -> nosample2
}
initial {
white1 notsent1 nosample1
white2 notsent2 nosample2
}
}
safety property "one sample" {
sample1 > 1 || sample2 > 1
}
liveness property "snapshot taken" {
init1 + send1white2 + send1red2 + comm1red > 0 &&
init2 + send2white1 + send2red1 + comm2red > 0 &&
init1 + send1white2 + send1red2 + comm1red > 0 &&
init2 + send2white1 + send2red1 + comm2red > 0 &&
init1 + send1white2 + send1red2 + comm1red > 0 &&
init2 + send2white1 + send2red1 + comm2red > 0 &&
init1 + send1white2 + send1red2 + comm1red > 0 &&
init2 + send2white1 + send2red1 + comm2red > 0 &&
snapshot + nosnapshot1 + nosnapshot2 > 0 &&
snapshot = 0
}
petri net "snapshot 2 with ltl" {
places {
white1 red1 sent1 notsent1 sample1 nosample1
white2 red2 sent2 notsent2 sample2 nosample2
not_init_fired init_fired
}
transitions {
init1 send1white2 send1red2 comm1white comm1red
init2 send2white1 send2red1 comm2white comm2red
snapshot nosnapshot1 nosnapshot2 nosnapshot3
init1_ send1white2_ send1red2_ comm1white_ comm1red_
init2_ send2white1_ send2red1_ comm2white_ comm2red_
snapshot_ nosnapshot1_ nosnapshot2_ nosnapshot3_
}
arcs {
white1 -> comm1white -> white1
{ red1, sent1 } -> comm1red -> { red1, sent1 }
{ white1, nosample1 } -> init1 -> { red1, sample1 }
{ red1, notsent1, white2, nosample2 } -> send1white2 -> { red1, sent1, red2, sample2 }
{ red1, notsent1, red2 } -> send1red2 -> { red1, sent1, red2 }
white1 -> comm1white_ -> white1
{ red1, sent1 } -> comm1red_ -> { red1, sent1 }
{ white1, nosample1 } -> init1_ -> { red1, sample1 }
{ red1, notsent1, white2, nosample2 } -> send1white2_ -> { red1, sent1, red2, sample2 }
{ red1, notsent1, red2 } -> send1red2_ -> { red1, sent1, red2 }
not_init_fired -> comm1white -> not_init_fired
not_init_fired -> comm1red -> not_init_fired
not_init_fired -> init1 -> init_fired
not_init_fired -> send1white2 -> not_init_fired
not_init_fired -> send1red2 -> not_init_fired
init_fired -> comm1white -> init_fired
init_fired -> comm1red -> init_fired
init_fired -> init1 -> init_fired
init_fired -> send1white2 -> init_fired
init_fired -> send1red2 -> init_fired
white2 -> comm2white -> white2
{ red2, sent2 } -> comm2red -> { red2, sent2 }
{ white2, nosample2 } -> init2 -> { red2, sample2 }
{ red2, notsent2, white2, nosample1 } -> send2white1 -> { red2, sent2, red1, sample1 }
{ red2, notsent2, red1 } -> send2red1 -> { red2, sent2, red1 }
white2 -> comm2white_ -> white2
{ red2, sent2 } -> comm2red_ -> { red2, sent2 }
{ white2, nosample2 } -> init2_ -> { red2, sample2 }
{ red2, notsent2, white2, nosample1 } -> send2white1_ -> { red2, sent2, red1, sample1 }
{ red2, notsent2, red1 } -> send2red1_ -> { red2, sent2, red1 }
not_init_fired -> comm2white -> not_init_fired
not_init_fired -> comm2red -> not_init_fired
not_init_fired -> init2 -> init_fired
not_init_fired -> send2white1 -> not_init_fired
not_init_fired -> send2red1 -> not_init_fired
init_fired -> comm2white_ -> init_fired
init_fired -> comm2red_ -> init_fired
init_fired -> init2_ -> init_fired
init_fired -> send2white1_ -> init_fired
init_fired -> send2red1_ -> init_fired
{ sample1, sample2, red1, red2, sent1, sent2 } -> snapshot -> { white1, white2, notsent1, notsent2, nosample1, nosample2 }
{ sample1, sample2, red1, red2, sent1, sent2 } -> snapshot_ -> { white1, white2, notsent1, notsent2, nosample1, nosample2 }
{ nosample1, sample2 } -> nosnapshot1 -> { nosample1, sample2 }
{ sample1, nosample2 } -> nosnapshot2 -> { sample1, nosample2 }
{ nosample1, nosample2 } -> nosnapshot3 -> { nosample1, nosample2 }
{ nosample1, sample2 } -> nosnapshot1_ -> { nosample1, sample2 }
{ sample1, nosample2 } -> nosnapshot2_ -> { sample1, nosample2 }
{ nosample1, nosample2 } -> nosnapshot3_ -> { nosample1, nosample2 }
not_init_fired -> snapshot -> not_init_fired
not_init_fired -> nosnapshot1 -> not_init_fired
not_init_fired -> nosnapshot2 -> not_init_fired
not_init_fired -> nosnapshot3 -> not_init_fired
init_fired -> snapshot_ -> not_init_fired
init_fired -> nosnapshot1_ -> init_fired
init_fired -> nosnapshot2_ -> init_fired
init_fired -> nosnapshot3_ -> init_fired
}
initial {
not_init_fired
white1 notsent1 nosample1
white2 notsent2 nosample2
}
}
/*safety property "places 1" {
sent1 + white2 > 1
}
safety property "places 2" {
sent2 + white1 > 1
}
liveness property {
(init1 > 0 || init2 > 0) && snapshot > 0
}*/
liveness property {
init1 + send1white2 + send1red2 + comm1white + comm1red +
init1_ + send1white2_ + send1red2_ + comm1white_ + comm1red_ > 0 &&
init2 + send2white1 + send2red1 + comm2white + comm2red +
init2_ + send2white1_ + send2red1_ + comm2white_ + comm2red_ > 0 &&
snapshot + nosnapshot1 + nosnapshot2 + nosnapshot3 +
snapshot_ + nosnapshot1_ + nosnapshot2_ + nosnapshot3_ > 0 &&
init1 = 0 && send1white2 = 0 && send1red2 = 0 && comm1white = 0 && comm1red = 0 &&
init2 = 0 && send2white1 = 0 && send2red1 = 0 && comm2white = 0 && comm2red = 0 &&
snapshot = 0 && nosnapshot1 = 0 && nosnapshot2 = 0 && nosnapshot3 = 0 &&
comm1white_ = 0 && comm2white_ = 0
// snapshot_ = 0 && comm1white_ = 1 && comm2white_ = 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