diff --git a/formrsctl.cc b/formrsctl.cc index 7ca391e..45a9a5d 100644 --- a/formrsctl.cc +++ b/formrsctl.cc @@ -189,8 +189,8 @@ bool FormRSCTL::hasOper(Oper op) const else { bool result = false; - if (arg[0] != NULL) result = arg[0]->hasOper(op); - if (!result && arg[1] != NULL) result = arg[1]->hasOper(op); + if (arg[0] != nullptr) result = arg[0]->hasOper(op); + if (!result && arg[1] != nullptr) result = arg[1]->hasOper(op); return result; } } @@ -249,7 +249,7 @@ bool FormRSCTL::isERSCTL(void) const std::string FormRSCTL::getActionsStr(void) const { - if (actions != NULL) + if (actions != nullptr) { std::string r = "[ "; bool firstact = true; @@ -271,7 +271,7 @@ std::string FormRSCTL::getActionsStr(void) const r += " ]"; return r; } - else if (boolCtx != NULL) + else if (boolCtx != nullptr) { return "< " + boolCtx->toStr() + " >"; } @@ -285,11 +285,11 @@ void FormRSCTL::encodeActions(const SymRS *srs) { if (RSCTL_COND_ACT(oper)) { - if (actions_bdd != NULL) forgetActionsBDD(); + if (actions_bdd != nullptr) forgetActionsBDD(); actions_bdd = new BDD(srs->getBDDfalse()); - assert(actions != NULL || boolCtx != NULL); - assert(!(actions != NULL && boolCtx != NULL)); - if (actions != NULL) + assert(actions != nullptr || boolCtx != nullptr); + assert(!(actions != nullptr && boolCtx != nullptr)); + if (actions != nullptr) { for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act) { @@ -302,7 +302,7 @@ void FormRSCTL::encodeActions(const SymRS *srs) *actions_bdd += single_action; } } - else if (boolCtx != NULL) + else if (boolCtx != nullptr) { *actions_bdd = boolCtx->getBDD(srs); } diff --git a/formrsctl.hh b/formrsctl.hh index fbbd92d..eac1723 100644 --- a/formrsctl.hh +++ b/formrsctl.hh @@ -82,8 +82,8 @@ public: { oper = BCTX_PV; name = varName; - arg[0] = NULL; - arg[1] = NULL; + arg[0] = nullptr; + arg[1] = nullptr; } /** @@ -94,8 +94,8 @@ public: BoolContexts(bool val) { oper = BCTX_TF; tf = val; - arg[0] = NULL; - arg[1] = NULL; + arg[0] = nullptr; + arg[1] = nullptr; } /** @@ -105,7 +105,7 @@ public: assert(op == BCTX_NOT); oper = op; arg[0] = form1; - arg[1] = NULL; + arg[1] = nullptr; } /** @@ -132,12 +132,12 @@ public: return oper; } BoolContexts *getLeftSF(void) const { - assert(arg[0] != NULL); + assert(arg[0] != nullptr); return arg[0]; } BoolContexts *getRightSF(void) const { assert(BCTX_COND_2ARG(oper)); - assert(arg[1] != NULL); + assert(arg[1] != nullptr); return arg[1]; } }; @@ -162,12 +162,12 @@ public: FormRSCTL(std::string varName) { oper = RSCTL_PV; name = varName; - arg[0] = NULL; - arg[1] = NULL; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; - boolCtx = NULL; + arg[0] = nullptr; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** @@ -178,12 +178,12 @@ public: FormRSCTL(bool val) { oper = RSCTL_TF; tf = val; - arg[0] = NULL; - arg[1] = NULL; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; - boolCtx = NULL; + arg[0] = nullptr; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** @@ -195,41 +195,41 @@ public: oper = op; arg[0] = form1; arg[1] = form2; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; - boolCtx = NULL; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** * @brief Constructor for two-argument formula with action restrictions. */ FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) { - assert(acts != NULL); + assert(acts != nullptr); assert(RSCTL_COND_2ARG(op)); assert(RSCTL_COND_ACT(op)); oper = op; arg[0] = form1; arg[1] = form2; - bdd = NULL; + bdd = nullptr; actions = acts; - actions_bdd = NULL; - boolCtx = NULL; + actions_bdd = nullptr; + boolCtx = nullptr; } /** * @brief Constructor for two-argument formula with Boolean context restrictions. */ FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) { - assert(bctx != NULL); + assert(bctx != nullptr); assert(RSCTL_COND_2ARG(op)); assert(RSCTL_COND_ACT(op)); oper = op; arg[0] = form1; arg[1] = form2; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; boolCtx = bctx; } @@ -241,42 +241,42 @@ public: assert(!RSCTL_COND_ACT(op)); oper = op; arg[0] = form1; - arg[1] = NULL; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; - boolCtx = NULL; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** * @brief Constructor for one-argument formula with action restrictions. */ FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) { - assert(acts != NULL); + assert(acts != nullptr); assert(RSCTL_COND_1ARG(op)); assert(RSCTL_COND_ACT(op)); oper = op; arg[0] = form1; - arg[1] = NULL; - bdd = NULL; + arg[1] = nullptr; + bdd = nullptr; actions = acts; - actions_bdd = NULL; - boolCtx = NULL; + actions_bdd = nullptr; + boolCtx = nullptr; } /** * @brief Constructor for one-argument formula with Boolean context restrictions. */ FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) { - assert(bctx != NULL); + assert(bctx != nullptr); assert(RSCTL_COND_1ARG(op)); assert(RSCTL_COND_ACT(op)); oper = op; arg[0] = form1; - arg[1] = NULL; - bdd = NULL; - actions = NULL; - actions_bdd = NULL; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; boolCtx = bctx; } @@ -295,12 +295,12 @@ public: bool hasOper(Oper op) const; const BDD *getBDD(void) const { assert(oper == RSCTL_PV); - assert(bdd != NULL); + assert(bdd != nullptr); return bdd; } const BDD *getActionsBDD(void) const { assert(RSCTL_COND_ACT(oper)); - assert(actions_bdd != NULL); + assert(actions_bdd != nullptr); return actions_bdd; } Oper getOper(void) const { @@ -308,12 +308,12 @@ public: return oper; } FormRSCTL *getLeftSF(void) const { - assert(arg[0] != NULL); + assert(arg[0] != nullptr); return arg[0]; } FormRSCTL *getRightSF(void) const { assert(RSCTL_COND_2ARG(oper)); - assert(arg[1] != NULL); + assert(arg[1] != nullptr); return arg[1]; } std::string getActionsStr(void) const; @@ -324,7 +324,7 @@ public: void encodeEntities(const SymRS *srs); void encodeActions(const SymRS *srs); void forgetActionsBDD(void) { - if (actions_bdd != NULL) delete actions_bdd; + if (actions_bdd != nullptr) delete actions_bdd; } bool isERSCTL(void) const; }; diff --git a/macro.hh b/macro.hh index 0c133c7..4a78a70 100644 --- a/macro.hh +++ b/macro.hh @@ -1,6 +1,8 @@ #ifndef __MY_MACROS__ #define __MY_MACROS__ +#include + #define LINENUM std::cout << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << std::endl; /* Fatal error */ #define FERROR(s) \ @@ -14,16 +16,19 @@ } #define VERB(s) \ +assert(opts != nullptr); \ if (opts->verbose > 0) { \ std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } #define VERB_L2(s) \ +assert(opts != nullptr); \ if (opts->verbose > 1) { \ std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } #define VERB_L3(s) \ +assert(opts != nullptr); \ if (opts->verbose > 2) { \ std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } diff --git a/main.cc b/main.cc index 2e2927c..2f8e3f1 100644 --- a/main.cc +++ b/main.cc @@ -10,12 +10,10 @@ int main(int argc, char **argv) { - - - RctSys rs; - rsin_driver driver(&rs); + rsin_driver driver; Options *opts = new Options; + driver.setOptions(opts); bool show_reactions = false; bool rstl_model_checking = false; @@ -95,10 +93,8 @@ int main(int argc, char **argv) default: usage_error = true; } - } - - rs.setOptions(opts); - + } + std::string inputfile; if (optind < argc) { @@ -113,9 +109,9 @@ int main(int argc, char **argv) if (usage_error) { cout << endl - << " **********************************" << endl - << " **Reaction Systems Model Checker**" << endl - << " **********************************" << endl + << " ------------------------------------" << endl + << " -- Reaction Systems Model Checker --" << endl + << " ------------------------------------" << endl << endl << " Version: " << VERSION << endl << " Contact: " << AUTHOR << endl @@ -128,28 +124,30 @@ int main(int argc, char **argv) << endl #endif << " Usage: " << argv[0] << " [options] " << endl << endl - << " -b -- disable bounded model checking (BMC) heuristic" << endl - << " -c -- perform RSCTL model checking" << endl + << " TASKS:" << endl + << " -c -- perform RSCTL model checking" << endl //<< " -f K -- generate SMT input for the depth K" << endl - << " -p -- show progress (where possible)" << endl - << " -P -- print parsed system" << endl - << " -r -- print reactions" << endl - << " -s -- print the set of all the reachable states" << endl - << " -t -- print the set of all the reachable states with their successors" << endl - << " -x -- use partitioned transition relation (may use less memory)" << endl - << " -z -- use reordering of the BDD variables" << endl - << " -v -- verbose (can be used more than once to increase verbosity)" << endl + << " -P -- print parsed system" << endl + << " -r -- print reactions" << endl + << " -s -- print the set of all the reachable states" << endl + << " -t -- print the set of all the reachable states with their successors" << endl + << endl << " OTHER:" << endl + << " -b -- disable bounded model checking (BMC) heuristic" << endl + << " -x -- use partitioned transition relation (may use less memory)" << endl + << " -z -- use reordering of the BDD variables" << endl + << " -v -- verbose (can be used more than once to increase verbosity)" << endl + << " -p -- show progress (where possible)" << endl << endl << " Benchmarking options:" << endl - << " -m -- measure and display time and memory usage" << endl - << " -B -- display an easy to parse summary (enables -m)" << endl + << " -m -- measure and display time and memory usage" << endl + << " -B -- display an easy to parse summary (enables -m)" << endl << endl; return 100; } if (!(reach_states || reach_states_succ || rstl_model_checking || show_reactions || print_parsed_sys)) { - FERROR("No task specified: -c, -f, -P, -r, or -s needs to be used"); + FERROR("No task specified: -c, -P, -r, or -s needs to be used"); } if (opts->verbose > 0) @@ -163,6 +161,17 @@ int main(int argc, char **argv) { FERROR("Parse error"); } + + // + // Here we retrieve the reaction system from the parser + // + // We decide which RS will be used at the parser level. + // This decision depends on whether we use concentrations, + // context automaton, etc. + // + auto rs = *driver.getReactionSystem(); + + rs.setOptions(opts); // these need to be passed to the driver if (show_reactions) rs.showReactions(); @@ -184,9 +193,14 @@ int main(int argc, char **argv) if (rstl_model_checking) { if (bmc) - mc.checkRSCTL(driver.getFormRSCTL()); - else - mc.checkRSCTLfull(driver.getFormRSCTL()); + { + cout << "Using BDD-based Bounded Model Checking" << endl; + mc.checkRSCTL(driver.getFormRSCTL()); + } + else + { + mc.checkRSCTLfull(driver.getFormRSCTL()); + } } } @@ -197,7 +211,7 @@ int main(int argc, char **argv) << "Verification time: " << opts->ver_time << " sec" << endl << "Encoding memory: " << opts->enc_mem << " MB" << endl << "Memory (total): " << opts->ver_mem << " MB" << endl - << "TOTAL time: " << opts->enc_time+opts->ver_time << " sec" << endl; + << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl; if (benchmarking) { cout << std::setprecision(4) diff --git a/mc.cc b/mc.cc index e3670a3..850e56f 100644 --- a/mc.cc +++ b/mc.cc @@ -151,7 +151,7 @@ bool ModelChecker::checkReach(const RctSys::Entities testState) BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form) { - assert(reach != NULL); + assert(reach != nullptr); Oper oper = form->getOper(); if (oper == RSCTL_PV) { @@ -364,7 +364,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form) if (opts->measure) opts->ver_time = cpuTime(); - assert(form != NULL); + assert(form != nullptr); bool result = false; @@ -378,7 +378,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form) form->encodeActions(srs); VERB("Contexts encoded"); - assert(reach == NULL); + assert(reach == nullptr); reach = new BDD(*initStates); BDD reach_p = cuddMgr->bddZero(); @@ -437,7 +437,7 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form) if (opts->measure) opts->ver_time = cpuTime(); - assert(form != NULL); + assert(form != nullptr); if (!form->isERSCTL()) { @@ -456,7 +456,7 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form) form->encodeActions(srs); VERB("Contexts encoded"); - assert(reach == NULL); + assert(reach == nullptr); reach = new BDD(*initStates); BDD reach_p = cuddMgr->bddZero(); @@ -499,6 +499,6 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form) void ModelChecker::cleanup(void) { delete reach; - reach = NULL; + reach = nullptr; } diff --git a/mc.hh b/mc.hh index 20ff756..35f1e7f 100644 --- a/mc.hh +++ b/mc.hh @@ -59,10 +59,10 @@ public: pv_succ_E = srs->getEncPVsucc_E(); pv_act_E = srs->getEncPVact_E(); trp = srs->getEncPartTrans(); - if (trp == NULL) trp_size = 0; + if (trp == nullptr) trp_size = 0; else trp_size = trp->size(); trm = srs->getEncMonoTrans(); - reach = NULL; + reach = nullptr; } void printReach(void); diff --git a/memtime.hh b/memtime.hh index df3a089..1bcef66 100644 --- a/memtime.hh +++ b/memtime.hh @@ -40,7 +40,7 @@ static inline int memReadStat(void) pid_t pid = getpid(); sprintf(name, "/proc/%d/statm", pid); FILE* in = fopen(name, "rb"); - if (in == NULL) + if (in == nullptr) { return 0; } diff --git a/rs.cc b/rs.cc index d2b327f..d3dde71 100644 --- a/rs.cc +++ b/rs.cc @@ -24,7 +24,7 @@ void RctSys::addEntity(std::string name) VERB_L2("Adding entity: " << name << " index=" << new_entity_id); - entities_ids.push_back(name); + entities_ids.push_back(name); entities_names[name] = new_entity_id; } } @@ -166,7 +166,6 @@ void RctSys::printSystem(void) showInitialStates(); showActionEntities(); showReactions(); - } bool CtxAut::hasState(std::string name) @@ -177,6 +176,15 @@ bool CtxAut::hasState(std::string name) return true; } +CtxAut::State CtxAut::getStateID(std::string name) +{ + if (!hasState(name)) + { + FERROR("No such state: " << name); + } + return states_names[name]; +} + void CtxAut::addState(std::string name) { if (!hasState(name)) @@ -190,12 +198,20 @@ void CtxAut::addState(std::string name) } } -void CtxAut::pushContextEntity(std::string entityName) +void CtxAut::pushContextEntity(RctSys::Entity entity_id) { - + tmpEntities.insert(entity_id); } void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) { - + VERB_L3("Saving transition"); + + Transition new_transition; + + new_transition.src_state = getStateID(srcStateName); + new_transition.ctx = tmpEntities; + tmpEntities.clear(); + new_transition.dst_state = getStateID(dstStateName); } + diff --git a/rs.hh b/rs.hh index d127e1e..97fc22b 100644 --- a/rs.hh +++ b/rs.hh @@ -95,12 +95,6 @@ class RctSys void printSystem(void); }; -class RctSysWithCtxAut : private RctSys -{ - friend class CtxAut; - -}; - // Context Automaton class CtxAut { @@ -113,14 +107,13 @@ class CtxAut RctSys::Entities ctx; State dst_state; }; + bool hasState(std::string name); void addState(std::string stateName); + State getStateID(std::string name); void addTransition(std::string srcStateName, std::string dstStateName); - void pushContextEntity(std::string entityName); - void setOptions(Options *opts) - { - this->opts = opts; - } + void pushContextEntity(RctSys::Entity entity_id); + void setOptions(Options *opts) { this->opts = opts; } private: Options *opts; @@ -129,5 +122,11 @@ class CtxAut RctSys::Entities tmpEntities; }; -#endif +class RctSysWithCtxAut : public RctSys +{ + // friend class CtxAut; + + CtxAut ctx_aut; +}; +#endif diff --git a/rsin_driver.cc b/rsin_driver.cc index 8c8862a..ac76c39 100644 --- a/rsin_driver.cc +++ b/rsin_driver.cc @@ -1,15 +1,31 @@ #include "rsin_driver.hh" #include "rsin_parser.hh" +rsin_driver::rsin_driver(void) +: trace_scanning(false), trace_parsing(false) +{ + initialise(); +} + rsin_driver::rsin_driver(RctSys *rs) : trace_scanning(false), trace_parsing(false) { - this->rsctlform = NULL; - this->rs = rs; + initialise(); + this->rs = rs; +} + +void rsin_driver::initialise(void) +{ + this->rs = nullptr; + this->rsctlform = nullptr; + opts = nullptr; + use_ctx_aut = false; + use_concentrations = false; } rsin_driver::~rsin_driver () { + // placeholder } int rsin_driver::parse(const std::string &f) @@ -33,10 +49,9 @@ void rsin_driver::error(const std::string &m) std::cerr << m << std::endl; } - FormRSCTL *rsin_driver::getFormRSCTL(void) { - if (rsctlform == NULL) + if (rsctlform == nullptr) { FERROR("RSCTL formula was not supplied!"); } @@ -44,3 +59,40 @@ FormRSCTL *rsin_driver::getFormRSCTL(void) return rsctlform; } +// +// Checks if we are not too late to be setting any options +// +void rsin_driver::ensureOptionsAllowed(void) +{ + if (rs != nullptr) + { + FERROR("Options cannot be set/modified after the reaction system is initialised") + } +} + +void rsin_driver::ensureReactionSystemReady(void) +{ + if (rs == nullptr) + setupReactionSystem(); +} + +void rsin_driver::setupReactionSystem(void) +{ + assert(rs == nullptr); + if (use_ctx_aut) + { + rs = new RctSysWithCtxAut; + } + else + { + rs = new RctSys; + } + rs->setOptions(opts); +} + +RctSys *rsin_driver::getReactionSystem(void) +{ + ensureReactionSystemReady(); + assert(rs != nullptr); + return rs; +} diff --git a/rsin_driver.hh b/rsin_driver.hh index f6acabc..7d8eec5 100644 --- a/rsin_driver.hh +++ b/rsin_driver.hh @@ -5,6 +5,7 @@ #include "rsin_parser.hh" #include "rs.hh" #include "formrsctl.hh" +#include "options.hh" // Tell Flex the lexer's prototype ... #define YY_DECL \ @@ -19,12 +20,20 @@ YY_DECL; class rsin_driver { public: + rsin_driver(void); rsin_driver(RctSys *rs); virtual ~rsin_driver(); //std::map variables; RctSys *rs; FormRSCTL *rsctlform; + Options *opts; + + // + // options in configuration file + // + bool use_ctx_aut; + bool use_concentrations; // Handling the scanner void scan_begin(); @@ -35,14 +44,26 @@ public: std::string file; bool trace_parsing; - void addFormRSCTL(FormRSCTL *f) { rsctlform = f; } + void setOptions(Options *opts) { this->opts = opts; }; + void addFormRSCTL(FormRSCTL *f) { rsctlform = f; }; FormRSCTL *getFormRSCTL(void); + void ensureOptionsAllowed(void); + void useContextAutomaton(void) { ensureOptionsAllowed(); use_ctx_aut = true; }; + void useConcentrations(void) { ensureOptionsAllowed(); use_concentrations = true; }; + + void ensureReactionSystemReady(void); + void setupReactionSystem(void); + + RctSys *getReactionSystem(void); + // Error handling. void error(const yy::location &l, const std::string &m); void error(const std::string &m); + +private: + void initialise(void); }; #endif - diff --git a/rsin_parser.ll b/rsin_parser.ll index 5c8249a..8f72e39 100644 --- a/rsin_parser.ll +++ b/rsin_parser.ll @@ -38,6 +38,9 @@ blank [ \t] typedef yy::rsin_parser::token token; %} +"options" return token::OPTIONS; +"use-context-automaton" return token::USE_CTX_AUT; +"use-concentrations" return token::USE_CONCENTRATIONS; "reactions" return token::REACTIONS; "initial-contexts" return token::INITIALCONTEXTS; "context-entities" return token::CONTEXTENTITIES; diff --git a/rsin_parser.yy b/rsin_parser.yy index 08722df..6fa3950 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -44,6 +44,7 @@ class rsin_driver; #include "rsin_driver.hh" } +%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS %token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM %token CONTEXTAUTOMATON STATES TRANSITIONS %token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR @@ -75,6 +76,7 @@ class rsin_driver; %start system; system: + | OPTIONS LCB options RCB system | REACTIONS LCB reactions RCB system | INITIALCONTEXTS LCB initstates RCB system | CONTEXTENTITIES LCB actionentities RCB system @@ -84,6 +86,14 @@ system: } ; +options: + | options option SEMICOL + ; + +option: + | USE_CTX_AUT { } + ; + /* * ------------------------- * REACTIONS @@ -95,7 +105,7 @@ reactions: reaction: | LCB reactionConditions RARR LCB reactionProducts RCB RCB { - driver.rs->commitReaction(); + driver.getReactionSystem()->commitReaction(); } ; @@ -109,7 +119,7 @@ reactants: ; reactant: IDENTIFIER { - driver.rs->pushReactant(*$1); + driver.getReactionSystem()->pushReactant(*$1); free($1); } ; @@ -121,7 +131,7 @@ inhibitors: inhibitor: | IDENTIFIER { - driver.rs->pushInhibitor(*$1); + driver.getReactionSystem()->pushInhibitor(*$1); free($1); } ; @@ -132,7 +142,7 @@ reactionProducts: ; reactionProduct: IDENTIFIER { - driver.rs->pushProduct(*$1); + driver.getReactionSystem()->pushProduct(*$1); free($1); } ; @@ -141,10 +151,10 @@ reactionProduct: IDENTIFIER { initstates: LCB initstate RCB { - driver.rs->commitInitState(); + driver.getReactionSystem()->commitInitState(); } | initstates COMMA LCB initstate RCB { - driver.rs->commitInitState(); + driver.getReactionSystem()->commitInitState(); } ; @@ -154,7 +164,7 @@ initstate: ; entity: IDENTIFIER { - driver.rs->pushStateEntity(*$1); + driver.getReactionSystem()->pushStateEntity(*$1); free($1); } ; @@ -167,7 +177,7 @@ actionentities: ; actentity: IDENTIFIER { - driver.rs->addActionEntity(*$1); + driver.getReactionSystem()->addActionEntity(*$1); free($1); } ; diff --git a/symrs.cc b/symrs.cc index e2eca69..4af9b45 100644 --- a/symrs.cc +++ b/symrs.cc @@ -318,7 +318,7 @@ void SymRS::encodeInitStates(void) #ifndef NDEBUG if (opts->part_tr_rel) - assert(partTrans != NULL); + assert(partTrans != nullptr); #endif initStates = new BDD(BDD_FALSE); diff --git a/symrs.hh b/symrs.hh index 2b2cc66..f20dc76 100644 --- a/symrs.hh +++ b/symrs.hh @@ -122,8 +122,8 @@ public: totalReactions = rs->getReactionsSize(); totalActions = rs->getActionsSize(); - partTrans = NULL; - monoTrans = NULL; + partTrans = nullptr; + monoTrans = nullptr; encode(); }