Commit b7158ad2 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added more test examples

parent a7d87f58
petri net "S-component test" {
places {
s1 s2 s3 s4
}
transitions {
t1 t2 t3
}
arcs {
s1 -> t1 -> s2
s3 -> t1 -> s3
s2 -> t2 -> s1
s4 -> t2 -> s4
s3 -> t3 -> s4
}
initial {
s1 s3
}
}
liveness property "termination" {
true
}
/*
#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 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 } -> u21 -> { p9 }
{ 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 + 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 = 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 + 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
}
/*
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 + 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
}
safety property "IF0" {
!(p1 + q1 = flag1v0 + flag2v0)
}
safety property "IF1" {
!(p2 + p3 + q2 + q3 = flag1v1 + flag2v1)
}
safety property "IF2" {
!(p6 + p7 + q6 + q7 >= flag1v2 + flag2v2)
}
safety property "IF3" {
!(p4 + p5 + p7 + q4 + q5 + q7 >= flag1v3 + flag2v3)
}
safety property "IF4" {
!(p8 + p9 + p10 + q8 + q9 + q10 = flag1v4 + flag2v4)
}
safety property "IF8" {
!(p7 + q7 <= flag1v2 + flag1v3 + flag2v2 + flag2v3)
}
safety property "A0" {
!(!(p7 + p8 + p9 + p10 + q7 + q8 + q9 + q10 > 0) || p4 + q4 = 0)
}
safety property "A1" {
!(!(p7 + p8 + p9 + p10 + q7 + q8 + q9 + q10 > 0) ||
(!(p7 + p8 + p9 + p10 > 0) || flag1v3 + flag1v4 > 0) ||
(!(q7 + q8 + q9 + q10 > 0) || flag2v3 + flag2v4 > 0))
}
safety property "A2" {
!(!(q9 + q10 > 0) || p4 + p5 + p6 + p7 + p8 + p9 + p10 = 0)
}
safety property "A3" {
!((!(p10 > 0 && q4 + q5 + q6 + q7 + q8 + q9 + q10 > 0) || flag2v4 > 0) &&
(!(q10 > 0 && p4 + p5 + p6 + p7 + p8 + p9 + p10 > 0) || flag1v4 > 0))
}
petri net "terminating" {
places { p1 p2 p3 p4 q1 q2 q3 q4 }
transitions { t1 t2 t3 t4 u1 u2 u3 }
arcs {
p1 -> t1 -> p2
p3 -> t1 -> p3
q1 -> t1 -> q1
p2 -> t2 -> p1
p4 -> t2 -> p4
q2 -> t2 -> q2
p3 -> t3 -> p4
p2 -> t3 -> p2
q3 -> t3 -> q3
p4 -> t4 -> p3
p1 -> t4 -> p1
q4 -> t4 -> q4
q1 -> u1 -> q2
q2 -> u2 -> q3
q3 -> u3 -> q4
}
initial { p1 p3 q1 q2 q3 }
}
liveness property "terminating" {
true // t1 + t2 + t3 + t4 + u1 + u2 + u3 > 0
}
petri net "terminating" {
places { p1 p2 p3 p4 p5 p6 p7 }
transitions { t1 t2 t3 t4 t5 t6 }
arcs {
p1 -> t1 -> p2
p4 -> t1 -> p4
p2 -> t2 -> p3
p5 -> t2 -> p5
p3 -> t3 -> p1
p6 -> t3 -> p6
p4 -> t4 -> p5
p5 -> t5 -> p6
p6 -> t6 -> p4
p7 -> t6
}
initial { p1 p4 p5 p7 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { q1 s2 s3 s4 s5 p2 p3 p4 p5 q2 }
transitions { t1 t2 t3 t4 u1 u2 u3 u4 v1 v2 }
arcs {
q1 -> t1 -> s2
s2 -> t2 -> q1
s3 -> t3 -> s4
s3 -> t1 -> s3
s4 -> t4 -> s3
s4 -> t2 -> s4
s5 -> t4
q1 -> u1 -> p2
p2 -> u2 -> q1
p3 -> u3 -> p4
p3 -> u1 -> p3
p4 -> u4 -> p3
p4 -> u2 -> p4
p5 -> u4
s2 -> v1 -> p2
q2 -> v1
p2 -> v2 -> s2
q2 -> v2
}
initial { q1 s3 s5 p3 p5 q2 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { s1 s2 s3 s4 s5 s6 s7 s8 s9 }
transitions { t1 t2 t3 t4 t5 t6 }
arcs {
s1 -> t1 -> s2
s3 -> t1 -> s3
s2 -> t2 -> s1
s4 -> t2 -> s4
{ s3 s5 } -> t3 -> { s4 s6 }
{ s4 s6 s9 } -> t4 -> { s3 s5 }
s7 -> t5 -> s8
s5 -> t5 -> s5
s8 -> t6 -> s7
s6 -> t6 -> s6
}
initial { s1 s7 s3 s6 s9 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { s1 s2 s3 s4 s5 s6 s7 }
transitions { t1 t2 t3 t4 t5 t6 }
arcs {
s1 -> t1 -> s2
s3 -> t1 -> s3
s2 -> t2 -> s1
s4 -> t2 -> s4
s3 -> t3 -> s4
s5 -> t3 -> s5
s4 -> t4 -> s3
s6 -> t4 -> s6
s5 -> t5 -> s6
s6 -> t6 -> s5
s7 -> t6
}
initial { s1 s3 s5 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { p1 p2 p3 p4 p5 }
transitions { t1 t2 t3 t4 }
arcs {
p1 -> t1 -> p2
p2 ->[3] t2 ->[3] p1
p3 -> t3 -> p4
p3 -> t1 -> p3
p4 -> t4 -> p3
p4 -> t2 -> p4
p5 -> t4
}
initial { p1[3] p3 p5 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { s1 s2 s3 s4 s5 s6 s7 }
transitions { t1 t2 t3 t4 t5 t6 }
arcs {
s1 -> t1 -> s2
s3 -> t1 -> s3
s2 -> t2 -> s1
s4 -> t2 -> s4
s3 -> t3 -> s4
s2 -> t4 -> s5
s6 -> t4 -> s6
s5 -> t5 -> s2
s7 -> t5 -> s7
s6 -> t6 -> s7
}
initial { s1 s3 s6 }
}
liveness property "terminating" {
true
}
petri net "terminating" {
places { p1 p2 }
transitions { t1 t2 }
places { p1 p2 p3 p4 p5 }
transitions { t1 t2 t3 t4 }
arcs {
p1 -> t1 -> p2
p3 -> t1 -> p3
p2 -> t2 -> p1
p4 -> t2 -> p4
p3 -> t3 -> p4
p4 -> t4 -> p3
p5 -> t4
}
initial { p1 }
initial { p1 p3 p5 }
}
liveness property "terminating" {
t1 + t2 + t3 + t4 > 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