From 877e9d095489e5f52613a1f8462dc8f655b7d05a Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sat, 8 Dec 2018 21:58:39 +0000 Subject: [PATCH] Benchmarks --- drs_benchmark.sh | 2 +- in/scripts/gen_tgc_sc.py | 22 +++++++++++----------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/drs_benchmark.sh b/drs_benchmark.sh index a925c62..b7ad43d 100755 --- a/drs_benchmark.sh +++ b/drs_benchmark.sh @@ -7,7 +7,7 @@ CMD="./reactics -B" timelimit="$((30*60))" # 30 minutes timelimit="$((5*60))" # 5 minutes -form_tgc_sc="`seq 1 3`" +form_tgc_sc="`seq 1 4`" form_asm="`seq 1 2`" for benchmark in "tgc_sc" "asm"; do diff --git a/in/scripts/gen_tgc_sc.py b/in/scripts/gen_tgc_sc.py index 81957c4..23878f4 100755 --- a/in/scripts/gen_tgc_sc.py +++ b/in/scripts/gen_tgc_sc.py @@ -79,31 +79,31 @@ for i in range(n): out += CA_STR.format(transitions) -# f1 -formula = "EF( proc0.in )" -out += PROPERTY_STR.format("f1",formula) +## f1 +#formula = "EF( proc0.in )" +#out += PROPERTY_STR.format("f1",formula) -# f2 +# f1 formula = "EF( EX( proc0.in ) )" for i in range(1, n): formula += " AND EF( EX( proc{:d}.in ) )".format(i, i) -out += PROPERTY_STR.format("f2",formula) +out += PROPERTY_STR.format("f1",formula) -# f3 +# f2 formula = "EF( proc0.approach" for i in range(1, n): formula += " AND proc{:d}.approach".format(i) formula += " )" -out += PROPERTY_STR.format("f3",formula) +out += PROPERTY_STR.format("f2",formula) -# f4 +# f3 subf = "~proc1.in" for i in range(2, n): subf += " AND ~proc{:d}.in".format(i) 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" for i in range(2, n): subf += " AND ~proc{:d}.in".format(i) @@ -111,7 +111,7 @@ all_agents = "proc0" for i in range(1, n): all_agents += ",proc{:d}".format(i) 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)