Commit 64e57c8f authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added two (unused) benchmarks

parent ccadabd9
n ps ts user system memory
2 22 24 0.08 0.01 14432
#!/usr/bin/python3
import sys
# //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
#
print("""
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
}
""")
#!/usr/bin/python3
import sys
print("""
petri net "The drinking philosophers for n=2" {
places {
p1h p1e
p2h p2e
req1p1 req1p2
req2p1 req2p2
fork1p1 fork1p2
fork2p1 fork2p2
fork1clean fork1dirty
fork2clean fork2dirty
}
transitions {
p1req1 p1req2 p1give1 p1give2 p1eat p1done
p2req1 p2req2 p2give1 p2give2 p2eat p2done
//p1done(2),p1eat(2),p1give1,p1give2,p1req1,p1req2,
//p2give1,p2give2,p2req1,p2req2
}
arcs {
{ p1h req1p1 fork1p2 } -> p1req1 -> { p1h req1p2 fork1p2 }
{ p1h req2p1 fork2p2 } -> p1req2 -> { p1h req2p2 fork2p2 }
{ p1h req1p1 fork1p1 fork1dirty } -> p1give1 -> { p1h req1p1 fork1p2 fork1clean }
{ p1h req2p1 fork2p1 fork2dirty } -> p1give2 -> { p1h req2p1 fork2p2 fork2clean }
{ p1h fork1p1 fork2p1 fork1clean fork2clean } -> p1eat -> { p1e fork1p1 fork2p1 fork1dirty fork2dirty }
{ p1e } -> p1done -> { p1h }
{ p2h req1p2 fork1p1 } -> p2req1 -> { p2h req1p1 fork1p1 }
{ p2h req2p2 fork2p1 } -> p2req2 -> { p2h req2p1 fork2p1 }
{ p2h req1p2 fork1p2 fork1dirty } -> p2give1 -> { p2h req1p2 fork1p1 fork1clean }
{ p2h req2p2 fork2p2 fork2dirty } -> p2give2 -> { p2h req2p2 fork2p1 fork2clean }
{ p2h fork1p2 fork2p2 fork1clean fork2clean } -> p2eat -> { p2e fork1p2 fork2p2 fork1dirty fork2dirty }
{ p2e } -> p2done -> { p2h }
}
initial {
p1h p2h
fork1dirty fork2dirty
fork1p1 fork2p1 req1p2 req2p2
}
}
liveness property "philosopher 1 does not starve" {
p1req1 + p1req2 + p1give1 + p1give2 + p1eat + p1done > 0 &&
p2req1 + p2req2 + p2give1 + p2give2 + p2eat + p2done > 0 &&
p1eat = 0
}
liveness property "philosopher 2 does not starve" {
p1req1 + p1req2 + p1give1 + p1give2 + p1eat + p1done > 0 &&
p2req1 + p2req2 + p2give1 + p2give2 + p2eat + p2done > 0 &&
p2eat = 0
}
safety property "mutual exclusion" {
p1e >= 1 && p2e >= 1
}
""")
PLACE fork1clean,fork1dirty,fork1p1,fork1p2,fork2clean,fork2dirty,fork2p1,fork2p2,p1e,p1h,p2e,p2h,req1p1,req1p2,req2p1,req2p2,p1eatc,p2eatc;
MARKING fork1dirty:1,fork1p1:1,fork2dirty:1,fork2p1:1,p1h:1,p2h:1,req1p2:1,req2p2:1;
TRANSITION p1done
CONSUME p1e:1;
PRODUCE p1h:1;
TRANSITION p1eat
CONSUME fork1clean:1,fork1p1:1,fork2clean:1,fork2p1:1,p1h:1;
PRODUCE fork1dirty:1,fork1p1:1,fork2dirty:1,fork2p1:1,p1e:1,p1eatc:1;
TRANSITION p1give1
CONSUME fork1dirty:1,fork1p1:1,p1h:1,req1p1:1;
PRODUCE fork1clean:1,fork1p2:1,p1h:1,req1p1:1;
TRANSITION p1give2
CONSUME fork2dirty:1,fork2p1:1,p1h:1,req2p1:1;
PRODUCE fork2clean:1,fork2p2:1,p1h:1,req2p1:1;
TRANSITION p1req1
CONSUME fork1p2:1,p1h:1,req1p1:1;
PRODUCE fork1p2:1,p1h:1,req1p2:1;
TRANSITION p1req2
CONSUME fork2p2:1,p1h:1,req2p1:1;
PRODUCE fork2p2:1,p1h:1,req2p2:1;
TRANSITION p2done
CONSUME p2e:1;
PRODUCE p2h:1;
TRANSITION p2eat
CONSUME fork1clean:1,fork1p2:1,fork2clean:1,fork2p2:1,p2h:1;
PRODUCE fork1dirty:1,fork1p2:1,fork2dirty:1,fork2p2:1,p2e:1,p2eatc:1;
TRANSITION p2give1
CONSUME fork1dirty:1,fork1p2:1,p2h:1,req1p2:1;
PRODUCE fork1clean:1,fork1p1:1,p2h:1,req1p2:1;
TRANSITION p2give2
CONSUME fork2dirty:1,fork2p2:1,p2h:1,req2p2:1;
PRODUCE fork2clean:1,fork2p1:1,p2h:1,req2p2:1;
TRANSITION p2req1
CONSUME fork1p1:1,p2h:1,req1p2:1;
PRODUCE fork1p1:1,p2h:1,req1p1:1;
TRANSITION p2req2
CONSUME fork2p1:1,p2h:1,req2p2:1;
PRODUCE fork2p1:1,p2h:1,req2p1:1;
EF ( p1eatc > p2eatc AND p1eatc <= 10 AND p2eatc <= 10 )
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