From 5df8d6aeb9d9c803df34508ee4ceeb88b0277326 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 14:06:08 +0100 Subject: [PATCH] Test harness & some refactoring --- examples/bdd/{tgc.rs => tgc.drs} | 0 examples/bdd/tgc4.drs | 70 ++++++++++++ reactics-bdd/ctx_aut.cc | 7 +- reactics-bdd/ctx_aut.hh | 3 - reactics-bdd/drs_benchmark.sh | 2 +- reactics-bdd/formrsctlk.cc | 49 -------- reactics-bdd/formrsctlk.hh | 46 -------- reactics-bdd/in/{hsr.rs => hsr.drs} | 0 reactics-bdd/in/{hsr_ca.rs => hsr_ca.drs} | 0 reactics-bdd/in/{hsr_drs.rs => hsr_drs.drs} | 0 .../in/old_syntax/{bc32.rs => bc32.drs} | 0 .../in/old_syntax/{bc8.rs => bc8.drs} | 0 .../in/old_syntax/{coffee.rs => coffee.drs} | 0 .../in/old_syntax/{expr.rs => expr.drs} | 0 .../{simple_I1.rs => simple_I1.drs} | 0 .../in/old_syntax/{test.rs => test.drs} | 0 reactics-bdd/in/old_syntax/{u1.rs => u1.drs} | 0 reactics-bdd/in/old_syntax/{u2.rs => u2.drs} | 0 reactics-bdd/in/scripts/bench_bc.sh | 6 +- reactics-bdd/in/scripts/bench_mutex.sh | 6 +- reactics-bdd/in/scripts/bench_pipe.sh | 6 +- reactics-bdd/in/scripts/benchmark.sh | 6 +- reactics-bdd/in/scripts/benchmark_abs1.sh | 6 +- reactics-bdd/in/scripts/benchmark_abs1_PT.sh | 6 +- reactics-bdd/in/scripts/benchmark_bc.sh | 6 +- reactics-bdd/in/scripts/benchmark_mutex.sh | 6 +- reactics-bdd/in/scripts/benchmark_mutex_PT.sh | 6 +- reactics-bdd/in/{trivial.rs => trivial.drs} | 0 reactics-bdd/mc.cc | 12 +- reactics-bdd/reactics.cc | 17 +-- reactics-bdd/rs.cc | 48 ++------ reactics-bdd/rs.hh | 1 + reactics-bdd/symrs.cc | 108 +----------------- reactics-bdd/symrs.hh | 13 --- reactics-bdd/{test.rs => test.drs} | 0 tests/expected/tgc4_mc.txt | 8 ++ tests/expected/tgc4_print.txt | 58 ++++++++++ tests/expected/tgc4_states.txt | 80 +++++++++++++ tests/expected/tgc_mc.txt | 8 ++ tests/expected/tgc_print.txt | 47 ++++++++ tests/expected/tgc_reactions.txt | 23 ++++ tests/expected/tgc_states.txt | 32 ++++++ tests/expected/trivial_print.txt | 17 +++ tests/expected/trivial_reactions.txt | 8 ++ tests/expected/trivial_states.txt | 3 + tests/run_tests.sh | 69 +++++++++++ 46 files changed, 478 insertions(+), 305 deletions(-) rename examples/bdd/{tgc.rs => tgc.drs} (100%) create mode 100644 examples/bdd/tgc4.drs rename reactics-bdd/in/{hsr.rs => hsr.drs} (100%) rename reactics-bdd/in/{hsr_ca.rs => hsr_ca.drs} (100%) rename reactics-bdd/in/{hsr_drs.rs => hsr_drs.drs} (100%) rename reactics-bdd/in/old_syntax/{bc32.rs => bc32.drs} (100%) rename reactics-bdd/in/old_syntax/{bc8.rs => bc8.drs} (100%) rename reactics-bdd/in/old_syntax/{coffee.rs => coffee.drs} (100%) rename reactics-bdd/in/old_syntax/{expr.rs => expr.drs} (100%) rename reactics-bdd/in/old_syntax/{simple_I1.rs => simple_I1.drs} (100%) rename reactics-bdd/in/old_syntax/{test.rs => test.drs} (100%) rename reactics-bdd/in/old_syntax/{u1.rs => u1.drs} (100%) rename reactics-bdd/in/old_syntax/{u2.rs => u2.drs} (100%) rename reactics-bdd/in/{trivial.rs => trivial.drs} (100%) rename reactics-bdd/{test.rs => test.drs} (100%) create mode 100644 tests/expected/tgc4_mc.txt create mode 100644 tests/expected/tgc4_print.txt create mode 100644 tests/expected/tgc4_states.txt create mode 100644 tests/expected/tgc_mc.txt create mode 100644 tests/expected/tgc_print.txt create mode 100644 tests/expected/tgc_reactions.txt create mode 100644 tests/expected/tgc_states.txt create mode 100644 tests/expected/trivial_print.txt create mode 100644 tests/expected/trivial_reactions.txt create mode 100644 tests/expected/trivial_states.txt create mode 100755 tests/run_tests.sh diff --git a/examples/bdd/tgc.rs b/examples/bdd/tgc.drs similarity index 100% rename from examples/bdd/tgc.rs rename to examples/bdd/tgc.drs diff --git a/examples/bdd/tgc4.drs b/examples/bdd/tgc4.drs new file mode 100644 index 0000000..ed9b345 --- /dev/null +++ b/examples/bdd/tgc4.drs @@ -0,0 +1,70 @@ + +options { use-context-automaton; make-progressive; }; +reactions { + + proc0 { + {{out}, {} -> {approach}}; + {{approach}, {req} -> {req}}; + {{allowed}, {} -> {in}}; + {{in}, {} -> {out,leave}}; + {{req}, {in} -> {req}}; + }; + + proc1 { + {{out}, {} -> {approach}}; + {{approach}, {req} -> {req}}; + {{allowed}, {} -> {in}}; + {{in}, {} -> {out,leave}}; + {{req}, {in} -> {req}}; + }; + + proc2 { + {{out}, {} -> {approach}}; + {{approach}, {req} -> {req}}; + {{allowed}, {} -> {in}}; + {{in}, {} -> {out,leave}}; + {{req}, {in} -> {req}}; + }; + + proc3 { + {{out}, {} -> {approach}}; + {{approach}, {req} -> {req}}; + {{allowed}, {} -> {in}}; + {{in}, {} -> {out,leave}}; + {{req}, {in} -> {req}}; + }; +}; + +context-automaton { + states { init, green, red }; + init-state { init }; + transitions { + { proc0={out} proc1={out} proc2={out} proc3={out} }: init -> green; + { proc0={allowed} }: green -> red : proc0.req; + { proc1={allowed} }: green -> red : proc1.req; + { proc2={allowed} }: green -> red : proc2.req; + { proc3={allowed} }: green -> red : proc3.req; + { proc0={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req; + { proc1={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req; + { proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req; + { proc3={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req AND ~proc3.req; + { proc0={} }: red -> green : proc0.leave; + { proc1={} }: red -> green : proc1.leave; + { proc2={} }: red -> green : proc2.leave; + { proc3={} }: red -> green : proc3.leave; + { proc0={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave; + { proc1={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave; + { proc2={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave; + { proc3={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave AND ~proc3.leave; + + }; +}; + +rsctlk-property { f1 : EF( EX( proc0.in ) ) AND EF( EX( proc1.in ) ) AND EF( EX( proc2.in ) ) AND EF( EX( proc3.in ) ) }; + +rsctlk-property { f2 : EF( proc0.approach AND proc1.approach AND proc2.approach AND proc3.approach ) }; + +rsctlk-property { f3 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in AND ~proc3.in) ) }; + +rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2,proc3](~proc1.in AND ~proc2.in AND ~proc3.in) ) }; + diff --git a/reactics-bdd/ctx_aut.cc b/reactics-bdd/ctx_aut.cc index fb7c9f7..7509c7e 100644 --- a/reactics-bdd/ctx_aut.cc +++ b/reactics-bdd/ctx_aut.cc @@ -13,12 +13,7 @@ CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) bool CtxAut::hasState(std::string name) { - if (states_names.find(name) == states_names.end()) { - return false; - } - else { - return true; - } + return states_names.find(name) != states_names.end(); } State CtxAut::getStateID(std::string name) diff --git a/reactics-bdd/ctx_aut.hh b/reactics-bdd/ctx_aut.hh index d446459..a91a326 100644 --- a/reactics-bdd/ctx_aut.hh +++ b/reactics-bdd/ctx_aut.hh @@ -12,10 +12,7 @@ #include #include #include -// #include "rs.hh" #include "types.hh" -// #include "options.hh" -// #include "stateconstr.hh" using std::cout; using std::endl; diff --git a/reactics-bdd/drs_benchmark.sh b/reactics-bdd/drs_benchmark.sh index b7ad43d..ef2e2c6 100755 --- a/reactics-bdd/drs_benchmark.sh +++ b/reactics-bdd/drs_benchmark.sh @@ -1,6 +1,6 @@ #!/bin/sh -TMPINPUT="tmp_$RANDOM$RANDOM.rs" +TMPINPUT="tmp_$RANDOM$RANDOM.drs" CMD="./reactics -B" diff --git a/reactics-bdd/formrsctlk.cc b/reactics-bdd/formrsctlk.cc index 4658e52..d203849 100644 --- a/reactics-bdd/formrsctlk.cc +++ b/reactics-bdd/formrsctlk.cc @@ -172,39 +172,6 @@ bool FormRSCTLK::isERSCTLK(void) const std::string FormRSCTLK::getActionsStr(void) const { - // if (actions != nullptr) { - // std::string r = "[ "; - // bool firstact = true; - // - // for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); - // ++act) { - // if (!firstact) { - // r += ","; - // } - // else { - // firstact = false; - // } - // - // r += "{"; - // bool firstent = true; - // - // for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) { - // if (!firstent) { - // r += ","; - // } - // else { - // firstent = false; - // } - // - // r += *ent; - // } - // - // r += "}"; - // } - // - // r += " ]"; - // return r; - // } if (boolCtx != nullptr) { return "< " + boolCtx->toStr() + " >"; } @@ -222,22 +189,6 @@ void FormRSCTLK::encodeActions(const SymRS *srs) actions_bdd = new BDD(srs->getBDDfalse()); assert(boolCtx != nullptr); - // assert(actions != nullptr || boolCtx != nullptr); - // assert(!(actions != nullptr && boolCtx != nullptr)); - - // if (actions != nullptr) { - // for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); - // ++act) { - // BDD single_action = srs->getBDDtrue(); - // - // for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) { - // single_action *= srs->encActStrEntity(*ent); - // } - // - // single_action = srs->compContext(single_action); - // *actions_bdd += single_action; - // } - // } if (boolCtx != nullptr) { *actions_bdd = boolCtx->getBDDforContext(srs); } diff --git a/reactics-bdd/formrsctlk.hh b/reactics-bdd/formrsctlk.hh index b9091fd..c9f557f 100644 --- a/reactics-bdd/formrsctlk.hh +++ b/reactics-bdd/formrsctlk.hh @@ -9,7 +9,6 @@ #include #include #include -// #include "rs.hh" #include "symrs.hh" #include "cudd.hh" #include "types.hh" @@ -56,9 +55,6 @@ using std::cout; using std::endl; -// typedef std::string Entity_f; -// typedef std::set Action_f; -// typedef vector ActionsVec_f; typedef std::set Agents_f; class StateConstr; @@ -74,7 +70,6 @@ class FormRSCTLK std::string proc_name; bool tf; BDD *bdd; - // ActionsVec_f *actions; BDD *actions_bdd; StateConstr *boolCtx; Agents_f agents; @@ -93,7 +88,6 @@ class FormRSCTLK arg[0] = nullptr; arg[1] = nullptr; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -110,7 +104,6 @@ class FormRSCTLK arg[0] = nullptr; arg[1] = nullptr; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -126,28 +119,10 @@ class FormRSCTLK arg[0] = form1; arg[1] = form2; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } - /** - * @brief Constructor for two-argument formula with action restrictions. - */ - // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2) - // { - // assert(acts != nullptr); - // assert(RSCTLK_COND_2ARG(op)); - // assert(RSCTLK_COND_ACT(op)); - // oper = op; - // arg[0] = form1; - // arg[1] = form2; - // bdd = nullptr; - // actions = acts; - // actions_bdd = nullptr; - // boolCtx = nullptr; - // } - /** * @brief Constructor for two-argument formula with Boolean context restrictions. */ @@ -160,7 +135,6 @@ class FormRSCTLK arg[0] = form1; arg[1] = form2; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = bctx; } @@ -176,28 +150,10 @@ class FormRSCTLK arg[0] = form1; arg[1] = nullptr; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } - /** - * @brief Constructor for one-argument formula with action restrictions. - */ - // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1) - // { - // assert(acts != nullptr); - // assert(RSCTLK_COND_1ARG(op)); - // assert(RSCTLK_COND_ACT(op)); - // oper = op; - // arg[0] = form1; - // arg[1] = nullptr; - // bdd = nullptr; - // // actions = acts; - // actions_bdd = nullptr; - // boolCtx = nullptr; - // } - /** * @brief Constructor for one-argument formula with Boolean context restrictions. */ @@ -210,7 +166,6 @@ class FormRSCTLK arg[0] = form1; arg[1] = nullptr; bdd = nullptr; - // actions = nullptr; actions_bdd = nullptr; boolCtx = bctx; } @@ -234,7 +189,6 @@ class FormRSCTLK delete arg[0]; delete arg[1]; delete bdd; - // delete actions; delete actions_bdd; delete boolCtx; } diff --git a/reactics-bdd/in/hsr.rs b/reactics-bdd/in/hsr.drs similarity index 100% rename from reactics-bdd/in/hsr.rs rename to reactics-bdd/in/hsr.drs diff --git a/reactics-bdd/in/hsr_ca.rs b/reactics-bdd/in/hsr_ca.drs similarity index 100% rename from reactics-bdd/in/hsr_ca.rs rename to reactics-bdd/in/hsr_ca.drs diff --git a/reactics-bdd/in/hsr_drs.rs b/reactics-bdd/in/hsr_drs.drs similarity index 100% rename from reactics-bdd/in/hsr_drs.rs rename to reactics-bdd/in/hsr_drs.drs diff --git a/reactics-bdd/in/old_syntax/bc32.rs b/reactics-bdd/in/old_syntax/bc32.drs similarity index 100% rename from reactics-bdd/in/old_syntax/bc32.rs rename to reactics-bdd/in/old_syntax/bc32.drs diff --git a/reactics-bdd/in/old_syntax/bc8.rs b/reactics-bdd/in/old_syntax/bc8.drs similarity index 100% rename from reactics-bdd/in/old_syntax/bc8.rs rename to reactics-bdd/in/old_syntax/bc8.drs diff --git a/reactics-bdd/in/old_syntax/coffee.rs b/reactics-bdd/in/old_syntax/coffee.drs similarity index 100% rename from reactics-bdd/in/old_syntax/coffee.rs rename to reactics-bdd/in/old_syntax/coffee.drs diff --git a/reactics-bdd/in/old_syntax/expr.rs b/reactics-bdd/in/old_syntax/expr.drs similarity index 100% rename from reactics-bdd/in/old_syntax/expr.rs rename to reactics-bdd/in/old_syntax/expr.drs diff --git a/reactics-bdd/in/old_syntax/simple_I1.rs b/reactics-bdd/in/old_syntax/simple_I1.drs similarity index 100% rename from reactics-bdd/in/old_syntax/simple_I1.rs rename to reactics-bdd/in/old_syntax/simple_I1.drs diff --git a/reactics-bdd/in/old_syntax/test.rs b/reactics-bdd/in/old_syntax/test.drs similarity index 100% rename from reactics-bdd/in/old_syntax/test.rs rename to reactics-bdd/in/old_syntax/test.drs diff --git a/reactics-bdd/in/old_syntax/u1.rs b/reactics-bdd/in/old_syntax/u1.drs similarity index 100% rename from reactics-bdd/in/old_syntax/u1.rs rename to reactics-bdd/in/old_syntax/u1.drs diff --git a/reactics-bdd/in/old_syntax/u2.rs b/reactics-bdd/in/old_syntax/u2.drs similarity index 100% rename from reactics-bdd/in/old_syntax/u2.rs rename to reactics-bdd/in/old_syntax/u2.drs diff --git a/reactics-bdd/in/scripts/bench_bc.sh b/reactics-bdd/in/scripts/bench_bc.sh index 5335a77..23cd961 100644 --- a/reactics-bdd/in/scripts/bench_bc.sh +++ b/reactics-bdd/in/scripts/bench_bc.sh @@ -42,10 +42,10 @@ for form in $forms; do echo "$x" > $filename - ./gen_bc.py $n $form > tmp.rs + ./gen_bc.py $n $form > tmp.drs - echo "EXEC: $tool $options $popt tmp.rs" - $tool $options $popt tmp.rs >&1 >> $filename + echo "EXEC: $tool $options $popt tmp.drs" + $tool $options $popt tmp.drs >&1 >> $filename result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" if [ "$result" = "" ];then diff --git a/reactics-bdd/in/scripts/bench_mutex.sh b/reactics-bdd/in/scripts/bench_mutex.sh index 822d4ab..b074516 100644 --- a/reactics-bdd/in/scripts/bench_mutex.sh +++ b/reactics-bdd/in/scripts/bench_mutex.sh @@ -44,11 +44,11 @@ for form in $forms; do echo "$x" > $filename - ./gen_mutex.py $n $form > tmp.rs + ./gen_mutex.py $n $form > tmp.drs - echo "EXEC: $tool $options $popt tmp.rs" + echo "EXEC: $tool $options $popt tmp.drs" - $tool $options $popt tmp.rs >&1 >> $filename + $tool $options $popt tmp.drs >&1 >> $filename result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" if [ "$result" = "" ];then diff --git a/reactics-bdd/in/scripts/bench_pipe.sh b/reactics-bdd/in/scripts/bench_pipe.sh index a527942..31f0e8b 100644 --- a/reactics-bdd/in/scripts/bench_pipe.sh +++ b/reactics-bdd/in/scripts/bench_pipe.sh @@ -43,11 +43,11 @@ for form in $forms; do echo "$x" > $filename - ./gen_abstract1.py $n $form > tmp.rs + ./gen_abstract1.py $n $form > tmp.drs - echo "EXEC: $tool $options $popt tmp.rs" + echo "EXEC: $tool $options $popt tmp.drs" - $tool $options $popt tmp.rs >&1 >> $filename + $tool $options $popt tmp.drs >&1 >> $filename result="$(tail -1 $filename | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" if [ "$result" = "" ];then diff --git a/reactics-bdd/in/scripts/benchmark.sh b/reactics-bdd/in/scripts/benchmark.sh index 61efef1..7798bab 100644 --- a/reactics-bdd/in/scripts/benchmark.sh +++ b/reactics-bdd/in/scripts/benchmark.sh @@ -4,8 +4,8 @@ for x in `seq 2 1 24`;do echo $y $x filename="results/f${y}_n${x}.out" echo "$x" > $filename - ./gen_bc.py $x $y > tmp.rs - ../main -c -B tmp.rs >> $filename + ./gen_bc.py $x $y > tmp.drs + ../main -c -B tmp.drs >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_f${y}.out echo $result @@ -13,4 +13,4 @@ for x in `seq 2 1 24`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/scripts/benchmark_abs1.sh b/reactics-bdd/in/scripts/benchmark_abs1.sh index 6089667..6b3f85b 100644 --- a/reactics-bdd/in/scripts/benchmark_abs1.sh +++ b/reactics-bdd/in/scripts/benchmark_abs1.sh @@ -4,8 +4,8 @@ for x in `seq 1 60`;do echo $x filename="results/abs_v${y}_f0_n${x}.out" echo "$x" > $filename - ./gen_abstract1.py $x $y > tmp.rs - ../main -z -c -p -v -B tmp.rs >&1 >> $filename + ./gen_abstract1.py $x $y > tmp.drs + ../main -z -c -p -v -B tmp.drs >&1 >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_v${y}_abs_f0.out echo $result @@ -13,4 +13,4 @@ for x in `seq 1 60`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/scripts/benchmark_abs1_PT.sh b/reactics-bdd/in/scripts/benchmark_abs1_PT.sh index 4f40afe..c69b705 100644 --- a/reactics-bdd/in/scripts/benchmark_abs1_PT.sh +++ b/reactics-bdd/in/scripts/benchmark_abs1_PT.sh @@ -4,8 +4,8 @@ for x in `seq 1 60`;do echo $x filename="results/abs_v${y}_f0_n${x}_PT.out" echo "$x" > $filename - ./gen_abstract1.py $x $y > tmp.rs - ../main -z -x -c -p -v -B tmp.rs >&1 >> $filename + ./gen_abstract1.py $x $y > tmp.drs + ../main -z -x -c -p -v -B tmp.drs >&1 >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_v${y}_abs_f0_PT.out echo $result @@ -13,4 +13,4 @@ for x in `seq 1 60`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/scripts/benchmark_bc.sh b/reactics-bdd/in/scripts/benchmark_bc.sh index f1c5231..acae1a4 100644 --- a/reactics-bdd/in/scripts/benchmark_bc.sh +++ b/reactics-bdd/in/scripts/benchmark_bc.sh @@ -4,8 +4,8 @@ for x in `seq 1 50`;do echo $x $y filename="results/bc_f${y}_n${x}.out" echo "$x" > $filename - ./gen_bc.py $x $y > tmp.rs - ../main -z -c -v -B tmp.rs >&1 >> $filename + ./gen_bc.py $x $y > tmp.drs + ../main -z -c -v -B tmp.drs >&1 >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_bc_f${y}.out echo $result @@ -13,4 +13,4 @@ for x in `seq 1 50`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/scripts/benchmark_mutex.sh b/reactics-bdd/in/scripts/benchmark_mutex.sh index e3cca35..2853dc7 100644 --- a/reactics-bdd/in/scripts/benchmark_mutex.sh +++ b/reactics-bdd/in/scripts/benchmark_mutex.sh @@ -4,8 +4,8 @@ for x in `seq 2 40`;do echo $x $y filename="results/mutex_f${y}_n${x}.out" echo "$x" > $filename - ./gen_mutex.py $x $y > tmp.rs - ../main -z -c -p -v -B tmp.rs >&1 >> $filename + ./gen_mutex.py $x $y > tmp.drs + ../main -z -c -p -v -B tmp.drs >&1 >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_mutex_f${y}.out echo $result @@ -13,4 +13,4 @@ for x in `seq 2 40`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/scripts/benchmark_mutex_PT.sh b/reactics-bdd/in/scripts/benchmark_mutex_PT.sh index 096b672..fba41b3 100644 --- a/reactics-bdd/in/scripts/benchmark_mutex_PT.sh +++ b/reactics-bdd/in/scripts/benchmark_mutex_PT.sh @@ -4,8 +4,8 @@ for x in `seq 2 40`;do echo $x $y filename="results/mutex_f${y}_n${x}_PT.out" echo "$x" > $filename - ./gen_mutex.py $x $y > tmp.rs - ../main -zcpxvB tmp.rs >&1 >> $filename + ./gen_mutex.py $x $y > tmp.drs + ../main -zcpxvB tmp.drs >&1 >> $filename result="$(tail -1 $filename | sed "s/STAT/$x /")" echo $result >> results/summary_mutex_f${y}_PT.out echo $result @@ -13,4 +13,4 @@ for x in `seq 2 40`;do done done -rm tmp.rs +rm tmp.drs diff --git a/reactics-bdd/in/trivial.rs b/reactics-bdd/in/trivial.drs similarity index 100% rename from reactics-bdd/in/trivial.rs rename to reactics-bdd/in/trivial.drs diff --git a/reactics-bdd/mc.cc b/reactics-bdd/mc.cc index d1c7b4c..19fb1c0 100644 --- a/reactics-bdd/mc.cc +++ b/reactics-bdd/mc.cc @@ -517,9 +517,9 @@ BDD ModelChecker::getIthOnly(Process proc_id) /* nothing has been found in the cache */ BDD bdd = BDD_TRUE; - for (auto i = 0; i < pv_drs_E->size(); ++i) { + for (size_t i = 0; i < pv_drs_E->size(); ++i) { - if (i == proc_id) { + if (i == static_cast(proc_id)) { continue; } @@ -591,13 +591,7 @@ bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form) VERB("Checking the formula"); - //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero()) - if (*initStates * getStatesRSCTLK(form) == *initStates) { - result = true; - } - else { - result = false; - } + result = (*initStates * getStatesRSCTLK(form) == *initStates); cleanup(); diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc index 90e1298..6cd731f 100644 --- a/reactics-bdd/reactics.cc +++ b/reactics-bdd/reactics.cc @@ -37,13 +37,13 @@ int main(int argc, char **argv) &option_index)) != -1) { switch (c) { case 0: - printf("option %s", long_options[option_index].name); + cout << "option " << long_options[option_index].name; if (optarg) { - printf(" with arg %s", optarg); + cout << " with arg " << optarg; } - printf("\n"); + cout << endl; if (strcmp(long_options[option_index].name, "trace-parsing")) { driver.trace_parsing = true; @@ -236,16 +236,7 @@ int main(int argc, char **argv) delete opts; - int ret_val; - - if (result) { - ret_val = 0; - } - else { - ret_val = 1; - } - - return ret_val; + return result ? 0 : 1; } void print_help(std::string path_str) diff --git a/reactics-bdd/rs.cc b/reactics-bdd/rs.cc index f04c578..8cfb547 100644 --- a/reactics-bdd/rs.cc +++ b/reactics-bdd/rs.cc @@ -14,12 +14,7 @@ RctSys::RctSys(void) bool RctSys::hasEntity(std::string name) { - if (entities_names.find(name) == entities_names.end()) { - return false; - } - else { - return true; - } + return entities_names.find(name) != entities_names.end(); } void RctSys::addEntity(std::string name) @@ -84,21 +79,12 @@ void RctSys::addProcess(std::string processName) bool RctSys::hasProcess(std::string processName) { - if (processes_names.find(processName) == processes_names.end()) { - return false; - } - else { - return true; - } + return processes_names.find(processName) != processes_names.end(); } bool RctSys::hasProcess(Process processID) { - if (processID >= processes_ids.size()) { - return false; - } - - return true; + return processID < processes_ids.size(); } Process RctSys::getProcessID(std::string processName) @@ -120,28 +106,26 @@ std::string RctSys::getProcessName(Process processID) } } -void RctSys::pushReactant(std::string entityName) +void RctSys::ensureEntity(std::string entityName) { if (!hasEntity(entityName)) { addEntity(entityName); } +} +void RctSys::pushReactant(std::string entityName) +{ + ensureEntity(entityName); tmpReactants.insert(getEntityID(entityName)); } void RctSys::pushInhibitor(std::string entityName) { - if (!hasEntity(entityName)) { - addEntity(entityName); - } - + ensureEntity(entityName); tmpInhibitors.insert(getEntityID(entityName)); } void RctSys::pushProduct(std::string entityName) { - if (!hasEntity(entityName)) { - addEntity(entityName); - } - + ensureEntity(entityName); tmpProducts.insert(getEntityID(entityName)); } @@ -232,10 +216,7 @@ void RctSys::commitInitState(void) void RctSys::addActionEntity(std::string entityName) { - if (!hasEntity(entityName)) { - addEntity(entityName); - } - + ensureEntity(entityName); actionEntities.insert(getEntityID(entityName)); } @@ -248,12 +229,7 @@ void RctSys::addActionEntity(Entity entity) bool RctSys::isActionEntity(Entity entity) { - if (actionEntities.count(entity) > 0) { - return true; - } - else { - return false; - } + return actionEntities.count(entity) > 0; } void RctSys::showActionEntities(void) diff --git a/reactics-bdd/rs.hh b/reactics-bdd/rs.hh index 27ace9b..68a0f54 100644 --- a/reactics-bdd/rs.hh +++ b/reactics-bdd/rs.hh @@ -50,6 +50,7 @@ class RctSys void addReactionForCurrentProcess(Reaction reaction); + void ensureEntity(std::string entityName); void pushReactant(std::string entityName); void pushInhibitor(std::string entityName); void pushProduct(std::string entityName); diff --git a/reactics-bdd/symrs.cc b/reactics-bdd/symrs.cc index d99b38a..61fa969 100644 --- a/reactics-bdd/symrs.cc +++ b/reactics-bdd/symrs.cc @@ -17,9 +17,6 @@ SymRS::SymRS(RctSys *rs, Options *opts) totalEntities = rs->getEntitiesSize(); - // TODO: remove - totalActions = 0; - totalRctSysStateVars = getTotalProductVariables(); totalCtxEntities = getTotalCtxEntitiesVariables(); @@ -404,39 +401,19 @@ BDD SymRS::encCtxEntity(Process proc_id, Entity entity) const bool SymRS::productEntityExists(Process proc_id, Entity entity) const { - if (prod_ent_local_idx.count(proc_id) == 0) { - return false; - } - else { - if (prod_ent_local_idx.at(proc_id).count(entity) == 1) { - return true; - } - } - - return false; + return prod_ent_local_idx.count(proc_id) != 0 && + prod_ent_local_idx.at(proc_id).count(entity) == 1; } bool SymRS::ctxEntityExists(Process proc_id, Entity entity) const { - if (ctx_ent_local_idx.count(proc_id) == 0) { - return false; - } - else { - if (ctx_ent_local_idx.at(proc_id).count(entity) == 1) { - return true; - } - } - - return false; + return ctx_ent_local_idx.count(proc_id) != 0 && + ctx_ent_local_idx.at(proc_id).count(entity) == 1; } bool SymRS::processUsesEntity(Process proc_id, Entity entity_id) const { - if (productEntityExists(proc_id, entity_id) || ctxEntityExists(proc_id, entity_id)) { - return true; - } - - return false; + return productEntityExists(proc_id, entity_id) || ctxEntityExists(proc_id, entity_id); } BDD SymRS::encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ) @@ -511,20 +488,6 @@ BDD SymRS::encContext(const EntitiesForProc &proc_entities) return r; } -BDD SymRS::compState(const BDD &state) const -{ - assert(0); - BDD s = state; - - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { - if (!(*pv)[i] * state != cuddMgr->bddZero()) { - s *= !(*pv)[i]; - } - } - - return s; -} - BDD SymRS::compContext(const BDD &context) const { BDD c = context; @@ -725,65 +688,6 @@ BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id) return enab; } -// BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id) -// { -// assert(prod_conds.size() > prod_proc_id); - -// BDD enab = BDD_FALSE; - -// auto production_conditions = prod_conds[prod_proc_id][entity_id]; - -// VERB_LN(5, "| Produce " << rs->getEntityName(entity_id) << " in " << rs->getProcessName(prod_proc_id) << ":"); - -// for (const auto &cond : production_conditions) { - -// BDD reactants = BDD_TRUE; -// BDD inhibitors = BDD_TRUE; - -// for (const auto &reactant : cond.rctt) { -// BDD proc_reactants = BDD_FALSE; - -// for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) { -// if (processUsesEntity(proc_id, reactant)) { -// proc_reactants += encProcEnabled(proc_id) * encEntityCondition(proc_id, reactant); - -// VERB_LN(5, "| - if process " << rs->getProcessName(proc_id) << " is enabled and has " << rs->getEntityName(reactant)); - -// } -// } // END FOR: prod_id - -// reactants *= proc_reactants; -// } // END FOR: reactant - -// // For inhibitors, we take all the processes first and then we iterate over the inhibitors -// for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) { -// BDD proc_inhibitors = BDD_TRUE; - -// for (const auto &inhibitor : cond.inhib) { -// if (processUsesEntity(proc_id, inhibitor)) { -// proc_inhibitors *= !encEntityCondition(proc_id, inhibitor); -// } -// } - -// if (proc_inhibitors != BDD_TRUE) { // just an optimisation -// proc_inhibitors += !encProcEnabled(proc_id); -// inhibitors *= proc_inhibitors; -// } -// } - -// enab += reactants * inhibitors; - -// } // END FOR: cond - -// if (opts->reorder_trans) { -// VERB_L2("Reordering"); -// Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); -// } - -// return enab; -// } - - BDD SymRS::encEntitySameSuccessor(Process proc_id, Entity entity_id) { return BDD_IFF(encEntity(proc_id, entity_id), encEntitySucc(proc_id, entity_id)); @@ -810,7 +714,7 @@ void SymRS::encodeTransitions(void) prod_conds.resize(numberOfProc); - for (auto proc_id = 0; proc_id < numberOfProc; ++proc_id) { + for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) { prod_conds[proc_id] = getProductionConditions(proc_id); } diff --git a/reactics-bdd/symrs.hh b/reactics-bdd/symrs.hh index bcb5999..4feef3c 100644 --- a/reactics-bdd/symrs.hh +++ b/reactics-bdd/symrs.hh @@ -15,7 +15,6 @@ #include "types.hh" #include "macro.hh" #include "bdd_macro.hh" -// #include "rs.hh" #include "options.hh" #include "memtime.hh" @@ -240,16 +239,11 @@ class SymRS vector *pv_proc_ctx; BDDvec *pv_proc_ctx_E; - // TODO: remove - BDDvec *pv_act; - BDD *pv_act_E; - unsigned int totalEntities; unsigned int numberOfProc; /*!< The number of DRS processes */ unsigned int totalStateVars; unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */ unsigned int totalCtxEntities; /*!< Total number of different (process,context) entities used */ - unsigned int totalActions; unsigned int totalCtxAutStateVars; EntitiesForProc usedProducts; /*!< Entities used in products (per process) */ @@ -309,13 +303,6 @@ class SymRS BDD encContext(const EntitiesForProc &proc_entities); - /** - * @brief Complements an encoding of a given state by negating all the variables that are not set to true - * - * @return Returns the encoded state - */ - BDD compState(const BDD &state) const; - BDD compContext(const BDD &context) const; std::string decodedRctSysStateToStr(const BDD &state); diff --git a/reactics-bdd/test.rs b/reactics-bdd/test.drs similarity index 100% rename from reactics-bdd/test.rs rename to reactics-bdd/test.drs diff --git a/tests/expected/tgc4_mc.txt b/tests/expected/tgc4_mc.txt new file mode 100644 index 0000000..a1ae75c --- /dev/null +++ b/tests/expected/tgc4_mc.txt @@ -0,0 +1,8 @@ +Using BDD-based Bounded Model Checking +Formula (((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) AND EF(E< proc3.allowed >X(proc3.in))) holds +Using BDD-based Bounded Model Checking +Formula EF((((proc0.approach AND proc1.approach) AND proc2.approach) AND proc3.approach)) holds +Using BDD-based Bounded Model Checking +Formula AG((proc0.in IMPLIES K[proc0](((~proc1.in AND ~proc2.in) AND ~proc3.in)))) holds +Using BDD-based Bounded Model Checking +Formula AG((proc0.in IMPLIES C[proc0 proc1 proc2 proc3](((~proc1.in AND ~proc2.in) AND ~proc3.in)))) holds diff --git a/tests/expected/tgc4_print.txt b/tests/expected/tgc4_print.txt new file mode 100644 index 0000000..ccbcebb --- /dev/null +++ b/tests/expected/tgc4_print.txt @@ -0,0 +1,58 @@ +# Context entities: out allowed +# Reactions: + + . proc = "proc0": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc1": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc2": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc3": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + +# Context Automaton States: + = Init state: init + * init + * green + * red + * T +# Context Automaton Transitions: + * [init -> green]: { proc0={ out } proc1={ out } proc2={ out } proc3={ out } } + * [green -> red]: { proc0={ allowed } } proc0.req + * [green -> red]: { proc1={ allowed } } proc1.req + * [green -> red]: { proc2={ allowed } } proc2.req + * [green -> red]: { proc3={ allowed } } proc3.req + * [green -> green]: { proc0={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req) + * [green -> green]: { proc1={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req) + * [green -> green]: { proc2={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req) + * [green -> green]: { proc3={ } } (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req) + * [red -> green]: { proc0={ } } proc0.leave + * [red -> green]: { proc1={ } } proc1.leave + * [red -> green]: { proc2={ } } proc2.leave + * [red -> green]: { proc3={ } } proc3.leave + * [red -> red]: { proc0={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave) + * [red -> red]: { proc1={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave) + * [red -> red]: { proc2={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave) + * [red -> red]: { proc3={ } } (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave) + * [green -> T]: { } ~((((((((true OR proc0.req) OR proc1.req) OR proc2.req) OR proc3.req) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) OR (((~proc0.req AND ~proc1.req) AND ~proc2.req) AND ~proc3.req)) + * [red -> T]: { } ~((((((((true OR proc0.leave) OR proc1.leave) OR proc2.leave) OR proc3.leave) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) OR (((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) AND ~proc3.leave)) + * [T -> T]: { } diff --git a/tests/expected/tgc4_states.txt b/tests/expected/tgc4_states.txt new file mode 100644 index 0000000..bb515cf --- /dev/null +++ b/tests/expected/tgc4_states.txt @@ -0,0 +1,80 @@ +{ proc0={ req } proc1={ approach } proc2={ req } proc3={ out leave } } +{ proc0={ req } proc1={ req } proc2={ approach } proc3={ out leave } } +{ proc0={ req } proc1={ req } proc2={ req } proc3={ out leave } } +{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ out leave } } +{ proc0={ approach } proc1={ req } proc2={ req } proc3={ out leave } } +{ proc0={ approach } proc1={ approach } proc2={ req in } proc3={ approach } } +{ proc0={ approach } proc1={ req } proc2={ out leave } proc3={ req } } +{ proc0={ approach } proc1={ req } proc2={ req in } proc3={ approach } } +{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ out leave } } +{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ out leave } } +{ proc0={ req } proc1={ approach } proc2={ req in } proc3={ req } } +{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ out leave } } +{ proc0={ req } proc1={ approach } proc2={ req } proc3={ req in } } +{ proc0={ approach } proc1={ req } proc2={ req in } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ out leave } proc3={ approach } } +{ proc0={ req in } proc1={ approach } proc2={ req } proc3={ req } } +{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ req in } } +{ proc0={ req } proc1={ req } proc2={ out leave } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ out leave } proc3={ req } } +{ proc0={ req } proc1={ req } proc2={ req in } proc3={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ out leave } proc3={ req } } +{ proc0={ req } proc1={ req } proc2={ req in } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ req in } proc3={ approach } } +{ proc0={ approach } proc1={ req } proc2={ out leave } proc3={ approach } } +{ proc0={ req } proc1={ req } proc2={ out leave } proc3={ approach } } +{ proc0={ } proc1={ } proc2={ } proc3={ } } +{ proc0={ approach } proc1={ approach } proc2={ out leave } proc3={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ req in } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ req in } } +{ proc0={ req in } proc1={ req } proc2={ approach } proc3={ req } } +{ proc0={ req in } proc1={ approach } proc2={ approach } proc3={ approach } } +{ proc0={ req } proc1={ req in } proc2={ req } proc3={ req } } +{ proc0={ req in } proc1={ req } proc2={ approach } proc3={ approach } } +{ proc0={ req } proc1={ req } proc2={ req } proc3={ req in } } +{ proc0={ approach } proc1={ req } proc2={ req } proc3={ req in } } +{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ req in } } +{ proc0={ out leave } proc1={ req } proc2={ approach } proc3={ approach } } +{ proc0={ req in } proc1={ req } proc2={ req } proc3={ req } } +{ proc0={ out leave } proc1={ req } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ req } proc2={ approach } proc3={ req in } } +{ proc0={ req in } proc1={ approach } proc2={ approach } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ req } } +{ proc0={ req in } proc1={ approach } proc2={ req } proc3={ approach } } +{ proc0={ out leave } proc1={ approach } proc2={ req } proc3={ req } } +{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ req in } } +{ proc0={ out leave } proc1={ req } proc2={ approach } proc3={ req } } +{ proc0={ req } proc1={ out leave } proc2={ req } proc3={ req } } +{ proc0={ req } proc1={ approach } proc2={ req } proc3={ req } } +{ proc0={ out leave } proc1={ req } proc2={ req } proc3={ req } } +{ proc0={ approach } proc1={ req in } proc2={ approach } proc3={ approach } } +{ proc0={ out leave } proc1={ approach } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ req } proc2={ req } proc3={ req } } +{ proc0={ approach } proc1={ out leave } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ out leave } proc2={ req } proc3={ req } } +{ proc0={ req } proc1={ out leave } proc2={ approach } proc3={ req } } +{ proc0={ approach } proc1={ out leave } proc2={ approach } proc3={ req } } +{ proc0={ approach } proc1={ req in } proc2={ req } proc3={ req } } +{ proc0={ out leave } proc1={ approach } proc2={ req } proc3={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ req } } +{ proc0={ out leave } proc1={ approach } proc2={ approach } proc3={ req } } +{ proc0={ req in } proc1={ req } proc2={ req } proc3={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ approach } proc3={ req } } +{ proc0={ req } proc1={ req } proc2={ approach } proc3={ req } } +{ proc0={ approach } proc1={ req } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ approach } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ req in } proc2={ approach } proc3={ req } } +{ proc0={ approach } proc1={ approach } proc2={ req } proc3={ approach } } +{ proc0={ approach } proc1={ req in } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ approach } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ req in } proc2={ approach } proc3={ req } } +{ proc0={ approach } proc1={ req } proc2={ approach } proc3={ req } } +{ proc0={ req } proc1={ req in } proc2={ approach } proc3={ approach } } +{ proc0={ req } proc1={ out leave } proc2={ approach } proc3={ approach } } +{ proc0={ req } proc1={ req } proc2={ approach } proc3={ approach } } +{ proc0={ approach } proc1={ out leave } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ out leave } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ req in } proc2={ req } proc3={ approach } } +{ proc0={ req } proc1={ req } proc2={ req } proc3={ approach } } diff --git a/tests/expected/tgc_mc.txt b/tests/expected/tgc_mc.txt new file mode 100644 index 0000000..6c19266 --- /dev/null +++ b/tests/expected/tgc_mc.txt @@ -0,0 +1,8 @@ +Using BDD-based Bounded Model Checking +Formula ((EF(E< proc0.allowed >X(proc0.in)) AND EF(E< proc1.allowed >X(proc1.in))) AND EF(E< proc2.allowed >X(proc2.in))) holds +Using BDD-based Bounded Model Checking +Formula EF(((proc0.approach AND proc1.approach) AND proc2.approach)) holds +Using BDD-based Bounded Model Checking +Formula AG((proc0.in IMPLIES K[proc0]((~proc1.in AND ~proc2.in)))) holds +Using BDD-based Bounded Model Checking +Formula AG((proc0.in IMPLIES C[proc0 proc1 proc2]((~proc1.in AND ~proc2.in)))) holds diff --git a/tests/expected/tgc_print.txt b/tests/expected/tgc_print.txt new file mode 100644 index 0000000..0685301 --- /dev/null +++ b/tests/expected/tgc_print.txt @@ -0,0 +1,47 @@ +# Context entities: out allowed +# Reactions: + + . proc = "proc0": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc1": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc2": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + +# Context Automaton States: + = Init state: init + * init + * green + * red + * T +# Context Automaton Transitions: + * [init -> green]: { proc0={ out } proc1={ out } proc2={ out } } + * [green -> red]: { proc0={ allowed } } proc0.req + * [green -> red]: { proc1={ allowed } } proc1.req + * [green -> red]: { proc2={ allowed } } proc2.req + * [green -> green]: { proc0={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req) + * [green -> green]: { proc1={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req) + * [green -> green]: { proc2={ } } ((~proc0.req AND ~proc1.req) AND ~proc2.req) + * [red -> green]: { proc0={ } } proc0.leave + * [red -> green]: { proc1={ } } proc1.leave + * [red -> green]: { proc2={ } } proc2.leave + * [red -> red]: { proc0={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) + * [red -> red]: { proc1={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) + * [red -> red]: { proc2={ } } ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave) + * [green -> T]: { } ~((((((true OR proc0.req) OR proc1.req) OR proc2.req) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req)) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req)) OR ((~proc0.req AND ~proc1.req) AND ~proc2.req)) + * [red -> T]: { } ~((((((true OR proc0.leave) OR proc1.leave) OR proc2.leave) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)) OR ((~proc0.leave AND ~proc1.leave) AND ~proc2.leave)) + * [T -> T]: { } diff --git a/tests/expected/tgc_reactions.txt b/tests/expected/tgc_reactions.txt new file mode 100644 index 0000000..6b44f93 --- /dev/null +++ b/tests/expected/tgc_reactions.txt @@ -0,0 +1,23 @@ +# Reactions: + + . proc = "proc0": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc1": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + + . proc = "proc2": + * (R={ out },I={ },P={ approach }) + * (R={ approach },I={ req },P={ req }) + * (R={ allowed },I={ },P={ in }) + * (R={ in },I={ },P={ out leave }) + * (R={ req },I={ in },P={ req }) + diff --git a/tests/expected/tgc_states.txt b/tests/expected/tgc_states.txt new file mode 100644 index 0000000..d48f59b --- /dev/null +++ b/tests/expected/tgc_states.txt @@ -0,0 +1,32 @@ +{ proc0={ req in } proc1={ req } proc2={ req } } +{ proc0={ req in } proc1={ req } proc2={ approach } } +{ proc0={ req } proc1={ req in } proc2={ approach } } +{ proc0={ req in } proc1={ approach } proc2={ req } } +{ proc0={ req in } proc1={ approach } proc2={ approach } } +{ proc0={ req } proc1={ req in } proc2={ req } } +{ proc0={ approach } proc1={ req in } proc2={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ req in } } +{ proc0={ approach } proc1={ req in } proc2={ req } } +{ proc0={ approach } proc1={ out leave } proc2={ req } } +{ proc0={ req } proc1={ approach } proc2={ out leave } } +{ proc0={ req } proc1={ req } proc2={ req in } } +{ proc0={ approach } proc1={ req } proc2={ req } } +{ proc0={ approach } proc1={ req } proc2={ req in } } +{ proc0={ out leave } proc1={ req } proc2={ req } } +{ proc0={ req } proc1={ approach } proc2={ req in } } +{ proc0={ req } proc1={ out leave } proc2={ approach } } +{ proc0={ approach } proc1={ out leave } proc2={ approach } } +{ proc0={ req } proc1={ req } proc2={ out leave } } +{ proc0={ req } proc1={ out leave } proc2={ req } } +{ proc0={ } proc1={ } proc2={ } } +{ proc0={ req } proc1={ approach } proc2={ req } } +{ proc0={ out leave } proc1={ req } proc2={ approach } } +{ proc0={ approach } proc1={ req } proc2={ out leave } } +{ proc0={ approach } proc1={ approach } proc2={ req } } +{ proc0={ req } proc1={ req } proc2={ approach } } +{ proc0={ out leave } proc1={ approach } proc2={ req } } +{ proc0={ approach } proc1={ req } proc2={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ approach } } +{ proc0={ approach } proc1={ approach } proc2={ out leave } } +{ proc0={ out leave } proc1={ approach } proc2={ approach } } +{ proc0={ req } proc1={ approach } proc2={ approach } } diff --git a/tests/expected/trivial_print.txt b/tests/expected/trivial_print.txt new file mode 100644 index 0000000..ad83c3e --- /dev/null +++ b/tests/expected/trivial_print.txt @@ -0,0 +1,17 @@ +# Context entities: e1 e4 +# Reactions: + + . proc = "m": + * (R={ e1 e4 },I={ e2 },P={ e1 e2 }) + * (R={ e2 },I={ e4 },P={ e1 e4 e3 }) + * (R={ e1 e3 },I={ e2 },P={ e1 e2 }) + * (R={ e3 },I={ e2 },P={ e1 }) + +# Context Automaton States: + = Init state: s0 + * s0 + * s1 +# Context Automaton Transitions: + * [s0 -> s1]: { m={ e1 e4 } } + * [s1 -> s1]: { m={ } } + * [s1 -> s1]: { m={ e4 } } diff --git a/tests/expected/trivial_reactions.txt b/tests/expected/trivial_reactions.txt new file mode 100644 index 0000000..0149240 --- /dev/null +++ b/tests/expected/trivial_reactions.txt @@ -0,0 +1,8 @@ +# Reactions: + + . proc = "m": + * (R={ e1 e4 },I={ e2 },P={ e1 e2 }) + * (R={ e2 },I={ e4 },P={ e1 e4 e3 }) + * (R={ e1 e3 },I={ e2 },P={ e1 e2 }) + * (R={ e3 },I={ e2 },P={ e1 }) + diff --git a/tests/expected/trivial_states.txt b/tests/expected/trivial_states.txt new file mode 100644 index 0000000..53dc9d6 --- /dev/null +++ b/tests/expected/trivial_states.txt @@ -0,0 +1,3 @@ +{ m={ e1 e4 e3 } } +{ m={ e1 e2 } } +{ m={ } } diff --git a/tests/run_tests.sh b/tests/run_tests.sh new file mode 100755 index 0000000..b64a847 --- /dev/null +++ b/tests/run_tests.sh @@ -0,0 +1,69 @@ +#!/usr/bin/env bash + +# Regression test harness for ReactICS BDD module +# Compares current output against saved expected output + +set -uo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" +REACTICS="$ROOT_DIR/reactics-bdd/reactics" +EXPECTED_DIR="$SCRIPT_DIR/expected" + +PASS=0 +FAIL=0 +ERRORS="" + +run_test() { + local name="$1" + local expected_file="$2" + shift 2 + local actual + actual=$("$@" 2>&1) || true + local expected + expected=$(cat "$expected_file") + + if [[ "$actual" == "$expected" ]]; then + echo " PASS: $name" + ((PASS++)) + else + echo " FAIL: $name" + diff <(echo "$expected") <(echo "$actual") | head -20 + ((FAIL++)) + ERRORS="$ERRORS\n - $name" + fi +} + +echo "Running ReactICS regression tests..." +echo + +# --- tgc.drs tests --- +echo "[tgc]" +run_test "tgc print" "$EXPECTED_DIR/tgc_print.txt" "$REACTICS" -P examples/bdd/tgc.drs +run_test "tgc reactions" "$EXPECTED_DIR/tgc_reactions.txt" "$REACTICS" -r examples/bdd/tgc.drs +run_test "tgc states" "$EXPECTED_DIR/tgc_states.txt" "$REACTICS" -s examples/bdd/tgc.drs +run_test "tgc mc (f1-f4)" "$EXPECTED_DIR/tgc_mc.txt" \ + bash -c 'for f in f1 f2 f3 f4; do '"$REACTICS"' -c $f examples/bdd/tgc.drs 2>&1; done' + +echo +echo "[trivial]" +run_test "trivial print" "$EXPECTED_DIR/trivial_print.txt" "$REACTICS" -P reactics-bdd/in/trivial.drs +run_test "trivial reactions" "$EXPECTED_DIR/trivial_reactions.txt" "$REACTICS" -r reactics-bdd/in/trivial.drs +run_test "trivial states" "$EXPECTED_DIR/trivial_states.txt" "$REACTICS" -s reactics-bdd/in/trivial.drs + +echo +echo "[tgc4]" +run_test "tgc4 print" "$EXPECTED_DIR/tgc4_print.txt" "$REACTICS" -P examples/bdd/tgc4.drs +run_test "tgc4 states" "$EXPECTED_DIR/tgc4_states.txt" "$REACTICS" -s examples/bdd/tgc4.drs +run_test "tgc4 mc (f1-f4)" "$EXPECTED_DIR/tgc4_mc.txt" \ + bash -c 'for f in f1 f2 f3 f4; do '"$REACTICS"' -c $f examples/bdd/tgc4.drs 2>&1; done' + +echo +echo "================================" +echo "Results: $PASS passed, $FAIL failed" +if [[ $FAIL -gt 0 ]]; then + echo -e "Failures:$ERRORS" + exit 1 +else + echo "All tests passed." +fi