Commit 9f06fedb by Philipp Meyer

### Changed and added more mutual exclusion examples

parent 196fe98a
 /* //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 }
 ... ... @@ -26,7 +26,7 @@ petri net "Lamport's algorithm" { } } liveness property "fairness for first process" { s1 + s2 > 0 && s3 = 0 && t6 >= 1 s1 + s2 > 0 && s3 = 0 && t1 + t2 + t3 + t4 + t5 + t6 + t7 > 0 } liveness property "fairness for second process" { t1 + t2 + t3 + t4 > 0 && t6 = 0 && s3 >= 1 ... ...
 ... ... @@ -37,10 +37,12 @@ petri net "Peterson's algorithm" { } } liveness property "fairness for first process" { u6 > 0 && u4 + u5 = 0 && v4 + v5 > 0 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" { v6 > 0 && v4 + v5 = 0 && u4 + u5 > 0 u1 + u2 + u3 + u4 + u5 + u6 + u7 > 0 && v1 + v2 + v3 + v4 + v5 + v6 + v7 > 0 && v4 + v5 = 0 } safety property "mutual exclusion" { p4 >= 1 && q4 >= 1 ... ...
 /* #Entry protocol p1: flag[self] ← 1 #Standing outside waiting room p2: await(all flag[1..N] ∈ {0, 1, 2}) #Wait for open door p3: flag[self] ← 3 #Standing in doorway p4: if any flag[1..N] = 1: #Another process is waiting to enter p5: flag[self] ← 2 #Waiting for other processes to enter p6: await(any flag[1..N] = 4) #Wait for a process to enter and close the door p7: flag[self] ← 4 #The door is closed p8: await(all flag[1..self-1] ∈ {0, 1}) #Wait for everyone of lower ID to finish exit protocol #Critical section #... #Exit protocol p9: await(all flag[self+1..N] ∈ {0, 1, 4}) #Ensure everyone in the waiting room has #realized that the door is supposed to be closed p10:flag[self] ← 0 #Leave. Reopen door if nobody is still in the waiting room */ petri net "Szymanski's algorithm" { places { p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 flag1v0 flag1v1 flag1v2 flag1v3 flag1v4 flag2v0 flag2v1 flag2v2 flag2v3 flag2v4 } transitions { u1 u2 u3 u4 u7 u8 u9 u10 u11 u12 u13 u18 u19 u20 u21 u26 u27 u30 u31 v1 v2 v3 v4 v7 v8 v9 v10 v11 v12 v13 v18 v19 v20 v21 v22 v26 v31 } arcs { { p1 flag1v0 } -> u1 -> { p2 flag1v1 } { p2 flag2v0 } -> u2 -> { p3 flag2v0 } { p2 flag2v1 } -> u3 -> { p3 flag2v1 } { p2 flag2v2 } -> u4 -> { p3 flag2v2 } { p3 flag1v1 } -> u7 -> { p4 flag1v3 } { p4 flag2v0 } -> u8 -> { p7 flag2v0 } { p4 flag2v1 } -> u9 -> { p5 flag2v1 } { p4 flag2v2 } -> u10 -> { p7 flag2v2 } { p4 flag2v3 } -> u11 -> { p7 flag2v3 } { p4 flag2v4 } -> u12 -> { p7 flag2v4 } { p5 flag1v3 } -> u13 -> { p6 flag1v2 } { p6 flag2v4 } -> u18 -> { p7 flag2v4 } { p7 flag1v2 } -> u19 -> { p8 flag1v4 } { p7 flag1v3 } -> u20 -> { p8 flag1v4 } { p8 } -> u21 -> { p9 } { p9 flag2v0 } -> u26 -> { p10 flag2v0 } { p9 flag2v1 } -> u27 -> { p10 flag2v1 } { p9 flag2v4 } -> u30 -> { p10 flag2v4 } { p10 flag1v4 } -> u31 -> { p1 flag1v0 } { q1 flag2v0 } -> v1 -> { q2 flag2v1 } { q2 flag1v0 } -> v2 -> { q3 flag1v0 } { q2 flag1v1 } -> v3 -> { q3 flag1v1 } { q2 flag1v2 } -> v4 -> { q3 flag1v2 } { q3 flag2v1 } -> v7 -> { q4 flag2v3 } { q4 flag1v0 } -> v8 -> { q7 flag1v0 } { q4 flag1v1 } -> v9 -> { q5 flag1v1 } { q4 flag1v2 } -> v10 -> { q7 flag1v2 } { q4 flag1v3 } -> v11 -> { q7 flag1v3 } { q4 flag1v4 } -> v12 -> { q7 flag1v4 } { q5 flag2v3 } -> v13 -> { q6 flag2v2 } { q6 flag1v4 } -> v18 -> { q7 flag1v4 } { q7 flag2v2 } -> v19 -> { q8 flag2v4 } { q7 flag2v3 } -> v20 -> { q8 flag2v4 } { q8 flag1v0 } -> v21 -> { q9 flag1v0 } { q8 flag1v1 } -> v22 -> { q9 flag1v1 } { q9 } -> v26 -> { q10 } { q10 flag2v4 } -> v31 -> { q1 flag2v0 } } initial { p1 q1 flag1v0 flag2v0 } } liveness property "fairness for first process" { u1 + u2 + u3 + u4 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u18 + u19 + u20 + u21 + u26 + u27 + u30 + u31 > 0 && v1 + v2 + v3 + v4 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v18 + v19 + v20 + v21 + v22 + v26 + v31 > 0 && u21 = 0 } liveness property "fairness for second process" { u1 + u2 + u3 + u4 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u18 + u19 + u20 + u21 + u26 + u27 + u30 + u31 > 0 && v1 + v2 + v3 + v4 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v18 + v19 + v20 + v21 + v22 + v26 + v31 > 0 && v21 + v22 = 0 } safety property "mutual exclusion" { p9 >= 1 && q9 >= 1 }
 /* #Entry protocol p1: flag[self] ← 1 #Standing outside waiting room p2: await(all flag[1..N] ∈ {0, 1, 2}) #Wait for open door p3: flag[self] ← 3 #Standing in doorway p4: if any flag[1..N] = 1: #Another process is waiting to enter p5: flag[self] ← 2 #Waiting for other processes to enter p6: await(any flag[1..N] = 4) #Wait for a process to enter and close the door p7: flag[self] ← 4 #The door is closed p8: await(all flag[1..self-1] ∈ {0, 1}) #Wait for everyone of lower ID to finish exit protocol #Critical section #... #Exit protocol p9: await(all flag[self+1..N] ∈ {0, 1, 4}) #Ensure everyone in the waiting room has #realized that the door is supposed to be closed p10:flag[self] ← 0 #Leave. Reopen door if nobody is still in the waiting room */ petri net "Szymanski's algorithm" { places { p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 flag1v0 flag1v1 flag1v2 flag1v3 flag1v4 flag2v0 flag2v1 flag2v2 flag2v3 flag2v4 } transitions { u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 u17 u18 u19 u20 u21 u22 u23 u24 u25 u26 u27 u28 u29 u30 u31 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 } arcs { { p1 flag1v0 } -> u1 -> { p2 flag1v1 } { p2 flag2v0 } -> u2 -> { p3 flag2v0 } { p2 flag2v1 } -> u3 -> { p3 flag2v1 } { p2 flag2v2 } -> u4 -> { p3 flag2v2 } { p2 flag2v3 } -> u5 -> { p2 flag2v3 } { p2 flag2v4 } -> u6 -> { p2 flag2v4 } { p3 flag1v1 } -> u7 -> { p4 flag1v3 } { p4 flag2v0 } -> u8 -> { p7 flag2v0 } { p4 flag2v1 } -> u9 -> { p5 flag2v1 } { p4 flag2v2 } -> u10 -> { p7 flag2v2 } { p4 flag2v3 } -> u11 -> { p7 flag2v3 } { p4 flag2v4 } -> u12 -> { p7 flag2v4 } { p5 flag1v3 } -> u13 -> { p6 flag1v2 } { p6 flag2v0 } -> u14 -> { p6 flag2v0 } { p6 flag2v1 } -> u15 -> { p6 flag2v1 } { p6 flag2v2 } -> u16 -> { p6 flag2v2 } { p6 flag2v3 } -> u17 -> { p6 flag2v3 } { p6 flag2v4 } -> u18 -> { p7 flag2v4 } { p7 flag1v2 } -> u19 -> { p8 flag1v4 } { p7 flag1v3 } -> u20 -> { p8 flag1v4 } { p8 flag2v0 } -> u21 -> { p9 flag2v0 } { p8 flag2v1 } -> u22 -> { p9 flag2v1 } { p8 flag2v2 } -> u23 -> { p9 flag2v2 } { p8 flag2v3 } -> u24 -> { p9 flag2v3 } { p8 flag2v4 } -> u25 -> { p9 flag2v4 } { p9 flag2v0 } -> u26 -> { p10 flag2v0 } { p9 flag2v1 } -> u27 -> { p10 flag2v1 } { p9 flag2v2 } -> u28 -> { p9 flag2v2 } { p9 flag2v3 } -> u29 -> { p9 flag2v3 } { p9 flag2v4 } -> u30 -> { p10 flag2v4 } { p10 flag1v4 } -> u31 -> { p1 flag1v0 } { q1 flag2v0 } -> v1 -> { q2 flag2v1 } { q2 flag1v0 } -> v2 -> { q3 flag1v0 } { q2 flag1v1 } -> v3 -> { q3 flag1v1 } { q2 flag1v2 } -> v4 -> { q3 flag1v2 } { q2 flag1v3 } -> v5 -> { q2 flag1v3 } { q2 flag1v4 } -> v6 -> { q2 flag1v4 } { q3 flag2v1 } -> v7 -> { q4 flag2v3 } { q4 flag1v0 } -> v8 -> { q7 flag1v0 } { q4 flag1v1 } -> v9 -> { q5 flag1v1 } { q4 flag1v2 } -> v10 -> { q7 flag1v2 } { q4 flag1v3 } -> v11 -> { q7 flag1v3 } { q4 flag1v4 } -> v12 -> { q7 flag1v4 } { q5 flag2v3 } -> v13 -> { q6 flag2v2 } { q6 flag1v0 } -> v14 -> { q6 flag1v0 } { q6 flag1v1 } -> v15 -> { q6 flag1v1 } { q6 flag1v2 } -> v16 -> { q6 flag1v2 } { q6 flag1v3 } -> v17 -> { q6 flag1v3 } { q6 flag1v4 } -> v18 -> { q7 flag1v4 } { q7 flag2v2 } -> v19 -> { q8 flag2v4 } { q7 flag2v3 } -> v20 -> { q8 flag2v4 } { q8 flag1v0 } -> v21 -> { q9 flag1v0 } { q8 flag1v1 } -> v22 -> { q9 flag1v1 } { q8 flag1v2 } -> v23 -> { q8 flag1v2 } { q8 flag1v3 } -> v24 -> { q8 flag1v3 } { q8 flag1v4 } -> v25 -> { q8 flag1v4 } { q9 flag1v0 } -> v26 -> { q10 flag1v0 } { q9 flag1v1 } -> v27 -> { q10 flag1v1 } { q9 flag1v2 } -> v28 -> { q10 flag1v2 } { q9 flag1v3 } -> v29 -> { q10 flag1v3 } { q9 flag1v4 } -> v30 -> { q10 flag1v4 } { q10 flag2v4 } -> v31 -> { q1 flag2v0 } } initial { p1 q1 flag1v0 flag2v0 } } /* liveness property "fairness for first process" { u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 > 0 && v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 && u21 + u22 + u23 + u24 + u25 = 0 } */ liveness property "fairness for second process" { u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 > 0 && v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 && v21 + v22 = 0 && (u17 = 0 || v16 = 0 || u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 ) && (u17 = 0 || v17 = 0 || u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 ) && (u16 = 0 || v16 = 0 || u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 ) && (u16 = 0 || v17 = 0 || v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 + u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 > 0 ) && (u5 = 0 || v15 = 0 || u1 + u2 + u3 + u4 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 + v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 ) && (u15 = 0 || v5 = 0 || v1 + v2 + v3 + v4 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 + u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u16 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 > 0 ) } /* liveness property "no livelock" { u1 + u2 + u3 + u4 + u5 + u6 + u7 + u8 + u9 + u10 + u11 + u12 + u13 + u14 + u15 + u16 + u17 + u18 + u19 + u20 + u21 + u22 + u23 + u24 + u25 + u26 + u27 + u28 + u29 + u30 + u31 > 0 && v1 + v2 + v3 + v4 + v5 + v6 + v7 + v8 + v9 + v10 + v11 + v12 + v13 + v14 + v15 + v16 + v17 + v18 + v19 + v20 + v21 + v22 + v23 + v24 + v25 + v26 + v27 + v28 + v29 + v30 + v31 > 0 && u1 = 0 && v1 = 0 } */ safety property "mutual exclusion" { p9 >= 1 && q9 >= 1 } safety property "not reachable 1" { flag1v2 >= 1 && flag2v3 >= 1 && q6 >= 1 && p6 >= 1 } safety property "not reachable 2" { flag2v3 >= 1 && flag1v1 >= 1 && q6 >= 1 && p2 >= 1 } safety property "not reachable 3" { flag2v2 >= 1 && flag1v2 >= 1 && p6 >= 1 && q6 >= 1 } safety property "not reachable 4" { flag2v3 >= 1 && flag1v3 >= 1 && p6 >= 1 && q6 >= 1 }
Supports Markdown
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