artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Benchmarks

Browse Source
This commit is contained in:
Artur Meski
2018-12-08 21:58:39 +00:00
parent 8226919c0e
commit 877e9d0954
2 changed files with 12 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
drs_benchmark.sh
View File

@@ -7,7 +7,7 @@ CMD="./reactics -B"
timelimit="$((30*60))" # 30 minutes timelimit="$((30*60))" # 30 minutes
timelimit="$((5*60))" # 5 minutes timelimit="$((5*60))" # 5 minutes
form_tgc_sc="`seq 1 3`" form_tgc_sc="`seq 1 4`"
form_asm="`seq 1 2`" form_asm="`seq 1 2`"
for benchmark in "tgc_sc" "asm"; do for benchmark in "tgc_sc" "asm"; do

22
in/scripts/gen_tgc_sc.py
View File

@@ -79,31 +79,31 @@ for i in range(n):
out += CA_STR.format(transitions) out += CA_STR.format(transitions)
# f1 ## f1
formula = "EF( proc0.in )" #formula = "EF( proc0.in )"
out += PROPERTY_STR.format("f1",formula) #out += PROPERTY_STR.format("f1",formula)
# f2 # f1
formula = "EF( E<proc0.allowed>X( proc0.in ) )" formula = "EF( E<proc0.allowed>X( proc0.in ) )"
for i in range(1, n): for i in range(1, n):
formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i) formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
out += PROPERTY_STR.format("f2",formula) out += PROPERTY_STR.format("f1",formula)
# f3 # f2
formula = "EF( proc0.approach" formula = "EF( proc0.approach"
for i in range(1, n): for i in range(1, n):
formula += " AND proc{:d}.approach".format(i) formula += " AND proc{:d}.approach".format(i)
formula += " )" formula += " )"
out += PROPERTY_STR.format("f3",formula) out += PROPERTY_STR.format("f2",formula)
# f4 # f3
subf = "~proc1.in" subf = "~proc1.in"
for i in range(2, n): for i in range(2, n):
subf += " AND ~proc{:d}.in".format(i) subf += " AND ~proc{:d}.in".format(i)
formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf) formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
out += PROPERTY_STR.format("f4",formula) out += PROPERTY_STR.format("f3",formula)
# f5 # f4
subf = "~proc1.in" subf = "~proc1.in"
for i in range(2, n): for i in range(2, n):
subf += " AND ~proc{:d}.in".format(i) subf += " AND ~proc{:d}.in".format(i)
@@ -111,7 +111,7 @@ all_agents = "proc0"
for i in range(1, n): for i in range(1, n):
all_agents += ",proc{:d}".format(i) all_agents += ",proc{:d}".format(i)
formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf) formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
out += PROPERTY_STR.format("f5",formula) out += PROPERTY_STR.format("f4",formula)
print(out) print(out)