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

Test harness & some refactoring

Browse Source
This commit is contained in:
Artur Meski
2026-04-10 14:06:08 +01:00
parent 363446821e
commit 5df8d6aeb9
46 changed files with 478 additions and 305 deletions
Download Patch File Download Diff File Expand all files Collapse all files

0
examples/bdd/tgc.rs → examples/bdd/tgc.drs
View File

70
examples/bdd/tgc4.drs Normal file
View File

@@ -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( 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 ) ) };
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) ) };

7
reactics-bdd/ctx_aut.cc
View File

@@ -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)

3
reactics-bdd/ctx_aut.hh
View File

@@ -12,10 +12,7 @@
#include <vector>
#include <string>
#include <cstdlib>
// #include "rs.hh"
#include "types.hh"
// #include "options.hh"
// #include "stateconstr.hh"
using std::cout;
using std::endl;

2
reactics-bdd/drs_benchmark.sh
View File

@@ -1,6 +1,6 @@
#!/bin/sh
TMPINPUT="tmp_$RANDOM$RANDOM.rs"
TMPINPUT="tmp_$RANDOM$RANDOM.drs"
CMD="./reactics -B"

49
reactics-bdd/formrsctlk.cc
View File

@@ -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);
}

46
reactics-bdd/formrsctlk.hh
View File

@@ -9,7 +9,6 @@
#include <iostream>
#include <string>
#include <cassert>
// #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<Entity_f> Action_f;
// typedef vector<Action_f> ActionsVec_f;
typedef std::set<std::string> 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;
}

0
reactics-bdd/in/hsr.rs → reactics-bdd/in/hsr.drs
View File

0
reactics-bdd/in/hsr_ca.rs → reactics-bdd/in/hsr_ca.drs
View File

0
reactics-bdd/in/hsr_drs.rs → reactics-bdd/in/hsr_drs.drs
View File

0
reactics-bdd/in/old_syntax/bc32.rs → reactics-bdd/in/old_syntax/bc32.drs
View File

0
reactics-bdd/in/old_syntax/bc8.rs → reactics-bdd/in/old_syntax/bc8.drs
View File

0
reactics-bdd/in/old_syntax/coffee.rs → reactics-bdd/in/old_syntax/coffee.drs
View File

0
reactics-bdd/in/old_syntax/expr.rs → reactics-bdd/in/old_syntax/expr.drs
View File

0
reactics-bdd/in/old_syntax/simple_I1.rs → reactics-bdd/in/old_syntax/simple_I1.drs
View File

0
reactics-bdd/in/old_syntax/test.rs → reactics-bdd/in/old_syntax/test.drs
View File

0
reactics-bdd/in/old_syntax/u1.rs → reactics-bdd/in/old_syntax/u1.drs
View File

0
reactics-bdd/in/old_syntax/u2.rs → reactics-bdd/in/old_syntax/u2.drs
View File

6
reactics-bdd/in/scripts/bench_bc.sh
View File

@@ -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

6
reactics-bdd/in/scripts/bench_mutex.sh
View File

@@ -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

6
reactics-bdd/in/scripts/bench_pipe.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark_abs1.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark_abs1_PT.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark_bc.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark_mutex.sh
View File

@@ -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

6
reactics-bdd/in/scripts/benchmark_mutex_PT.sh
View File

@@ -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

0
reactics-bdd/in/trivial.rs → reactics-bdd/in/trivial.drs
View File

12
reactics-bdd/mc.cc
View File

@@ -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<size_t>(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();

17
reactics-bdd/reactics.cc
View File

@@ -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)

48
reactics-bdd/rs.cc
View File

@@ -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)

1
reactics-bdd/rs.hh
View File

@@ -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);

108
reactics-bdd/symrs.cc
View File

@@ -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);
}

13
reactics-bdd/symrs.hh
View File

@@ -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<BDDvec> *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);

0
reactics-bdd/test.rs → reactics-bdd/test.drs
View File

8
tests/expected/tgc4_mc.txt Normal file
View File

@@ -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

58
tests/expected/tgc4_print.txt Normal file
View File

@@ -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]: { }

80
tests/expected/tgc4_states.txt Normal file
View File

@@ -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 } }

8
tests/expected/tgc_mc.txt Normal file
View File

@@ -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

47
tests/expected/tgc_print.txt Normal file
View File

@@ -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]: { }

23
tests/expected/tgc_reactions.txt Normal file
View File

@@ -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 })

32
tests/expected/tgc_states.txt Normal file
View File

@@ -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 } }

17
tests/expected/trivial_print.txt Normal file
View File

@@ -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 } }

8
tests/expected/trivial_reactions.txt Normal file
View File

@@ -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 })

3
tests/expected/trivial_states.txt Normal file
View File

@@ -0,0 +1,3 @@
{ m={ e1 e4 e3 } }
{ m={ e1 e2 } }
{ m={ } }

69
tests/run_tests.sh Executable file
View File

@@ -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