From 5df8d6aeb9d9c803df34508ee4ceeb88b0277326 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 14:06:08 +0100 Subject: [PATCH 1/7] 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 From 6bddf4bf3867d14f8255d684b94e9ab866dc1ed3 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 14:24:37 +0100 Subject: [PATCH 2/7] Tests for Python/SMT --- TESTING.md | 55 +++++ tests/run_all_tests.sh | 27 +++ tests/test_smt.py | 501 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 583 insertions(+) create mode 100644 TESTING.md create mode 100755 tests/run_all_tests.sh create mode 100644 tests/test_smt.py diff --git a/TESTING.md b/TESTING.md new file mode 100644 index 0000000..e0abb66 --- /dev/null +++ b/TESTING.md @@ -0,0 +1,55 @@ +# Testing ReactICS + +## Prerequisites + +- **BDD module**: compiled (`./reactics setup` or `make` in `reactics-bdd/`) +- **SMT module**: Python 3 with `z3-solver` and `pytest` installed + +``` +pip install z3-solver pytest +``` + +## Running all tests + +``` +bash tests/run_all_tests.sh +``` + +This runs both the BDD and SMT test suites in sequence. + +## BDD tests + +``` +bash tests/run_tests.sh +``` + +10 regression tests that run the compiled `reactics-bdd/reactics` binary +against example `.drs` files and compare output to saved baselines in +`tests/expected/`. Covers: + +- Parsed system printing (`-P`) +- Reaction listing (`-r`) +- Reachable state enumeration (`-s`) +- RSCTLK model checking (`-c`) for properties f1--f4 + +Input files: `examples/bdd/tgc.drs`, `examples/bdd/tgc4.drs`, +`reactics-bdd/in/trivial.drs`. + +To update baselines after an intentional output change, delete the +relevant file in `tests/expected/` and re-run; the test will regenerate it. + +## SMT tests + +``` +python3 -m pytest tests/test_smt.py -v +``` + +23 pytest tests exercising the Python API directly. Organised by layer: + +- **Data model** -- ReactionSystem, concentrations, context automata, + formula construction (BagDescription, rsLTL) +- **SmtCheckerRS** -- basic reachability (no concentrations) +- **SmtCheckerRSC** -- reachability and rsLTL model checking with + concentrations (chain reaction, heat shock response) +- **SmtCheckerRSCParam** -- parametric verification +- **RSC-to-RS translation** -- verifying the translated system diff --git a/tests/run_all_tests.sh b/tests/run_all_tests.sh new file mode 100755 index 0000000..747d926 --- /dev/null +++ b/tests/run_all_tests.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash + +# Runs all ReactICS regression tests (BDD + SMT) + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" + +cd "$ROOT_DIR" + +failed=0 + +echo "========== BDD Tests ==========" +echo +bash "$SCRIPT_DIR/run_tests.sh" || failed=1 + +echo +echo "========== SMT Tests (pytest) ==========" +echo +python3 -m pytest "$SCRIPT_DIR/test_smt.py" -v || failed=1 + +echo +if [[ $failed -eq 0 ]]; then + echo "All test suites passed." +else + echo "Some tests FAILED." + exit 1 +fi diff --git a/tests/test_smt.py b/tests/test_smt.py new file mode 100644 index 0000000..17f1b02 --- /dev/null +++ b/tests/test_smt.py @@ -0,0 +1,501 @@ +""" +Regression tests for the ReactICS SMT module. + +Tests the Python API directly: reaction system construction, +context automata, and SMT-based verification (reachability + rsLTL). +""" + +import sys +import os +import io +from contextlib import redirect_stdout + +# Add reactics-smt to the path +sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..", "reactics-smt")) + +from z3 import sat, unsat +from rs import ( + ReactionSystem, + ContextAutomaton, + ReactionSystemWithConcentrations, + ContextAutomatonWithConcentrations, + ReactionSystemWithConcentrationsParam, + ReactionSystemWithAutomaton, +) +from smt import SmtCheckerRS, SmtCheckerRSC, SmtCheckerRSCParam +from logics import Formula_rsLTL, BagDescription +from rsltl_shortcuts import ltl_F, bag_entity, param_entity, param_And + + +# --------------------------------------------------------------------------- +# Helpers +# --------------------------------------------------------------------------- + +def run_silent(fn, *args, **kwargs): + """Run a function with stdout suppressed, return its result.""" + with redirect_stdout(io.StringIO()): + return fn(*args, **kwargs) + + +# --------------------------------------------------------------------------- +# Data model tests +# --------------------------------------------------------------------------- + +class TestReactionSystem: + def test_add_entities(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + assert rs.background_set == ["a", "b"] + assert rs.get_entity_id("a") == 0 + assert rs.get_entity_id("b") == 1 + assert rs.get_entity_name(0) == "a" + + def test_add_reaction(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + rs.add_bg_set_entity("c") + rs.add_reaction(["a"], ["b"], ["c"]) + assert len(rs.reactions) == 1 + reactants, inhibitors, products = rs.reactions[0] + assert reactants == [0] + assert inhibitors == [1] + assert products == [2] + + def test_reactions_by_product(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + rs.add_reaction(["a"], [], ["b"]) + rbp = rs.get_reactions_by_product() + assert 1 in rbp # entity id for "b" + assert len(rbp[1]) == 1 + + def test_duplicate_entity_raises(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + try: + rs.add_bg_set_entity("a") + assert False, "Should have raised" + except RuntimeError: + pass + + +class TestReactionSystemWithConcentrations: + def test_add_entity_with_concentration(self): + rs = ReactionSystemWithConcentrations() + rs.add_bg_set_entity(("x", 3)) + rs.add_bg_set_entity(("y", 5)) + assert rs.background_set == ["x", "y"] + assert rs.get_max_concentration_level(0) == 3 + assert rs.get_max_concentration_level(1) == 5 + + def test_add_reaction_with_concentrations(self): + rs = ReactionSystemWithConcentrations() + rs.add_bg_set_entity(("a", 2)) + rs.add_bg_set_entity(("b", 1)) + rs.add_reaction([("a", 1)], [], [("b", 1)]) + assert len(rs.reactions) == 1 + + def test_meta_reactions(self): + rs = ReactionSystemWithConcentrations() + rs.add_bg_set_entity(("e", 3)) + rs.add_bg_set_entity(("inc", 1)) + rs.add_reaction_inc("e", "inc", [("e", 1)], [("e", 3)]) + e_id = rs.get_entity_id("e") + assert e_id in rs.meta_reactions + assert rs.meta_reactions[e_id][0][0] == "inc" + + +class TestContextAutomaton: + def test_states_and_transitions(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + ca = ContextAutomaton(rs) + ca.add_init_state("s0") + ca.add_state("s1") + assert ca.get_init_state_id() == 0 + assert ca.get_state_id("s1") == 1 + ca.add_transition("s0", ["a"], "s1") + ca.add_transition("s1", [], "s1") + assert len(ca.transitions) == 2 + + def test_invalid_transition_raises(self): + rs = ReactionSystem() + rs.add_bg_set_entity("a") + ca = ContextAutomaton(rs) + ca.add_init_state("s0") + try: + ca.add_transition("s0", ["a"], "nonexistent") + assert False, "Should have raised" + except RuntimeError: + pass + + +class TestContextAutomatonWithConcentrations: + def test_transitions_with_concentrations(self): + rs = ReactionSystemWithConcentrations() + rs.add_bg_set_entity(("a", 2)) + rs.add_bg_set_entity(("b", 1)) + ca = ContextAutomatonWithConcentrations(rs) + ca.add_init_state("s0") + ca.add_state("s1") + ca.add_transition("s0", [("a", 2)], "s1") + ca.add_transition("s1", [], "s1") + assert len(ca.transitions) == 2 + + +# --------------------------------------------------------------------------- +# Formula construction tests +# --------------------------------------------------------------------------- + +class TestFormulas: + def test_bag_description(self): + b = BagDescription.f_entity("x") + assert str(b) == "x" + b_gt = b > 0 + assert ">" in str(b_gt) + + def test_rsltl_formula(self): + f = Formula_rsLTL.f_F( + BagDescription.f_TRUE(), + BagDescription.f_entity("x") > 0, + ) + assert "F" in str(f) + + def test_combined_formula(self): + f = Formula_rsLTL.f_G( + BagDescription.f_TRUE(), + Formula_rsLTL.f_Implies( + BagDescription.f_entity("a") == 1, + Formula_rsLTL.f_F( + BagDescription.f_TRUE(), + BagDescription.f_entity("b") > 0, + ), + ), + ) + assert "G" in str(f) + assert "F" in str(f) + + +# --------------------------------------------------------------------------- +# Verification tests: SmtCheckerRS (basic, no concentrations) +# --------------------------------------------------------------------------- + +def _build_simple_rs(): + """A minimal RS for testing: a -> b -> c with context automaton.""" + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + rs.add_bg_set_entity("c") + rs.add_reaction(["a"], [], ["b"]) + rs.add_reaction(["b"], [], ["c"]) + + ca = ContextAutomaton(rs) + ca.add_init_state("s0") + ca.add_state("s1") + ca.add_transition("s0", ["a"], "s1") + ca.add_transition("s1", [], "s1") + + return ReactionSystemWithAutomaton(rs, ca) + + +class TestSmtCheckerRS: + def test_reachability_sat(self): + rsa = _build_simple_rs() + checker = SmtCheckerRS(rsa) + run_silent( + checker.check_reachability, + ["c"], + print_witness=False, + print_time=False, + print_mem=False, + ) + # After finding SAT, solver state should be satisfiable + assert checker.solver.check() == sat + + def test_reachability_unreachable(self): + """Entity 'a' is never produced, so it shouldn't be reachable as a final state.""" + rs = ReactionSystem() + rs.add_bg_set_entity("a") + rs.add_bg_set_entity("b") + rs.add_reaction(["a"], [], ["b"]) + + ca = ContextAutomaton(rs) + ca.add_init_state("s0") + ca.add_state("s1") + # Context provides 'a' initially, then nothing + ca.add_transition("s0", ["a"], "s1") + ca.add_transition("s1", [], "s1") + + rsa = ReactionSystemWithAutomaton(rs, ca) + checker = SmtCheckerRS(rsa) + + # 'b' is reachable (produced from 'a') + run_silent( + checker.check_reachability, + ["b"], + print_witness=False, + print_time=False, + print_mem=False, + ) + assert checker.solver.check() == sat + + +# --------------------------------------------------------------------------- +# Verification tests: SmtCheckerRSC (with concentrations) +# --------------------------------------------------------------------------- + +def _build_chain_rsc(chain_len=2, max_conc=2): + """Build a chain reaction system with concentrations.""" + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("inc", 1)) + r.add_bg_set_entity(("dec", 1)) + + for i in range(1, chain_len + 1): + r.add_bg_set_entity(("e_" + str(i), max_conc)) + + for i in range(1, chain_len + 1): + ent = "e_" + str(i) + r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, max_conc)]) + r.add_reaction_dec(ent, "dec", [(ent, 1)], []) + if i < chain_len: + r.add_reaction([(ent, max_conc)], [], [("e_" + str(i + 1), 1)]) + + r.add_reaction( + [("e_" + str(chain_len), max_conc)], + [("dec", 1)], + [("e_" + str(chain_len), max_conc)], + ) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("init") + c.add_state("working") + c.add_transition("init", [("e_1", 1), ("inc", 1)], "working") + c.add_transition("working", [("inc", 1)], "working") + + return ReactionSystemWithAutomaton(r, c) + + +class TestSmtCheckerRSC: + def test_chain_reachability_sat(self): + """Chain(2,2): e_2=2 should be reachable at level 3.""" + rc = _build_chain_rsc(2, 2) + checker = SmtCheckerRSC(rc) + prop = ([("e_2", 2)], []) + run_silent( + checker.check_reachability, + prop, + print_witness=False, + print_time=False, + print_mem=False, + max_level=10, + ) + assert checker.solver.check() == sat + assert checker.current_level == 3 + + def test_chain_reachability_longer(self): + """Chain(3,2): e_3=2 should be reachable at level 5.""" + rc = _build_chain_rsc(3, 2) + checker = SmtCheckerRSC(rc) + prop = ([("e_3", 2)], []) + run_silent( + checker.check_reachability, + prop, + print_witness=False, + print_time=False, + print_mem=False, + max_level=10, + ) + assert checker.solver.check() == sat + assert checker.current_level == 5 + + def test_rsltl_finally(self): + """Check rsLTL F formula on chain(2,2).""" + rc = _build_chain_rsc(2, 2) + checker = SmtCheckerRSC(rc) + form = Formula_rsLTL.f_F( + BagDescription.f_entity("inc") > 0, + BagDescription.f_entity("e_2") >= 2, + ) + run_silent( + checker.check_rsltl, + formula=form, + print_witness=False, + print_time=False, + print_mem=False, + ) + assert checker.solver.check() == sat + assert checker.current_level == 3 + + def test_rsltl_finally_fast(self): + """Chain(2,2), F(e_1==2): should be SAT at level 1.""" + rc = _build_chain_rsc(2, 2) + checker = SmtCheckerRSC(rc) + form = Formula_rsLTL.f_F( + BagDescription.f_entity("inc") > 0, + BagDescription.f_entity("e_1") == 2, + ) + run_silent( + checker.check_rsltl, + formula=form, + print_witness=False, + print_time=False, + print_mem=False, + ) + assert checker.solver.check() == sat + assert checker.current_level == 1 + + def test_rsltl_next_until(self): + """Chain(2,2), X[TRUE](e_1 > 0 U[inc > 0] e_2 > 0): SAT at level 2.""" + rc = _build_chain_rsc(2, 2) + checker = SmtCheckerRSC(rc) + form = Formula_rsLTL.f_X( + BagDescription.f_TRUE(), + Formula_rsLTL.f_U( + BagDescription.f_entity("inc") > 0, + BagDescription.f_entity("e_1") > 0, + BagDescription.f_entity("e_2") > 0, + ), + ) + run_silent( + checker.check_rsltl, + formula=form, + print_witness=False, + print_time=False, + print_mem=False, + ) + assert checker.solver.check() == sat + assert checker.current_level == 2 + + +# --------------------------------------------------------------------------- +# Verification tests: SmtCheckerRSC on heat shock response +# --------------------------------------------------------------------------- + +def _build_heat_shock(): + """Heat shock response model.""" + stress_temp = 42 + max_temp = 50 + + r = ReactionSystemWithConcentrations() + for e in [("hsp", 1), ("hsf", 1), ("hsf2", 1), ("hsf3", 1), ("hse", 1), + ("mfp", 1), ("prot", 1), ("hsf3:hse", 1), ("hsp:mfp", 1), + ("hsp:hsf", 1), ("temp", max_temp), ("heat", 1), ("cool", 1)]: + r.add_bg_set_entity(e) + + r.add_reaction([("hsf", 1)], [("hsp", 1)], [("hsf3", 1)]) + r.add_reaction([("hsf", 1), ("hsp", 1), ("mfp", 1)], [], [("hsf3", 1)]) + r.add_reaction([("hsf3", 1)], [("hse", 1), ("hsp", 1)], [("hsf", 1)]) + r.add_reaction([("hsf3", 1), ("hsp", 1), ("mfp", 1)], [("hse", 1)], [("hsf", 1)]) + r.add_reaction([("hsf3", 1), ("hse", 1)], [("hsp", 1)], [("hsf3:hse", 1)]) + r.add_reaction([("hsp", 1), ("hsf3", 1), ("mfp", 1), ("hse", 1)], [], [("hsf3:hse", 1)]) + r.add_reaction([("hse", 1)], [("hsf3", 1)], [("hse", 1)]) + r.add_reaction([("hsp", 1), ("hsf3", 1), ("hse", 1)], [("mfp", 1)], [("hse", 1)]) + r.add_reaction([("hsf3:hse", 1)], [("hsp", 1)], [("hsp", 1), ("hsf3:hse", 1)]) + r.add_reaction([("hsp", 1), ("mfp", 1), ("hsf3:hse", 1)], [], [("hsp", 1), ("hsf3:hse", 1)]) + r.add_reaction([("hsf", 1), ("hsp", 1)], [("mfp", 1)], [("hsp:hsf", 1)]) + r.add_reaction([("hsp:hsf", 1), ("temp", stress_temp)], [], [("hsf", 1), ("hsp", 1)]) + r.add_reaction([("hsp:hsf", 1)], [("temp", stress_temp)], [("hsp:hsf", 1)]) + r.add_reaction([("hsp", 1), ("hsf3:hse", 1)], [("mfp", 1)], [("hse", 1), ("hsp:hsf", 1)]) + r.add_reaction([("temp", stress_temp), ("prot", 1)], [], [("mfp", 1), ("prot", 1)]) + r.add_reaction([("prot", 1)], [("temp", stress_temp)], [("prot", 1)]) + r.add_reaction([("hsp", 1), ("mfp", 1)], [], [("hsp:mfp", 1)]) + r.add_reaction([("mfp", 1)], [("hsp", 1)], [("mfp", 1)]) + r.add_reaction([("hsp:mfp", 1)], [], [("hsp", 1), ("prot", 1)]) + + r.add_reaction_inc("temp", "heat", [("temp", 1)], [("temp", max_temp)]) + r.add_reaction_dec("temp", "cool", [("temp", 1)], []) + r.add_permanency("temp", [("heat", 1), ("cool", 1)]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("0") + c.add_state("1") + c.add_transition("0", [("hsf", 1), ("prot", 1), ("hse", 1), ("temp", 35)], "1") + c.add_transition("1", [("cool", 1)], "1") + c.add_transition("1", [("heat", 1)], "1") + c.add_transition("1", [], "1") + + return ReactionSystemWithAutomaton(r, c) + + +class TestHeatShockResponse: + def test_mfp_reachable(self): + """mfp should be reachable at level 9.""" + rc = _build_heat_shock() + checker = SmtCheckerRSC(rc) + prop = ([("mfp", 1)], []) + run_silent( + checker.check_reachability, + prop, + print_witness=False, + print_time=False, + print_mem=False, + max_level=40, + ) + assert checker.solver.check() == sat + assert checker.current_level == 9 + + +# --------------------------------------------------------------------------- +# Verification tests: SmtCheckerRSCParam (parametric) +# --------------------------------------------------------------------------- + +def _build_parametric_overview(): + """Parametric example from doc/overview.py.""" + prs = ReactionSystemWithConcentrationsParam() + for ec in [("a", 3), ("b", 2), ("c", 1), ("h", 1)]: + prs.add_bg_set_entity(ec) + + lda = prs.get_param("lda") + prs.add_reaction([("a", 1)], [("h", 1)], [("b", 2)]) + prs.add_reaction(lda, [("h", 1)], [("c", 1)]) + + ca = ContextAutomatonWithConcentrations(prs) + ca.add_init_state("0") + ca.add_state("1") + ca.add_transition("0", [("a", 3)], "1") + ca.add_transition("1", [], "1") + ca.add_transition("1", [("h", 1)], "1") + + return ReactionSystemWithAutomaton(prs, ca), lda + + +class TestSmtCheckerRSCParam: + def test_parametric_sat(self): + """Parametric overview: F[h==0](c>0) should be SAT at level 2.""" + rc, lda = _build_parametric_overview() + pc = param_entity(lda, "a") == 0 + f = ltl_F(bag_entity("h") == 0, "c") + + checker = SmtCheckerRSCParam(rc, optimise=True) + run_silent( + checker.check_rsltl, + formulae_list=[f], + param_constr=pc, + ) + # The parametric checker uses path-based solving; + # after SAT the solver should be satisfiable + assert checker.solver.check() == sat + + +# --------------------------------------------------------------------------- +# RS translation tests (RSC -> RS) +# --------------------------------------------------------------------------- + +class TestRSCtoRSTranslation: + def test_translated_system_reachability(self): + """Chain(2,2) translated to plain RS: e_2#2 should be reachable.""" + rc = _build_chain_rsc(2, 2) + orc = rc.get_ordinary_reaction_system_with_automaton() + checker = SmtCheckerRS(orc) + run_silent( + checker.check_reachability, + ["e_2#2"], + print_witness=False, + print_time=False, + print_mem=False, + ) + assert checker.solver.check() == sat From 554b34afcfd8620ca63e4ebb37c7ba806051bd0b Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 14:30:46 +0100 Subject: [PATCH 3/7] Refactoring: Python/SMT --- reactics-smt/rs/context_automaton.py | 12 ++--- .../context_automaton_with_concentrations.py | 9 ++-- reactics-smt/rs/extended_context_automaton.py | 2 +- reactics-smt/rs/reaction_system.py | 7 +-- .../rs/reaction_system_with_concentrations.py | 47 ++----------------- ...action_system_with_concentrations_param.py | 18 ++----- reactics-smt/rs_testing.py | 2 - reactics-smt/rssmt.py | 1 - reactics-smt/smt/__init__.py | 1 - reactics-smt/smt/smt_checker_rs.py | 2 +- reactics-smt/smt/smt_checker_rsc.py | 3 -- reactics-smt/smt/smt_checker_rsc_param.py | 3 -- 12 files changed, 20 insertions(+), 87 deletions(-) diff --git a/reactics-smt/rs/context_automaton.py b/reactics-smt/rs/context_automaton.py index 6d0a084..3b29e68 100644 --- a/reactics-smt/rs/context_automaton.py +++ b/reactics-smt/rs/context_automaton.py @@ -55,10 +55,7 @@ def get_init_state_name(self): return self._states[self._init_state] def is_state(self, name): - if name in self._states: - return True - else: - return False + return name in self._states def get_state_id(self, name): try: @@ -78,10 +75,7 @@ def print_states(self): print(state) def is_valid_rs_set(self, elements): - if set(elements).issubset(self._reaction_system.background_set): - return True - else: - return False + return set(elements).issubset(self._reaction_system.background_set) def is_valid_context(self, context): return self.is_valid_rs_set(context) @@ -95,7 +89,7 @@ def get_set_of_ids(self, elements): return new_set def add_transition(self, src, context_set, dst): - if not type(context_set) is set and not type(context_set) is list: + if not isinstance(context_set, (set, list)): print("Contexts set must be of type set or list") if not self.is_valid_context(context_set): diff --git a/reactics-smt/rs/context_automaton_with_concentrations.py b/reactics-smt/rs/context_automaton_with_concentrations.py index 14b0271..f702df1 100644 --- a/reactics-smt/rs/context_automaton_with_concentrations.py +++ b/reactics-smt/rs/context_automaton_with_concentrations.py @@ -9,12 +9,9 @@ def __init__(self, reaction_system): super(ContextAutomatonWithConcentrations, self).__init__(reaction_system) def is_valid_context(self, context): - if set([e for e, lvl in context]).issubset( + return set(e for e, lvl in context).issubset( self._reaction_system.background_set - ): - return True - else: - return False + ) def context2str(self, ctx): if len(ctx) == 0: @@ -26,7 +23,7 @@ def context2str(self, ctx): return s def add_transition(self, src, context_set, dst): - if not type(context_set) is set and not type(context_set) is list: + if not isinstance(context_set, (set, list)): print("Contexts set must be of type set or list") if not self.is_valid_context(context_set): diff --git a/reactics-smt/rs/extended_context_automaton.py b/reactics-smt/rs/extended_context_automaton.py index bae9ce2..502cb77 100644 --- a/reactics-smt/rs/extended_context_automaton.py +++ b/reactics-smt/rs/extended_context_automaton.py @@ -70,7 +70,7 @@ def add_transition(self, src, actions, ctx_reaction, dst): ctx_reactants, ctx_inhibitors, ctx_products = ctx_reaction - if not type(ctx_products) is set and not type(ctx_products) is list: + if not isinstance(ctx_products, (set, list)): print("Contexts set (context products) must be of type set or list") if not self.is_valid_rs_set(ctx_reactants): diff --git a/reactics-smt/rs/reaction_system.py b/reactics-smt/rs/reaction_system.py index ad10a9f..e1d55fc 100644 --- a/reactics-smt/rs/reaction_system.py +++ b/reactics-smt/rs/reaction_system.py @@ -43,11 +43,8 @@ def add_bg_set_entities(self, elements): self.add_bg_set_entity(e) def is_in_background_set(self, entity): - """Checks if the given name is valid wrt the background set=""" - if entity in self.background_set: - return True - else: - return False + """Checks if the given name is valid wrt the background set""" + return entity in self.background_set def get_entity_id(self, name): try: diff --git a/reactics-smt/rs/reaction_system_with_concentrations.py b/reactics-smt/rs/reaction_system_with_concentrations.py index 9bdeb28..00967c8 100644 --- a/reactics-smt/rs/reaction_system_with_concentrations.py +++ b/reactics-smt/rs/reaction_system_with_concentrations.py @@ -18,9 +18,9 @@ def __init__(self): def add_bg_set_entity(self, e): name = "" def_max_conc = -1 - if type(e) is tuple and len(e) == 2: + if isinstance(e, tuple) and len(e) == 2: name, def_max_conc = e - elif type(e) is str: + elif isinstance(e, str): name = e print("\nWARNING: no maximal concentration level specified for:", e, "\n") else: @@ -46,18 +46,10 @@ def get_max_concentration_level(self, e): def is_valid_entity_with_concentration(self, e): """Sanity check for entities with concentration""" - if type(e) is tuple: - if len(e) == 2 and type(e[1]) is int: - return True + if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int): + return True - if type(e) is list: - if len(e) == 2 and type(e[1]) is int: - return True - - print("FATAL. Invalid entity+concentration: {:s}".format(e)) - exit(1) - - return False + raise RuntimeError("Invalid entity+concentration: " + repr(e)) def get_state_ids(self, state): """Returns entities of the given state without levels""" @@ -415,33 +407,4 @@ def e_value(i): return rs -class ReactionSystemWithAutomaton(object): - def __init__(self, reaction_system, context_automaton): - self.rs = reaction_system - self.ca = context_automaton - - def show(self, soft=False): - self.rs.show(soft) - self.ca.show() - - def is_with_concentrations(self): - if not isinstance(self.rs, ReactionSystemWithConcentrations): - return False - if not isinstance(self.ca, ContextAutomatonWithConcentrations): - return False - return True - - def sanity_check(self): - pass - - def get_ordinary_reaction_system_with_automaton(self): - if not self.is_with_concentrations(): - raise RuntimeError("Not RS/CA with concentrations") - - ors = self.rs.get_reaction_system() - oca = self.ca.get_automaton_with_flat_contexts(ors) - - return ReactionSystemWithAutomaton(ors, oca) - - # EOF diff --git a/reactics-smt/rs/reaction_system_with_concentrations_param.py b/reactics-smt/rs/reaction_system_with_concentrations_param.py index ab628dc..1e52492 100644 --- a/reactics-smt/rs/reaction_system_with_concentrations_param.py +++ b/reactics-smt/rs/reaction_system_with_concentrations_param.py @@ -34,9 +34,9 @@ def __init__(self): def add_bg_set_entity(self, e): name = "" def_max_conc = -1 - if type(e) is tuple and len(e) == 2: + if isinstance(e, tuple) and len(e) == 2: name, def_max_conc = e - elif type(e) is str: + elif isinstance(e, str): name = e print("\nWARNING: no maximal concentration level specified for:", e, "\n") else: @@ -80,18 +80,10 @@ def get_max_concentration_level(self, e): def is_valid_entity_with_concentration(self, e): """Sanity check for entities with concentration""" - if type(e) is tuple: - if len(e) == 2 and type(e[1]) is int: - return True - - if type(e) is list: - if len(e) == 2 and type(e[1]) is int: - return True - - print("FATAL. Invalid entity+concentration: {:s}".format(e)) - exit(1) + if isinstance(e, (tuple, list)) and len(e) == 2 and isinstance(e[1], int): + return True - return False + raise RuntimeError("Invalid entity+concentration: " + repr(e)) def is_valid_concentration_for_entity(self, entity, level): """Checks the concentration level for entity""" diff --git a/reactics-smt/rs_testing.py b/reactics-smt/rs_testing.py index 727dcce..c492227 100644 --- a/reactics-smt/rs_testing.py +++ b/reactics-smt/rs_testing.py @@ -1,12 +1,10 @@ from rs import * from smt import * -import rs_examples from logics import * from rsltl_shortcuts import * from itertools import chain, combinations -import sys import resource def powerset(iterable,N=None): diff --git a/reactics-smt/rssmt.py b/reactics-smt/rssmt.py index 4ebf902..95398ec 100755 --- a/reactics-smt/rssmt.py +++ b/reactics-smt/rssmt.py @@ -11,7 +11,6 @@ from rs import * from smt import * import sys -import rs_examples import rs_testing from colour import * diff --git a/reactics-smt/smt/__init__.py b/reactics-smt/smt/__init__.py index dbce176..af9a852 100644 --- a/reactics-smt/smt/__init__.py +++ b/reactics-smt/smt/__init__.py @@ -1,4 +1,3 @@ -# from smt.smt_checker import SmtChecker from smt.smt_checker_rs import SmtCheckerRS from smt.smt_checker_rsc import SmtCheckerRSC from smt.smt_checker_rsc_param import SmtCheckerRSCParam diff --git a/reactics-smt/smt/smt_checker_rs.py b/reactics-smt/smt/smt_checker_rs.py index 88242a4..57ee035 100644 --- a/reactics-smt/smt/smt_checker_rs.py +++ b/reactics-smt/smt/smt_checker_rs.py @@ -267,7 +267,7 @@ def check_reachability( ): """Main testing function""" - if not type(state) is tuple: + if not isinstance(state, tuple): state = (state, []) if print_time: diff --git a/reactics-smt/smt/smt_checker_rsc.py b/reactics-smt/smt/smt_checker_rsc.py index 9b4a795..7934e73 100644 --- a/reactics-smt/smt/smt_checker_rsc.py +++ b/reactics-smt/smt/smt_checker_rsc.py @@ -11,9 +11,6 @@ from logics import rsLTL_Encoder -# def simplify(x): -# return x - class SmtCheckerRSC(object): def __init__(self, rsca): diff --git a/reactics-smt/smt/smt_checker_rsc_param.py b/reactics-smt/smt/smt_checker_rsc_param.py index 2d48fcf..c345025 100644 --- a/reactics-smt/smt/smt_checker_rsc_param.py +++ b/reactics-smt/smt/smt_checker_rsc_param.py @@ -14,9 +14,6 @@ from rs.reaction_system_with_concentrations_param import ParameterObj, is_param -# def simplify(x): -# return x - def z3_max(a, b): return If(a > b, a, b) From f319d09ad7fbd4016dc94f7182b578c1038f08c6 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 17:52:22 +0100 Subject: [PATCH 4/7] Generators: cleanup --- examples/bdd/generators/gen_asm.py | 103 ++++++++++++ examples/bdd/generators/gen_drs.py | 35 ++-- examples/bdd/generators/gen_tgc.py | 151 +++++++++--------- .../bdd/generators/old_syntax/gen_abstract.py | 62 +++++++ examples/bdd/generators/old_syntax/gen_bc.py | 88 ++++++++++ .../bdd/generators/old_syntax/gen_mutex.py | 71 ++++++++ reactics-bdd/in/scripts/gen_abstract1.py | 47 ------ reactics-bdd/in/scripts/gen_asm.py | 93 ----------- reactics-bdd/in/scripts/gen_bc.py | 118 -------------- reactics-bdd/in/scripts/gen_mutex.py | 76 --------- reactics-bdd/in/scripts/gen_tgc_sc.py | 117 -------------- 11 files changed, 422 insertions(+), 539 deletions(-) create mode 100644 examples/bdd/generators/gen_asm.py create mode 100644 examples/bdd/generators/old_syntax/gen_abstract.py create mode 100644 examples/bdd/generators/old_syntax/gen_bc.py create mode 100644 examples/bdd/generators/old_syntax/gen_mutex.py delete mode 100755 reactics-bdd/in/scripts/gen_abstract1.py delete mode 100755 reactics-bdd/in/scripts/gen_asm.py delete mode 100755 reactics-bdd/in/scripts/gen_bc.py delete mode 100755 reactics-bdd/in/scripts/gen_mutex.py delete mode 100755 reactics-bdd/in/scripts/gen_tgc_sc.py diff --git a/examples/bdd/generators/gen_asm.py b/examples/bdd/generators/gen_asm.py new file mode 100644 index 0000000..0f2e169 --- /dev/null +++ b/examples/bdd/generators/gen_asm.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +""" +Generator for the Assembly-line (ASM) benchmark. + +Produces a distributed reaction system modelling an assembly line +where N sequential processes pass activation tokens. Each process +cycles through entities a -> y,b -> c -> d, and the final process +signals 'done'. Uses a context automaton for scheduling. +""" + +import argparse + + +OPTIONS = "options { use-context-automaton; make-progressive; };\n" + +PROC_TEMPLATE = """ + proc{i} {{ + {{{{a}}, {{s}} -> {{y}}}}; + {{{{y}}, {{s}} -> {{y}}}}; + {{{{a}}, {{s}} -> {{b}}}}; + {{{{b}}, {{s}} -> {{c}}}}; + {{{{c}}, {{s}} -> {{d}}}}; + {{{{d,y}}, {{s}} -> {{dy}}}}; + }}; +""" + +FINAL_PROC = """ + procFinal { + {{done}, {s} -> {done}}; + }; +""" + +CA_TEMPLATE = """ +context-automaton {{ + states {{ init, act }}; + init-state {{ init }}; + transitions {{ +{transitions} + }}; +}}; +""" + +PROPERTY_TEMPLATE = '\nrsctlk-property {{ {name} : {formula} }};\n' + + +def generate(n): + out = OPTIONS + out += "\nreactions {\n" + for i in range(1, n + 1): + out += PROC_TEMPLATE.format(i=i) + out += FINAL_PROC + out += "};\n" + + indent = 8 * " " + transitions = "" + + # init -> act: first process gets activated + transitions += "{indent}{{ proc1={{a}} }}: init -> act;\n".format(indent=indent) + + # act -> act: process stays idle (dy not produced) + for i in range(1, n + 1): + transitions += "{indent}{{ proc{i}={{}} }}: act -> act : ~proc{i}.dy;\n".format( + indent=indent, i=i) + + # act -> act: next process gets activated when previous produces 'dy' + for i in range(2, n + 1): + transitions += "{indent}{{ proc{i}={{a}} }}: act -> act : proc{prev}.dy;\n".format( + indent=indent, i=i, prev=i - 1) + + # act -> act: final process signals done when all have produced 'dy' + all_dy = " AND ".join("proc{}.dy".format(i) for i in range(1, n + 1)) + transitions += "{indent}{{ procFinal={{done}} }}: act -> act : {guard};\n".format( + indent=indent, guard=all_dy) + + out += CA_TEMPLATE.format(transitions=transitions) + + # f1: the assembly line eventually completes + out += PROPERTY_TEMPLATE.format(name="f1", formula="EF( procFinal.done )") + + # f2: last process knows its predecessor has produced 'y' + f2 = "AG( proc{n}.d IMPLIES K[proc{n}]( proc{prev}.y ) )".format(n=n, prev=n - 1) + out += PROPERTY_TEMPLATE.format(name="f2", formula=f2) + + # x1: negation of f1 (sanity check -- should also hold) + out += PROPERTY_TEMPLATE.format(name="x1", formula="EF( ~procFinal.done )") + + return out + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("n", type=int, help="number of processes (must be > 1)") + args = parser.parse_args() + + if args.n < 2: + parser.error("number of processes must be > 1") + + print(generate(args.n)) + + +if __name__ == "__main__": + main() diff --git a/examples/bdd/generators/gen_drs.py b/examples/bdd/generators/gen_drs.py index c076f7a..c1f22a7 100755 --- a/examples/bdd/generators/gen_drs.py +++ b/examples/bdd/generators/gen_drs.py @@ -1,6 +1,15 @@ #!/usr/bin/env python3 +""" +Generator for the DRS (Distributed Reaction Systems) epistemic benchmark. + +Produces a distributed reaction system with epistemic properties +(knowledge operators). The system models signal transduction cascades +with configurable depth (x), number of components (y), threshold (z), +and context automaton variant (a or b). +""" import sys +import argparse import itertools @@ -272,18 +281,20 @@ def generate_formula(self): def main(): - if len(sys.argv) < 1 + 4: - print(f"Usage: {sys.argv[0]} ") - print("\twhere x,y,z >= 2 and y >= z") - print("\tAut: a, b") - sys.exit(1) - - g = DRSGenerator( - x=int(sys.argv[1]), - y=int(sys.argv[2]), - z=int(sys.argv[3]), - aut=sys.argv[4], - ) + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("x", type=int, help="cascade depth (>= 2)") + parser.add_argument("y", type=int, help="number of components (>= 2, >= z)") + parser.add_argument("z", type=int, help="threshold (>= 2, <= y)") + parser.add_argument("aut", choices=["a", "b"], help="automaton variant") + args = parser.parse_args() + + if args.x < 2 or args.y < 2 or args.z < 2: + parser.error("x, y, z must all be >= 2") + if args.y < args.z: + parser.error("y must be >= z") + + DRSGenerator(x=args.x, y=args.y, z=args.z, aut=args.aut) if __name__ == "__main__": diff --git a/examples/bdd/generators/gen_tgc.py b/examples/bdd/generators/gen_tgc.py index d4bfcf0..32b8654 100755 --- a/examples/bdd/generators/gen_tgc.py +++ b/examples/bdd/generators/gen_tgc.py @@ -1,13 +1,20 @@ -#!/usr/bin/env python - -from sys import argv,exit +#!/usr/bin/env python3 +""" +Generator for the Traffic Guard Controller (TGC) benchmark. -OPTIONS_STR = """ -options { use-context-automaton; make-progressive; }; +Produces a distributed reaction system where N processes compete +for access to a shared resource, governed by a context automaton +with green/red states. Generates RSCTLK properties for liveness, +reachability, and mutual exclusion (epistemic). """ -PROC_STR = """ - proc{:d} {{ +import argparse + + +OPTIONS = "options { use-context-automaton; make-progressive; };\n" + +PROC_TEMPLATE = """ + proc{i} {{ {{{{out}}, {{}} -> {{approach}}}}; {{{{approach}}, {{req}} -> {{req}}}}; {{{{allowed}}, {{}} -> {{in}}}}; @@ -16,102 +23,94 @@ }}; """ -CA_STR = """ +CA_TEMPLATE = """ context-automaton {{ states {{ init, green, red }}; init-state {{ init }}; transitions {{ -{:s} +{transitions} }}; }}; """ -PROPERTY_STR = """ -rsctlk-property {{ {:s} : {:s} }}; -""" - +PROPERTY_TEMPLATE = '\nrsctlk-property {{ {name} : {formula} }};\n' -################################################################# -if len(argv) < 1: - print("Usage: {:s} ".format(argv[0])) - exit(100) +def conj(fmt, indices, sep=" AND "): + return sep.join(fmt.format(i=i) for i in indices) -n = int(argv[1]) -assert n > 1, "number of proc must be > 1" +def generate(n): + out = OPTIONS + out += "\nreactions {\n" + for i in range(n): + out += PROC_TEMPLATE.format(i=i) + out += "};\n" -out = "" + indent = 8 * " " + transitions = "" -out += OPTIONS_STR -out += "reactions {\n" -for i in range(n): - out += PROC_STR.format(i) -out += "};\n" + # init -> green: all processes start with 'out' + transitions += indent + "{ " + transitions += " ".join("proc{:d}={{out}}".format(i) for i in range(n)) + transitions += " }: init -> green;\n" -transitions = "" + # green -> red: a process requests + for i in range(n): + transitions += "{indent}{{ proc{i}={{allowed}} }}: green -> red : proc{i}.req;\n".format( + indent=indent, i=i) -init_trans = 8*" " + "{ " -for i in range(n): - init_trans += "proc{:d}={{out}} ".format(i) -init_trans += "}: init -> green;\n" -transitions += init_trans + # green -> green: no requests pending + no_req = conj("~proc{i}.req", range(n)) + for i in range(n): + transitions += "{indent}{{ proc{i}={{}} }}: green -> green : {guard};\n".format( + indent=indent, i=i, guard=no_req) -for i in range(n): - transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i) + # red -> green: a process leaves + for i in range(n): + transitions += "{indent}{{ proc{i}={{}} }}: red -> green : proc{i}.leave;\n".format( + indent=indent, i=i) -no_req_cond = "~proc0.req" -for i in range(1, n): - no_req_cond += " AND ~proc{:d}.req".format(i) + # red -> red: no process leaves + no_leave = conj("~proc{i}.leave", range(n)) + for i in range(n): + transitions += "{indent}{{ proc{i}={{}} }}: red -> red : {guard};\n".format( + indent=indent, i=i, guard=no_leave) -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond) + out += CA_TEMPLATE.format(transitions=transitions) -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i) + # f1: each process can eventually enter + f1 = conj("EF( EX( proc{i}.in ) )", range(n)) + out += PROPERTY_TEMPLATE.format(name="f1", formula=f1) -no_leave_cond = "~proc0.leave" -for i in range(1, n): - no_leave_cond += " AND ~proc{:d}.leave".format(i) + # f2: all processes can simultaneously approach + f2 = "EF( " + conj("proc{i}.approach", range(n)) + " )" + out += PROPERTY_TEMPLATE.format(name="f2", formula=f2) -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond) + # f3: mutual exclusion (knowledge) + others_not_in = conj("~proc{i}.in", range(1, n)) + f3 = "AG( proc0.in IMPLIES K[proc0]({}) )".format(others_not_in) + out += PROPERTY_TEMPLATE.format(name="f3", formula=f3) -out += CA_STR.format(transitions) + # f4: mutual exclusion (common knowledge) + all_agents = conj("proc{i}", range(n), sep=",") + f4 = "AG( proc0.in IMPLIES C[{}]({}) )".format(all_agents, others_not_in) + out += PROPERTY_TEMPLATE.format(name="f4", formula=f4) -## f1 -#formula = "EF( proc0.in )" -#out += PROPERTY_STR.format("f1",formula) + return out -# 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("f1",formula) -# f2 -formula = "EF( proc0.approach" -for i in range(1, n): - formula += " AND proc{:d}.approach".format(i) -formula += " )" -out += PROPERTY_STR.format("f2",formula) +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("n", type=int, help="number of processes (must be > 1)") + args = parser.parse_args() -# 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("f3",formula) + if args.n < 2: + parser.error("number of processes must be > 1") -# f4 -subf = "~proc1.in" -for i in range(2, n): - subf += " AND ~proc{:d}.in".format(i) -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("f4",formula) + print(generate(args.n)) -print(out) +if __name__ == "__main__": + main() diff --git a/examples/bdd/generators/old_syntax/gen_abstract.py b/examples/bdd/generators/old_syntax/gen_abstract.py new file mode 100644 index 0000000..f7302ce --- /dev/null +++ b/examples/bdd/generators/old_syntax/gen_abstract.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +""" +Generator for the Abstract Pipeline benchmark. + +Produces a reaction system modelling a pipeline of N modules, +each cycling through entities a -> y,b -> c -> d before passing +activation to the next module. The final reaction requires all +modules to have completed (all y_i present). + +NOTE: generates old-syntax input (context-entities, initial-contexts, +rsctl-property) which is not compatible with the current parser. +""" + +import argparse + + +def generate(n, variant): + out = "reactions {\n" + out += "\t{ {x},{s} -> {a1} };\n" + + for i in range(1, n + 1): + out += "\t{{ {{a{i}}},{{s}} -> {{y{i}}} }};\n".format(i=i) + out += "\t{{ {{a{i}}},{{s}} -> {{b{i}}} }};\n".format(i=i) + out += "\t{{ {{b{i}}},{{s}} -> {{c{i}}} }};\n".format(i=i) + out += "\t{{ {{c{i}}},{{s}} -> {{d{i}}} }};\n".format(i=i) + out += "\t{{ {{d{i},y{i}}},{{s}} -> {{a{j}}} }};\n".format(i=i, j=i + 1) + out += "\t{{ {{y{i}}},{{s}} -> {{y{i}}} }};\n".format(i=i) + + final_reactants = "a" + str(n + 1) + for i in range(1, n + 1): + final_reactants += ",y" + str(i) + out += "\t{{ {{{r}}},{{s}} -> {{r}} }};\n".format(r=final_reactants) + out += "}\n" + + if variant == 1: + out += "context-entities { s }\n" + elif variant == 2: + ctx = "s" + for i in range(1, n + 1): + if i % 2 == 0: + ctx += ",a" + str(i) + out += "context-entities {{ {} }}\n".format(ctx) + + out += "initial-contexts { {x} }\n" + out += "rsctl-property { E[{}]F(r) }\n" + + return out + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("n", type=int, help="number of pipeline modules") + parser.add_argument("variant", type=int, choices=[1, 2], + help="context variant (1: minimal, 2: extended)") + args = parser.parse_args() + + print(generate(args.n, args.variant)) + + +if __name__ == "__main__": + main() diff --git a/examples/bdd/generators/old_syntax/gen_bc.py b/examples/bdd/generators/old_syntax/gen_bc.py new file mode 100644 index 0000000..9941a89 --- /dev/null +++ b/examples/bdd/generators/old_syntax/gen_bc.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +""" +Generator for the Binary Counter (BC) benchmark. + +Produces a reaction system modelling an N-bit binary counter +with increment and decrement operations controlled via context +entities. Generates one of four RSCTL properties. + +NOTE: generates old-syntax input (context-entities, initial-contexts, +rsctl-property) which is not compatible with the current parser. +""" + +import argparse + +K = 8 # constant used by property 3 + + +def generate(n, prop): + out = "reactions {\n" + + # (1) no dec, no inc: bits persist + out += "\t# (1) no decrement, no increment\n" + for j in range(n): + out += "\t{{{{p{j}}},{{dec,inc}} -> {{p{j}}}}};\n".format(j=j) + + # (2) increment operation + out += "\n\t# (2) increment operation\n" + out += "\t{{inc},{dec,p0} -> {p0}};\n" + for j in range(1, n): + bits = ",".join("p" + str(k) for k in range(j)) + out += "\t{{{{inc,{bits}}},{{dec,p{j}}} -> {{p{j}}}}};\n".format(bits=bits, j=j) + + out += "\n\t# the more significant bits remain (inc)\n" + for j in range(n): + for k in range(j + 1, n): + out += "\t{{{{inc,p{k}}},{{dec,p{j}}} -> {{p{k}}}}};\n".format(j=j, k=k) + + # (3) decrement operation + out += "\n\t# (3) decrement operation\n" + for j in range(n): + bits = ",".join("p" + str(k) for k in range(j + 1)) + out += "\t{{{{dec}},{{inc,{bits}}} -> {{p{j}}}}};\n".format(bits=bits, j=j) + + out += "\n\t# the more significant bits remain (dec)\n" + for j in range(n): + for k in range(j + 1, n): + out += "\t{{{{dec,p{j},p{k}}},{{inc}} -> {{p{k}}}}};\n".format(j=j, k=k) + + out += "}\n\n" + out += "context-entities { inc,dec }\n" + out += "initial-contexts { {} }\n" + + if prop == 1: + all_neg = " AND ".join("~p" + str(i) for i in range(n)) + all_pos = " AND ".join("p" + str(i) for i in range(n)) + out += "rsctl-property {{ AG(({}) IMPLIES E[{{inc}},{{dec}}]F({})) }}\n".format( + all_neg, all_pos) + elif prop == 2: + all_pos = " AND ".join("p" + str(i) for i in range(n)) + all_neg = " AND ".join("~p" + str(i) for i in range(n)) + out += "rsctl-property {{ AG(({}) IMPLIES A[{{inc}}]X({})) }}\n".format( + all_pos, all_neg) + elif prop == 3: + parts = ["p" + str(i) for i in range(n - K)] + parts += ["~p" + str(i) for i in range(n - K, n)] + out += "rsctl-property {{ E[{{inc}}]F({}) }}\n".format(" AND ".join(parts)) + elif prop == 4: + out += "rsctl-property {{ AG( p{} IMPLIES EF ~p{} ) }}\n".format(n - 1, n - 1) + + return out + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("n", type=int, help="number of bits") + parser.add_argument("property", type=int, choices=[1, 2, 3, 4], + help="property to generate (1-4)") + args = parser.parse_args() + + if args.property == 3 and args.n < K + 1: + parser.error("n must be >= {} for property 3".format(K + 1)) + + print(generate(args.n, args.property)) + + +if __name__ == "__main__": + main() diff --git a/examples/bdd/generators/old_syntax/gen_mutex.py b/examples/bdd/generators/old_syntax/gen_mutex.py new file mode 100644 index 0000000..4027446 --- /dev/null +++ b/examples/bdd/generators/old_syntax/gen_mutex.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +""" +Generator for the Mutual Exclusion (Mutex) benchmark. + +Produces a reaction system modelling N processes competing for +exclusive access to a critical section, using activation signals, +request tokens, and a lock. Generates one of three RSCTL properties. + +NOTE: generates old-syntax input (context-entities, initial-contexts, +rsctl-property) which is not compatible with the current parser. +""" + +import argparse + + +def generate(n, formula): + out = "reactions {\n" + for i in range(n): + out += "\t{{{{out{i},act{i}}},{{}} -> {{request{i}}}}};\n".format(i=i) + out += "\t{{{{out{i}}},{{act{i}}} -> {{out{i}}}}};\n".format(i=i) + + for j in range(n): + if i != j: + out += "\t{{{{request{i},act{i},act{j}}},{{}} -> {{request{i}}}}};\n".format( + i=i, j=j) + + out += "\t{{{{request{i}}},{{act{i}}} -> {{request{i}}}}};\n".format(i=i) + + other_acts = ",".join("act" + str(j) for j in range(n) if i != j) + out += "\t{{{{request{i},act{i}}},{{{others},lock}} -> {{in{i},lock}}}};\n".format( + i=i, others=other_acts) + + out += "\t{{{{in{i},act{i}}},{{}} -> {{out{i},done}}}};\n".format(i=i) + out += "\t{{{{in{i}}},{{act{i}}} -> {{in{i}}}}};\n".format(i=i) + + out += "\t{{lock},{done} -> {lock}};\n" + out += "}\n" + + ctx_ents = ",".join("act" + str(i) for i in range(n)) + out += "context-entities {{ {} }}\n".format(ctx_ents) + + init_ents = ",".join("out" + str(i) for i in range(n)) + out += "initial-contexts {{ {{{}}} }}\n".format(init_ents) + + if formula == 1: + out += "rsctl-property { A[{act1}]F(in1) }\n" + elif formula == 2: + out += "rsctl-property { E[{act1}]F(in1) }\n" + elif formula == 3: + pairs = [] + for i in range(n): + for j in range(i + 1, n): + pairs.append("~(in{} AND in{})".format(i, j)) + out += "rsctl-property {{ AG({}) }}\n".format(" AND ".join(pairs)) + + return out + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("n", type=int, help="number of processes") + parser.add_argument("formula", type=int, choices=[1, 2, 3], + help="formula to generate (1: A[]F, 2: E[]F, 3: AG mutex)") + args = parser.parse_args() + + print(generate(args.n, args.formula)) + + +if __name__ == "__main__": + main() diff --git a/reactics-bdd/in/scripts/gen_abstract1.py b/reactics-bdd/in/scripts/gen_abstract1.py deleted file mode 100755 index 8112ae8..0000000 --- a/reactics-bdd/in/scripts/gen_abstract1.py +++ /dev/null @@ -1,47 +0,0 @@ -#!/usr/bin/env python - -from sys import argv,exit - -if len(argv) < 3: - print "Usage:", argv[0], " " - exit(100) - -n = int(argv[1]) -v = int(argv[2]) - -if not ( v > 0 and v < 3 ): - print "unsupported variant" - exit(100) - -print "reactions {" -s = "\t{ {x},{s} -> {a1} };\n" -print s - -for i in range(1,n+1): - s = "\t{ {a" + str(i) + "},{s} -> {y" + str(i) + "} };\n" - s += "\t{ {a" + str(i) + "},{s} -> {b" + str(i) + "} };\n" - s += "\t{ {b" + str(i) + "},{s} -> {c" + str(i) + "} };\n" - s += "\t{ {c" + str(i) + "},{s} -> {d" + str(i) + "} };\n" - s += "\t{ {d" + str(i) + ",y" + str(i) + "},{s} -> {a" + str(i+1) + "} };\n" - s += "\t{ {y" + str(i) + "},{s} -> {y" + str(i) + "} };\n" - print s - -s = "\t{ {a" + str(n+1) -for i in range(1,n+1): - s += ",y" + str(i) -s += "},{s} -> {r} };\n" -print s -print "}" - -if v == 1: - print "context-entities { s }" -elif v == 2: - s = "context-entities { s" - for i in range(1,n+1): - if i % 2 == 0: - s += ",a" + str(i) - s += " }" - print s - -print "initial-contexts { {x} }" -print "rsctl-property { E[{}]F(r) }" diff --git a/reactics-bdd/in/scripts/gen_asm.py b/reactics-bdd/in/scripts/gen_asm.py deleted file mode 100755 index a83a4e6..0000000 --- a/reactics-bdd/in/scripts/gen_asm.py +++ /dev/null @@ -1,93 +0,0 @@ -#!/usr/bin/env python - -from sys import argv,exit - -OPTIONS_STR = """ -options { use-context-automaton; make-progressive; }; -""" - -PROC_STR = """ - proc{:d} {{ - {{{{a}}, {{s}} -> {{y}}}}; - {{{{y}}, {{s}} -> {{y}}}}; - {{{{a}}, {{s}} -> {{b}}}}; - {{{{b}}, {{s}} -> {{c}}}}; - {{{{c}}, {{s}} -> {{d}}}}; - {{{{d,y}}, {{s}} -> {{dy}}}}; - }}; -""" - -FINAL_PROC = """ - procFinal { - {{done}, {s} -> {done}}; - }; -""" - -CA_STR = """ -context-automaton {{ - states {{ init, act }}; - init-state {{ init }}; - transitions {{ -{:s} - }}; -}}; -""" - -PROPERTY_STR = """ -rsctlk-property {{ {:s} : {:s} }}; -""" - - -################################################################# - -if len(argv) < 1: - print("Usage: {:s} ".format(argv[0])) - exit(100) - -n = int(argv[1]) - -assert n > 1, "number of proc must be > 1" - -out = "" - -out += OPTIONS_STR -out += "reactions {\n" -for i in range(1, n+1): - out += PROC_STR.format(i) - -out += FINAL_PROC -out += "};\n" - -transitions = "" - -init_trans = 8*" " + "{ proc1={a} }: init -> act;\n" -transitions += init_trans - -for i in range(1, n+1): - transitions += "{:s}{{ proc{:d}={{}} }}: act -> act : ~proc{:d}.dy;\n".format(8*" ", i, i, i) - -for i in range(2, n+1): - transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1) - -final_cond = "proc1.dy" -for i in range(2, n+1): - final_cond += " AND proc{:d}.dy".format(i) - -transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond) - -out += CA_STR.format(transitions) - -# f1 -formula = "EF( procFinal.done )" -out += PROPERTY_STR.format("f1",formula) - -# f2 -formula = "AG( proc{:d}.d IMPLIES K[proc{:d}]( proc{:d}.y ) )".format(n, n, n-1) -out += PROPERTY_STR.format("f2",formula) - -# x1 -formula = "EF( ~procFinal.done )" -out += PROPERTY_STR.format("x1",formula) - -print(out) - diff --git a/reactics-bdd/in/scripts/gen_bc.py b/reactics-bdd/in/scripts/gen_bc.py deleted file mode 100755 index 0e543ff..0000000 --- a/reactics-bdd/in/scripts/gen_bc.py +++ /dev/null @@ -1,118 +0,0 @@ -#!/usr/bin/env python2.7 - -from sys import argv,exit - - -if len(argv) < 3: - print "Usage:", argv[0], " " - exit(100) - -n = int(argv[1]) -property = int(argv[2]) - -K = 8 -if property == 3: - if n < K+1: - print "too small n" - exit(100) - -if not ( property >= 1 and property < 5 ): - print "property: 1-4" - exit(101) - -print "reactions {" - -# (1) no dec, no inc -print "\t# (1) no decrement, no increment" -for j in range(0,n): - print "\t{{p" + str(j) + "},{dec,inc} -> {p" + str(j) + "}};" - -# (2) increment -s = "\n\t# (2) increment operation\n" -s += "\t{{inc},{dec,p0} -> {p0}};\n" -for j in range(1,n): - s += "\t{{inc," - for k in range(0,j): - s += "p" + str(k) - if k < j-1: - s += "," - s += "},{dec,p" + str(j) + "} -> {p" + str(j) + "}};\n" - -print s - -print "\t# the more significant bits remain (inc)" -s = "" -for j in range(0,n): - for k in range(j+1,n): - s += "\t{{inc,p" + str(k) + "},{dec,p" + str(j) + "} -> {p" + str(k) + "}};\n" - -print s - -print "\t# (3) decrement operation" -s = "" -for j in range(0,n): - s += "\t{{dec},{inc," - for k in range(0,j+1): - s += "p" + str(k) - if k < j: - s += "," - s += "} -> {p" + str(j) + "}};\n" -print s - -print "\t# the more significant bits remain (dec)" -s = "" -for j in range(0,n): - for k in range(j+1,n): - s += "\t{{dec,p" + str(j) + ",p" + str(k) + "},{inc} -> {p" + str(k) + "}};\n" - -s += "}\n" -print s - -print "context-entities { inc,dec }" -print "initial-contexts { {} }" - -if property == 4: - print "rsctl-property { AG( p" + str(n-1) + " IMPLIES EF ~p" + str(n-1) + " ) }" -elif property == 1: - s = "rsctl-property { AG((" - for i in range(0,n): - s += "~p" + str(i) - if i < n-1: - s += " AND " - s += ") IMPLIES E[{inc},{dec}]F(" - for i in range(0,n): - s += "p" + str(i) - if i < n-1: - s += " AND " - - s += ")) }" - print s -elif property == 2: - s = "rsctl-property { AG((" - for i in range(0,n): - s += "p" + str(i) - if i < n-1: - s += " AND " - s += ") IMPLIES A[{inc}]X(" - for i in range(0,n): - s += "~p" + str(i) - if i < n-1: - s += " AND " - - s += ")) }" - print s - -elif property == 3: - s = "rsctl-property { E[{inc}]F(" - for i in range(0,n-K): - s += "p" + str(i) - if i < n-1: - s += " AND " - for i in range(n-K,n): - s += "~p" + str(i) - if i < n-1: - s += " AND " - s += ") }" - print s - - diff --git a/reactics-bdd/in/scripts/gen_mutex.py b/reactics-bdd/in/scripts/gen_mutex.py deleted file mode 100755 index 95337d5..0000000 --- a/reactics-bdd/in/scripts/gen_mutex.py +++ /dev/null @@ -1,76 +0,0 @@ -#!/usr/bin/env python - -from sys import argv,exit - - -if len(argv) < 3: - print "Usage:", argv[0], " " - exit(100) - -n = int(argv[1]) -f = int(argv[2]) - -if not ( f>0 and f<4 ): - print "unsupported formula" - exit(100) - -print "reactions {" -for i in range(0,n): - s = "\t{{out" + str(i) + ",act" + str(i) + "},{} -> {request" + str(i) + "}};\n" - s += "\t{{out" + str(i) + "},{act" + str(i) + "} -> {out" + str(i) + "}};\n" - for j in range(0,n): - if i != j: - s += "\t{{request" + str(i) + ",act" + str(i) + ",act" + str(j) + "},{} -> {request" + str(i) + "}};\n" - #s += "\t{{request" + str(i) + "},{" - #for j in range(0,n): - # s += "act" + str(j) - # if j < n-1: - # s += "," - #s += "} -> {request" + str(i) + "}};\n" - s += "\t{{request" + str(i) + "},{act" + str(i) + "} -> {request" + str(i) + "}};\n" - s += "\t{{request" + str(i) + ",act" + str(i) + "},{" - for j in range(0,n): - if i != j: - s += "act" + str(j) + "," - s += "lock} -> {in" + str(i) + ",lock}};\n" - s += "\t{{in" + str(i) + ",act" + str(i) + "},{} -> {out" + str(i) + ",done}};\n" - s += "\t{{in" + str(i) + "},{act" + str(i) + "} -> {in" + str(i) + "}};\n" - print s - -print "\t{{lock},{done} -> {lock}};" - -print "}" - -s = "context-entities {" -for i in range(0,n): - s += "act" + str(i) - if i < n-1: - s += "," -s += "}\n" -print s - -s = "initial-contexts { {" -for i in range(0,n): - s += "out" + str(i) - if i < n-1: - s += "," -s += "} }\n" -print s - -#print "rsctl-property { A[{act1}]G(A[{act1}]F(in1)) }" -if f == 1: - print "rsctl-property { A[{act1}]F(in1) }" -elif f == 2: - print "rsctl-property { E[{act1}]F(in1) }" -elif f == 3: - s = "rsctl-property { AG(" - for i in range(0,n): - for j in range(i+1,n): - s += "~(in" + str(i) + " AND in" + str(j) + ")" - if i < n-2: - s += " AND " - s += ") }" - print s -else: - exit(111) - diff --git a/reactics-bdd/in/scripts/gen_tgc_sc.py b/reactics-bdd/in/scripts/gen_tgc_sc.py deleted file mode 100755 index d4bfcf0..0000000 --- a/reactics-bdd/in/scripts/gen_tgc_sc.py +++ /dev/null @@ -1,117 +0,0 @@ -#!/usr/bin/env python - -from sys import argv,exit - -OPTIONS_STR = """ -options { use-context-automaton; make-progressive; }; -""" - -PROC_STR = """ - proc{:d} {{ - {{{{out}}, {{}} -> {{approach}}}}; - {{{{approach}}, {{req}} -> {{req}}}}; - {{{{allowed}}, {{}} -> {{in}}}}; - {{{{in}}, {{}} -> {{out,leave}}}}; - {{{{req}}, {{in}} -> {{req}}}}; - }}; -""" - -CA_STR = """ -context-automaton {{ - states {{ init, green, red }}; - init-state {{ init }}; - transitions {{ -{:s} - }}; -}}; -""" - -PROPERTY_STR = """ -rsctlk-property {{ {:s} : {:s} }}; -""" - - -################################################################# - -if len(argv) < 1: - print("Usage: {:s} ".format(argv[0])) - exit(100) - -n = int(argv[1]) - -assert n > 1, "number of proc must be > 1" - -out = "" - -out += OPTIONS_STR -out += "reactions {\n" -for i in range(n): - out += PROC_STR.format(i) -out += "};\n" - -transitions = "" - -init_trans = 8*" " + "{ " -for i in range(n): - init_trans += "proc{:d}={{out}} ".format(i) -init_trans += "}: init -> green;\n" -transitions += init_trans - -for i in range(n): - transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i) - -no_req_cond = "~proc0.req" -for i in range(1, n): - no_req_cond += " AND ~proc{:d}.req".format(i) - -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond) - -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i) - -no_leave_cond = "~proc0.leave" -for i in range(1, n): - no_leave_cond += " AND ~proc{:d}.leave".format(i) - -for i in range(n): - transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond) - -out += CA_STR.format(transitions) - -## f1 -#formula = "EF( proc0.in )" -#out += PROPERTY_STR.format("f1",formula) - -# 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("f1",formula) - -# f2 -formula = "EF( proc0.approach" -for i in range(1, n): - formula += " AND proc{:d}.approach".format(i) -formula += " )" -out += PROPERTY_STR.format("f2",formula) - -# 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("f3",formula) - -# f4 -subf = "~proc1.in" -for i in range(2, n): - subf += " AND ~proc{:d}.in".format(i) -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("f4",formula) - -print(out) - From e1f7a0e91a1f43603f5839c67283aede0c5dddfd Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 18:00:10 +0100 Subject: [PATCH 5/7] Test runner --- TESTING.md | 14 ++++++++-- run_tests.sh | 3 +++ tests/run_all_tests.sh | 60 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 74 insertions(+), 3 deletions(-) create mode 100755 run_tests.sh diff --git a/TESTING.md b/TESTING.md index e0abb66..1c99d4b 100644 --- a/TESTING.md +++ b/TESTING.md @@ -12,10 +12,10 @@ pip install z3-solver pytest ## Running all tests ``` -bash tests/run_all_tests.sh +./run_tests.sh ``` -This runs both the BDD and SMT test suites in sequence. +This runs the BDD, SMT, and generator test suites in sequence. ## BDD tests @@ -53,3 +53,13 @@ python3 -m pytest tests/test_smt.py -v concentrations (chain reaction, heat shock response) - **SmtCheckerRSCParam** -- parametric verification - **RSC-to-RS translation** -- verifying the translated system + +## Generator tests + +7 tests that run each generator (from `examples/bdd/generators/`), +feed the output into the BDD model checker, and verify the expected +verification result (holds / does not hold). + +Generators using old syntax (`examples/bdd/generators/old_syntax/`) +are not tested this way as they are not compatible with the current +parser. diff --git a/run_tests.sh b/run_tests.sh new file mode 100755 index 0000000..bc65fc7 --- /dev/null +++ b/run_tests.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# Run all ReactICS tests (BDD, SMT, generators) +exec bash "$(dirname "$0")/tests/run_all_tests.sh" "$@" diff --git a/tests/run_all_tests.sh b/tests/run_all_tests.sh index 747d926..bbfa9d3 100755 --- a/tests/run_all_tests.sh +++ b/tests/run_all_tests.sh @@ -1,24 +1,82 @@ #!/usr/bin/env bash -# Runs all ReactICS regression tests (BDD + SMT) +# Runs all ReactICS regression tests (BDD + SMT + generators) + +set -uo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" +REACTICS="$ROOT_DIR/reactics-bdd/reactics" +GENERATORS="$ROOT_DIR/examples/bdd/generators" cd "$ROOT_DIR" failed=0 +# --------------------------------------------------------------- echo "========== BDD Tests ==========" echo bash "$SCRIPT_DIR/run_tests.sh" || failed=1 +# --------------------------------------------------------------- echo echo "========== SMT Tests (pytest) ==========" echo python3 -m pytest "$SCRIPT_DIR/test_smt.py" -v || failed=1 +# --------------------------------------------------------------- +echo +echo "========== Generator Tests ==========" +echo + +gen_pass=0 +gen_fail=0 + +check_gen() { + local name="$1" + local gen_cmd="$2" + local property="$3" + local expected="$4" + + local tmpfile + tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs) + + eval "$gen_cmd" > "$tmpfile" 2>&1 + local result + result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true) + rm -f "$tmpfile" + + if [[ "$result" == "$expected" ]]; then + echo " PASS: $name" + ((gen_pass++)) + else + echo " FAIL: $name (expected '$expected', got '$result')" + ((gen_fail++)) + failed=1 + fi +} + +echo "[gen_tgc]" +check_gen "tgc(3) f1" "python3 $GENERATORS/gen_tgc.py 3" f1 "holds" +check_gen "tgc(3) f3" "python3 $GENERATORS/gen_tgc.py 3" f3 "holds" +check_gen "tgc(4) f2" "python3 $GENERATORS/gen_tgc.py 4" f2 "holds" + +echo +echo "[gen_asm]" +check_gen "asm(3) f1" "python3 $GENERATORS/gen_asm.py 3" f1 "holds" +check_gen "asm(3) f2" "python3 $GENERATORS/gen_asm.py 3" f2 "holds" + +echo +echo "[gen_drs]" +check_gen "drs(2,2,2,a) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 a" f0 "does not hold" +check_gen "drs(2,2,2,b) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 b" f0 "holds" + +echo +echo "Generator results: $gen_pass passed, $gen_fail failed" + +# --------------------------------------------------------------- echo +echo "================================" if [[ $failed -eq 0 ]]; then echo "All test suites passed." else From 54c8320a30eda167934952f6b5b90774197ca62b Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 18:11:36 +0100 Subject: [PATCH 6/7] CI tests --- .github/workflows/tests.yml | 38 +++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 .github/workflows/tests.yml diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml new file mode 100644 index 0000000..56735ef --- /dev/null +++ b/.github/workflows/tests.yml @@ -0,0 +1,38 @@ +name: Tests + +on: + push: + branches: [master, refactor] + pull_request: + branches: [master] + +jobs: + test: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y g++ make bison flex + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: "3.12" + + - name: Install Python dependencies + run: pip install z3-solver pytest + + - name: Build CUDD + working-directory: reactics-bdd + run: ./build_cudd.sh + + - name: Build ReactICS BDD module + working-directory: reactics-bdd + run: make + + - name: Run all tests + run: ./run_tests.sh From 38182de3077cf27012265a1d272501193c3a79fd Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 10 Apr 2026 18:13:31 +0100 Subject: [PATCH 7/7] CI tests: split --- .github/workflows/tests.yml | 69 ++++++++++++++++++++++++++++++++++--- 1 file changed, 65 insertions(+), 4 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 56735ef..6f61a61 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -7,9 +7,9 @@ on: branches: [master] jobs: - test: + bdd: + name: BDD tests runs-on: ubuntu-latest - steps: - uses: actions/checkout@v4 @@ -18,6 +18,23 @@ jobs: sudo apt-get update sudo apt-get install -y g++ make bison flex + - name: Build CUDD + working-directory: reactics-bdd + run: ./build_cudd.sh + + - name: Build ReactICS BDD module + working-directory: reactics-bdd + run: make + + - name: Run BDD tests + run: bash tests/run_tests.sh + + smt: + name: SMT tests + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up Python uses: actions/setup-python@v5 with: @@ -26,6 +43,21 @@ jobs: - name: Install Python dependencies run: pip install z3-solver pytest + - name: Run SMT tests + run: python3 -m pytest tests/test_smt.py -v + + generators: + name: Generator tests + runs-on: ubuntu-latest + needs: bdd + steps: + - uses: actions/checkout@v4 + + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y g++ make bison flex + - name: Build CUDD working-directory: reactics-bdd run: ./build_cudd.sh @@ -34,5 +66,34 @@ jobs: working-directory: reactics-bdd run: make - - name: Run all tests - run: ./run_tests.sh + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: "3.12" + + - name: Run generator tests + run: | + REACTICS="$PWD/reactics-bdd/reactics" + GENERATORS="$PWD/examples/bdd/generators" + failed=0 + check_gen() { + local name="$1" gen_cmd="$2" property="$3" expected="$4" + local tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs) + eval "$gen_cmd" > "$tmpfile" 2>&1 + local result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true) + rm -f "$tmpfile" + if [ "$result" = "$expected" ]; then + echo " PASS: $name" + else + echo " FAIL: $name (expected '$expected', got '$result')" + failed=1 + fi + } + check_gen "tgc(3) f1" "python3 $GENERATORS/gen_tgc.py 3" f1 "holds" + check_gen "tgc(3) f3" "python3 $GENERATORS/gen_tgc.py 3" f3 "holds" + check_gen "tgc(4) f2" "python3 $GENERATORS/gen_tgc.py 4" f2 "holds" + check_gen "asm(3) f1" "python3 $GENERATORS/gen_asm.py 3" f1 "holds" + check_gen "asm(3) f2" "python3 $GENERATORS/gen_asm.py 3" f2 "holds" + check_gen "drs(2,2,2,a) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 a" f0 "does not hold" + check_gen "drs(2,2,2,b) f0" "python3 $GENERATORS/gen_drs.py 2 2 2 b" f0 "holds" + exit $failed