Commit 1c1d70bd authored by Philipp Meyer's avatar Philipp Meyer

Remove petri net examples; add population protocol examples

parent ad3b64e6
population protocol "Broadcast Protocol" {
states { true false}
transitions { x_false_true }
arcs {
{ false, true } -> x_false_true -> { true, true }
}
initial { true false }
yes { true }
no { false }
}
/*
//flag[] is boolean array; and turn is an integer
flag[1] = false
flag[2] = false
turn = 1 // or 2
P1:
p1:flag[1] = true;
p2:while (flag[2] == true) {
p3: if (turn ≠ 1) {
p4: flag[1] = false;
p5: while (turn ≠ 1) {
// busy wait
}
p6: flag[1] = true;
}
}
p7:// critical section
...
turn = 2;
p8:flag[1] = false;
// remainder section
P2:
q1:flag[2] = true;
q2:while (flag[1] == true) {
q3: if (turn ≠ 2) {
q4: flag[2] = false;
q5: while (turn ≠ 2) {
// busy wait
}
q6: flag[2] = true;
}
}
q7:// critical section
...
turn = 1;
q8:flag[2] = false;
// remainder section
*/
petri net "Dekker's algorithm" {
places {
p1 p2 p3 p4 p5 p6 p7 p8
q1 q2 q3 q4 q5 q6 q7 q8
flag1t flag1f flag2t flag2f turn1 turn2
}
transitions {
u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12
v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12
}
arcs {
{ p1 flag1f } -> u1 -> { p2 flag1t }
{ p2 flag2f } -> u2 -> { p7 flag2f }
{ p2 flag2t } -> u3 -> { p3 flag2t }
{ p3 turn1 } -> u4 -> { p2 turn1 }
{ p3 turn2 } -> u5 -> { p4 turn2 }
{ p4 flag1t } -> u6 -> { p5 flag1f }
{ p5 turn1 } -> u7 -> { p6 turn1 }
{ p5 turn2 } -> u8 -> { p5 turn2 }
{ p6 flag1f } -> u9 -> { p2 flag1t }
{ p7 turn1 } -> u10 -> { p8 turn2 }
{ p7 turn2 } -> u11 -> { p8 turn2 }
{ p8 flag1t } -> u12 -> { p1 flag1f }
{ q1 flag2f } -> v1 -> { q2 flag2t }
{ q2 flag1f } -> v2 -> { q7 flag1f }
{ q2 flag1t } -> v3 -> { q3 flag1t }
{ q3 turn1 } -> v4 -> { q4 turn1 }
{ q3 turn2 } -> v5 -> { q2 turn2 }
{ q4 flag2t } -> v6 -> { q5 flag2f }
{ q5 turn1 } -> v7 -> { q5 turn1 }
{ q5 turn2 } -> v8 -> { q6 turn2 }
{ q6 flag2f } -> v9 -> { q2 flag2t }
{ q7 turn1 } -> v10 -> { q8 turn1 }
{ q7 turn2 } -> v11 -> { q8 turn1 }
{ q8 flag2t } -> v12 -> { q1 flag2f }
}
initial {
p1 q1 flag1f flag2f turn1
}
}
liveness property "fairness for first process" {
u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 > 0 &&
v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 > 0 &&
u2 = 0
}
liveness property "fairness for second process" {
u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 > 0 &&
v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 > 0 &&
v2 = 0
}
safety property "mutual exclusion" {
p7 >= 1 && q7 >= 1
}
petri net "Free Choice" {
places {
s r
}
transitions {
t u
}
arcs {
s -> t
r -> t
s -> u
r -> u
}
initial {
s r
}
}
/*
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
}
liveness property "h dispatched" {
dh = 0
}
PLACE 'sigma,'m1,'m2,x,not_x,scheduler,h,g,pending_h,pending_g,'x,'not_x,'scheduler,'h,'g,'pending_h,'pending_g,dg_out,dh_out;
MARKING 'm1:1,'pending_h:1,'scheduler:1,'x:1,pending_h:1,scheduler:1,x:1;
TRANSITION 'switch
CONSUME 'm1:1;
PRODUCE 'm2:1;
TRANSITION dh
CONSUME 'scheduler:1,'pending_h:1,scheduler:1,pending_h:1,'m1:1;
PRODUCE 'h:1,h:1,'m1:1;
TRANSITION 'dh
CONSUME 'scheduler:1,'pending_h:1,'m2:1;
PRODUCE 'h:1,'sigma:1,'m2:1,dh_out:1;
TRANSITION dg
CONSUME 'scheduler:1,'pending_g:1,scheduler:1,pending_g:1,'m1:1;
PRODUCE 'g:1,g:1,'m1:1;
TRANSITION 'dg
CONSUME 'scheduler:1,'pending_g:1,'m2:1;
PRODUCE 'g:1,'sigma:1,'m2:1,dg_out:1;
TRANSITION ht
CONSUME 'h:1,'x:1,h:1,x:1,'m1:1;
PRODUCE 'x:1,'pending_h:1,'pending_g:1,'scheduler:1,x:1,pending_h:1,pending_g:1,scheduler:1,'m1:1;
TRANSITION 'ht
CONSUME 'h:1,'x:1,'m2:1;
PRODUCE 'x:1,'pending_h:1,'pending_g:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION hf
CONSUME 'h:1,'not_x:1,h:1,not_x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'hf
CONSUME 'h:1,'not_x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION gt
CONSUME 'g:1,'x:1,g:1,x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'gt
CONSUME 'g:1,'x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
TRANSITION gf
CONSUME 'g:1,'not_x:1,g:1,not_x:1,'m1:1;
PRODUCE 'not_x:1,'scheduler:1,not_x:1,scheduler:1,'m1:1;
TRANSITION 'gf
CONSUME 'g:1,'not_x:1,'m2:1;
PRODUCE 'not_x:1,'scheduler:1,'sigma:1,'m2:1;
PROBLEM termination_by_reachability:
GOAL REACHABILITY;
FILE h_fairly_terminates.pnet.terminating TYPE LOLA;
INITIAL 'm1:1,'pending_h:1,'scheduler:1,'x:1,pending_h:1,scheduler:1,x:1;
FINAL COVER;
CONSTRAINTS 'sigma>1,dh_out>1,dg_out>1,'x+-1x>0,'not_x+-1not_x>0,'scheduler+-1scheduler>0,'h+-1h>0,'g+-1g>0,'pending_h+-1pending_h>0,'pending_g+-1pending_g>0;
EF ('sigma >= 1 AND dh_out >= 1 AND dg_out >= 1 AND ('x - x) >= 0 AND ('not_x - not_x) >= 0 AND ('scheduler - scheduler) >= 0 AND ('h - h) >= 0 AND ('g - g) >= 0 AND ('pending_h - pending_h) >= 0 AND ('pending_g - pending_g) >= 0)
petri net "asynchronous program" {
places {
// State
x not_x x_ not_x_
// Scheduler
scheduler scheduler_
// Handlers
h g h_ g_
// Pending instances
pending_h pending_g pending_h_ pending_g_
m1 m2 dh_out dg_out
}
transitions {
dh dg ht hf gt gf
dh_ dg_ ht_ hf_ gt_ gf_
switch
}
arcs {
// Dispatch h
{ scheduler, pending_h, scheduler_, pending_h_, m1 } -> dh -> { h, h_, m1 }
{ scheduler_, pending_h_, m2 } -> dh_ -> { h_, m2, dh_out }
// Dispatch g
{ scheduler, pending_g, scheduler_, pending_g_, m1 } -> dg -> { g, g_, m1 }
{ scheduler_, pending_g_, m2 } -> dg_ -> { g_, m2, dg_out }
// Exit h if x == true
{ h, x, h_, x_, m1 } -> ht -> { x, pending_h, pending_g, scheduler, x_, pending_h_, pending_g_, scheduler_, m1 }
{ h_, x_, m2 } -> ht_ -> { x_, pending_h_, pending_g_, scheduler_, m2 }
// Exit h if x == false
{ h, not_x, h_, not_x_, m1 } -> hf -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ h_, not_x_, m2 } -> hf_ -> { not_x_, scheduler_, m2 }
// Exit g if x == true
{ g, x, g_, x_, m1 } -> gt -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ g_, x_, m2 } -> gt_ -> { not_x_, scheduler_, m2 }
// Exit g if x == false
{ g, not_x, g_, not_x_, m1 } -> gf -> { not_x, scheduler, not_x_, scheduler_, m1 }
{ g_, not_x_, m2 } -> gf_ -> { not_x_, scheduler_, m2 }
m1 -> switch -> m2
}
initial {
// Initially, x is true, there's one pending instance of h(),
// and the scheduler has control.
x pending_h scheduler
x_ pending_h_ scheduler_
m1
}
}
safety property "terminating" {
dh_out >= 1 && dg_out >= 1 &&
x_ >= x && not_x_ >= not_x &&
scheduler_ >= scheduler &&
h_ >= h && g_ >= g &&
pending_h_ >= pending_h && pending_g_ >= pending_g
}
PLACE
p1, p2, p3, b1, nb1,
q1, q2, q3, q4, q5, b2, nb2;
MARKING
p1, q1, nb1, nb2;
TRANSITION s1
CONSUME p1, nb1;
PRODUCE p2, b1;
TRANSITION s2
CONSUME p2, b2;
PRODUCE p2, b2;
TRANSITION s3
CONSUME p2, nb2;
PRODUCE p3, nb2;
TRANSITION s4
CONSUME p3, b1;
PRODUCE p1, nb1;
TRANSITION t1
CONSUME q1, nb2;
PRODUCE q2, b2;
TRANSITION t2
CONSUME q2, b1;
PRODUCE q3, b1;
TRANSITION t3
CONSUME q3, b2;
PRODUCE q4, nb2;
TRANSITION t4
CONSUME q4, nb1;
PRODUCE q1, nb1;
TRANSITION t5
CONSUME q4, b1;
PRODUCE q4, b1;
TRANSITION t6
CONSUME q2, nb1;
PRODUCE q5, nb1;
TRANSITION t7
CONSUME q5, b2;
PRODUCE q1, nb2;
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, nb2 } -> s2 -> { p3, nb2 }
{ p2, b2 } -> s3 -> { p2, b2 }
{ 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 + 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" {
s1 + s2 + s3 + s4 > 0 && t6 = 0 && t1 + t2 + t3 + t4 + t5 + t6 + t7 > 0
}
safety property "mutual exclusion" {
p3 >= 1 && q5 >= 1
}
place p1 init 1;
place p2;
place p3;
place b1;
place nb1 init 1;
place q1 init 1;
place q2;
place q3;
place q4;
place q5;
place b2;
place nb2 init 1;
trans s1 in p1 nb1 out p2 b1;
trans s2 in p2 b2 out p2 b2;
trans s3 in p2 nb2 out p3 nb2;
trans s4 in p3 b1 out p1 nb1;
trans t1 in q1 nb2 out q2 b2;
trans t2 in q2 b1 out q3 b1;
trans t3 in q3 b2 out q4 nb2;
trans t4 in q4 nb1 out q1 nb1;
trans t5 in q4 b1 out q4 b1;
trans t6 in q2 nb1 out q5 nb1;
trans t7 in q5 b2 out q1 nb2;
petri net "Lamport's algorithm" {
places {
p1 p2 p3 b1 nb1
q1 q2 q3 q4 q5 nb2
}
transitions {
s1 s2 s3
t1 t2 t3 t4 t5 t6
}
arcs {
{ p1, nb1 } -> s1 -> { p2, b1 }
{ p2, nb2 } -> s2 -> { p3, nb2 }
{ p3, b1 } -> s3 -> { p1, nb1 }
{ q1, nb2 } -> t1 -> { q2, }
{ q2, b1 } -> t2 -> { q3, b1 }
{ q3, } -> t3 -> { q4, nb2 }
{ q4, nb1 } -> t4 -> { q1, nb1 }
{ q2, nb1 } -> t5 -> { q5, nb1 }
{ q5, } -> t6 -> { q1, nb2 }
}
initial {
p1 q1 nb1 nb2
}
}
safety property "mutual exclusion" {
p3 >= 1 && q5 >= 1
}
petri net "leader election 2" {
places {
s1 s1m1 s1m2
s2 s2m1 s2m2
lead
}
transitions {
s1send1 s1pass2 s1accept1
s2send2 s2discard1 s2accept2
newleader
}
arcs {
s1 -> s1send1 -> s1m1
s2 -> s2send2 -> s2m2
s1m1 -> s2discard1
s1m2 -> s2accept2 -> lead
s2m1 -> s1accept1 -> lead
s2m2 -> s1pass2 -> s1m2
lead -> newleader -> { s1 s2 }
}
initial { s1 s2 }
}
safety property {
lead >= 2
}
liveness property {
newleader = 0
}
petri net "improved leader election 2" {
places {
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 {
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 {
{ 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
}
}
safety property "passive" {
s1aP >= 1 && s2aP >= 1
}
liveness property {
s1done = 0 && s2done = 0
}
population protocol "Majority Protocol" {
states { good bad neutral mildlybad}
transitions { x_good_bad x_good_mildlybad x_bad_neutral x_neutral_mildlybad }
arcs {
{ good, bad } -> x_good_bad -> { neutral, mildlybad }
{ good, mildlybad } -> x_good_mildlybad -> { good, neutral }
{ bad, neutral } -> x_bad_neutral -> { bad, mildlybad }
{ neutral, mildlybad } -> x_neutral_mildlybad -> { mildlybad, mildlybad }
}
initial { good bad }
yes { good neutral }
no { bad mildlybad }
}
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" {
u1 + u2 + u3 + u4 + u5 + u6 + u7 > 0 && u4 + u5 = 0 &&
v1 + v2 + v3 + v4 + v5 + v6 + v7 > 0
}
liveness property "fairness for second process" {
u1 + u2 + u3 + u4 + u5 + u6 + u7 > 0 &&
v1 + v2 + v3 + v4 + v5 + v6 + v7 > 0 && v4 + v5 = 0
}
safety property "mutual exclusion" {