From 5f1a759c8fa972996653d1eae6769a891f55bf1a Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Wed, 28 Mar 2018 21:00:44 +0100 Subject: [PATCH] Reformatting --- bdd_macro.hh | 8 +- ctx_aut.cc | 117 +++---- ctx_aut.hh | 58 ++-- formrsctl.cc | 519 ++++++++++++++--------------- formrsctl.hh | 417 ++++++++++++----------- macro.hh | 12 +- main.cc | 427 ++++++++++++------------ mc.cc | 873 ++++++++++++++++++++++++------------------------- mc.hh | 24 +- memtime.hh | 43 +-- options.hh | 25 +- rs.cc | 359 ++++++++++---------- rs.hh | 156 +++++---- rsin_driver.cc | 85 +++-- rsin_driver.hh | 48 +-- symrs.cc | 842 +++++++++++++++++++++++------------------------ symrs.hh | 229 ++++++++----- types.hh | 18 +- 18 files changed, 2204 insertions(+), 2056 deletions(-) diff --git a/bdd_macro.hh b/bdd_macro.hh index 43136af..dee04e3 100644 --- a/bdd_macro.hh +++ b/bdd_macro.hh @@ -1,11 +1,11 @@ #ifndef __BDD_MACRO_HH__ #define __BDD_MACRO_HH__ -#define BDD_IFF(p,q) (!(p+q)+(p*q)) -#define BDD_TRUE (cuddMgr->bddOne()) -#define BDD_FALSE (cuddMgr->bddZero()) +#define BDD_IFF(p,q) (!(p+q)+(p*q)) +#define BDD_TRUE (cuddMgr->bddOne()) +#define BDD_FALSE (cuddMgr->bddZero()) -#define BDD_PRINT(t) ((t).PrintMinterm()) +#define BDD_PRINT(t) ((t).PrintMinterm()) #endif diff --git a/ctx_aut.cc b/ctx_aut.cc index a77e21c..1354b53 100644 --- a/ctx_aut.cc +++ b/ctx_aut.cc @@ -1,108 +1,111 @@ #include "ctx_aut.hh" -CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) -{ - setOptions(opts); - this->parent_rctsys = parent_rctsys; +CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) +{ + setOptions(opts); + this->parent_rctsys = parent_rctsys; } bool CtxAut::hasState(std::string name) { - if (states_names.find(name) == states_names.end()) - return false; - else - return true; + if (states_names.find(name) == states_names.end()) { + return false; + } + else { + return true; + } } State CtxAut::getStateID(std::string name) { - if (!hasState(name)) - { - FERROR("No such state: " << name); - } - return states_names[name]; + if (!hasState(name)) { + FERROR("No such state: " << name); + } + + return states_names[name]; } std::string CtxAut::getStateName(State state_id) { - assert(state_id < states_ids.size()); - return states_ids[state_id]; + assert(state_id < states_ids.size()); + return states_ids[state_id]; } void CtxAut::addState(std::string name) { - if (!hasState(name)) - { - State new_state_id = states_ids.size(); + if (!hasState(name)) { + State new_state_id = states_ids.size(); - VERB_L2("Adding state: " << name << " index=" << new_state_id); + VERB_L2("Adding state: " << name << " index=" << new_state_id); - states_ids.push_back(name); - states_names[name] = new_state_id; - - if (!init_state_defined) - { - setInitState(name); - } + states_ids.push_back(name); + states_names[name] = new_state_id; + + if (!init_state_defined) { + setInitState(name); } + } } void CtxAut::setInitState(std::string name) { - VERB_L2("Setting initial CA state: " << name); - State state_id = getStateID(name); - VERB_L2("Got initial CA state ID: index=" << state_id); - init_state_id = state_id; - init_state_defined = true; + VERB_L2("Setting initial CA state: " << name); + State state_id = getStateID(name); + VERB_L2("Got initial CA state ID: index=" << state_id); + init_state_id = state_id; + init_state_defined = true; } State CtxAut::getInitState(void) { - assert(init_state_defined); - return init_state_id; + assert(init_state_defined); + return init_state_id; } void CtxAut::printAutomaton(void) { - showStates(); - showTransitions(); + showStates(); + showTransitions(); } void CtxAut::showStates(void) { - cout << "# Context Automaton States:" << endl; - cout << " = Init state: " << getStateName(init_state_id) << endl; - for (const auto &s : states_ids) - cout << " * " << s << endl; + cout << "# Context Automaton States:" << endl; + cout << " = Init state: " << getStateName(init_state_id) << endl; + + for (const auto &s : states_ids) { + cout << " * " << s << endl; + } } -void CtxAut::pushContextEntity(Entity entity_id) +void CtxAut::pushContextEntity(Entity entity_id) { - tmpEntities.insert(entity_id); + tmpEntities.insert(entity_id); } -void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) +void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) { - VERB_L3("Saving transition"); - - CtxAutTransition new_transition; - - new_transition.src_state = getStateID(srcStateName); - new_transition.ctx = tmpEntities; - tmpEntities.clear(); - new_transition.dst_state = getStateID(dstStateName); - transitions.push_back(new_transition); + VERB_L3("Saving transition"); + + CtxAutTransition new_transition; + + new_transition.src_state = getStateID(srcStateName); + new_transition.ctx = tmpEntities; + tmpEntities.clear(); + new_transition.dst_state = getStateID(dstStateName); + transitions.push_back(new_transition); } void CtxAut::showTransitions(void) { - cout << "# Context Automaton Transitions:" << endl; - for (const auto &t : transitions) - { - cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(t.dst_state) - << "]: {" << parent_rctsys->entitiesToStr(t.ctx) << "}" << endl; - } + cout << "# Context Automaton Transitions:" << endl; + + for (const auto &t : transitions) { + cout << " * [" << getStateName(t.src_state) << " -> " << getStateName( + t.dst_state) + << "]: {" << parent_rctsys->entitiesToStr(t.ctx) << "}" << endl; + } } /** EOF **/ diff --git a/ctx_aut.hh b/ctx_aut.hh index a2e2f6f..d5c143e 100644 --- a/ctx_aut.hh +++ b/ctx_aut.hh @@ -28,32 +28,38 @@ class RctSys; class CtxAut { friend class SymRS; - - public: - CtxAut(Options *opts, RctSys *parent_rctsys); - bool hasState(std::string name); - void addState(std::string stateName); - void setInitState(std::string stateName); - State getInitState(void); - State getStateID(std::string name); - std::string getStateName(State state_id); - void printAutomaton(void); - void showStates(void); - void addTransition(std::string srcStateName, std::string dstStateName); - void showTransitions(void); - void pushContextEntity(Entity entity_id); - void setOptions(Options *opts) { this->opts = opts; } - size_t statesCount(void) { return states_ids.size(); } - - private: - RctSys *parent_rctsys; - Options *opts; - StatesById states_ids; - StatesByName states_names; - State init_state_id; - bool init_state_defined; - Entities tmpEntities; - CtxAutTransitions transitions; + + public: + CtxAut(Options *opts, RctSys *parent_rctsys); + bool hasState(std::string name); + void addState(std::string stateName); + void setInitState(std::string stateName); + State getInitState(void); + State getStateID(std::string name); + std::string getStateName(State state_id); + void printAutomaton(void); + void showStates(void); + void addTransition(std::string srcStateName, std::string dstStateName); + void showTransitions(void); + void pushContextEntity(Entity entity_id); + void setOptions(Options *opts) + { + this->opts = opts; + } + size_t statesCount(void) + { + return states_ids.size(); + } + + private: + RctSys *parent_rctsys; + Options *opts; + StatesById states_ids; + StatesByName states_names; + State init_state_id; + bool init_state_defined; + Entities tmpEntities; + CtxAutTransitions transitions; }; #endif /* RS_CTX_AUT_HH */ diff --git a/formrsctl.cc b/formrsctl.cc index 45a9a5d..8f465e0 100644 --- a/formrsctl.cc +++ b/formrsctl.cc @@ -11,313 +11,300 @@ std::string BoolContexts::toStr(void) const { - if (oper == BCTX_PV) - { - return name; + if (oper == BCTX_PV) { + return name; + } + else if (oper == BCTX_TF) { + if (tf) { + return "true"; } - else if (oper == BCTX_TF) - { - if (tf) return "true"; - else return "false"; - } - else if (oper == BCTX_AND) - { - return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")"; - } - else if (oper == BCTX_OR) - { - return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")"; - } - else if (oper == BCTX_XOR) - { - return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")"; - } - else if (oper == BCTX_NOT) - { - return "~" + arg[0]->toStr(); - } - - else - { - return "??"; - assert(0); + else { + return "false"; } + } + else if (oper == BCTX_AND) { + return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")"; + } + else if (oper == BCTX_OR) { + return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")"; + } + else if (oper == BCTX_XOR) { + return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")"; + } + else if (oper == BCTX_NOT) { + return "~" + arg[0]->toStr(); + } + + else { + return "??"; + assert(0); + } } BDD BoolContexts::getBDD(const SymRS *srs) const { - if (oper == BCTX_PV) - { - return srs->encActStrEntity(name); - } - else if (oper == BCTX_TF) - { - if (tf) return srs->getBDDtrue(); - else return srs->getBDDfalse(); - } - else if (oper == BCTX_AND) - { - return arg[0]->getBDD(srs) * arg[1]->getBDD(srs); - } - else if (oper == BCTX_OR) - { - return arg[0]->getBDD(srs) + arg[1]->getBDD(srs); - } - else if (oper == BCTX_XOR) - { - return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs); - } - else if (oper == BCTX_NOT) - { - return !arg[0]->getBDD(srs); - } - else - { - assert(0); - FERROR("Undefined operator used in Boolean context definition. This should not happen."); - return srs->getBDDfalse(); - } + if (oper == BCTX_PV) { + return srs->encActStrEntity(name); + } + else if (oper == BCTX_TF) { + if (tf) { + return srs->getBDDtrue(); + } + else { + return srs->getBDDfalse(); + } + } + else if (oper == BCTX_AND) { + return arg[0]->getBDD(srs) * arg[1]->getBDD(srs); + } + else if (oper == BCTX_OR) { + return arg[0]->getBDD(srs) + arg[1]->getBDD(srs); + } + else if (oper == BCTX_XOR) { + return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs); + } + else if (oper == BCTX_NOT) { + return !arg[0]->getBDD(srs); + } + else { + assert(0); + FERROR("Undefined operator used in Boolean context definition. This should not happen."); + return srs->getBDDfalse(); + } } std::string FormRSCTL::toStr(void) const { - if (oper == RSCTL_PV) - { - return name; + if (oper == RSCTL_PV) { + return name; + } + else if (oper == RSCTL_TF) { + if (tf) { + return "true"; } - else if (oper == RSCTL_TF) - { - if (tf) return "true"; - else return "false"; - } - else if (oper == RSCTL_AND) - { - return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_OR) - { - return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_XOR) - { - return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_IMPL) - { - return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_NOT) - { - return "~" + arg[0]->toStr(); - } - else if (oper == RSCTL_EX) - { - return "EX(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_EG) - { - return "EG(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_EU) - { - return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_EF) - { - return "EF(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AX) - { - return "AX(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AG) - { - return "AG(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AU) - { - return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_AF) - { - return "AF(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_EX_ACT) - { - return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_EG_ACT) - { - return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_EU_ACT) - { - return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_EF_ACT) - { - return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AX_ACT) - { - return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AG_ACT) - { - return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")"; - } - else if (oper == RSCTL_AU_ACT) - { - return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; - } - else if (oper == RSCTL_AF_ACT) - { - return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")"; + else { + return "false"; } + } + else if (oper == RSCTL_AND) { + return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_OR) { + return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_XOR) { + return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_IMPL) { + return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_NOT) { + return "~" + arg[0]->toStr(); + } + else if (oper == RSCTL_EX) { + return "EX(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_EG) { + return "EG(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_EU) { + return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_EF) { + return "EF(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AX) { + return "AX(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AG) { + return "AG(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AU) { + return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")"; + } + else if (oper == RSCTL_AF) { + return "AF(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_EX_ACT) { + return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_EG_ACT) { + return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_EU_ACT) { + return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + + ")"; + } + else if (oper == RSCTL_EF_ACT) { + return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AX_ACT) { + return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AG_ACT) { + return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")"; + } + else if (oper == RSCTL_AU_ACT) { + return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + + ")"; + } + else if (oper == RSCTL_AF_ACT) { + return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")"; + } - else - { - return "??"; - assert(0); - } + else { + return "??"; + assert(0); + } } bool FormRSCTL::hasOper(Oper op) const { - if (oper == op) - return true; - else - { - bool result = false; - if (arg[0] != nullptr) result = arg[0]->hasOper(op); - if (!result && arg[1] != nullptr) result = arg[1]->hasOper(op); - return result; + if (oper == op) { + return true; + } + else { + bool result = false; + + if (arg[0] != nullptr) { + result = arg[0]->hasOper(op); } + + if (!result && arg[1] != nullptr) { + result = arg[1]->hasOper(op); + } + + return result; + } } void FormRSCTL::encodeEntities(const SymRS *srs) { - if (RSCTL_COND_1ARG(oper)) - { - arg[0]->encodeEntities(srs); - } - else if (RSCTL_COND_2ARG(oper)) - { - arg[0]->encodeEntities(srs); - arg[1]->encodeEntities(srs); - } - else if (oper == RSCTL_PV) - { - bdd = new BDD(srs->encEntity(name)); - } + if (RSCTL_COND_1ARG(oper)) { + arg[0]->encodeEntities(srs); + } + else if (RSCTL_COND_2ARG(oper)) { + arg[0]->encodeEntities(srs); + arg[1]->encodeEntities(srs); + } + else if (oper == RSCTL_PV) { + bdd = new BDD(srs->encEntity(name)); + } } bool FormRSCTL::isERSCTL(void) const { - if (oper == RSCTL_PV) - { - return true; + if (oper == RSCTL_PV) { + return true; + } + + if (oper == RSCTL_NOT) { + if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF) { + return true; } - - if (oper == RSCTL_NOT) - { - if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF) - return true; - else - return false; + else { + return false; } + } - if (RSCTL_COND_IS_UNIVERSAL(oper)) - { - return false; - } - - if (RSCTL_COND_1ARG(oper)) - { - return arg[0]->isERSCTL(); - } - - if (RSCTL_COND_2ARG(oper)) - { - return arg[0]->isERSCTL() && arg[1]->isERSCTL(); - } - - assert(0); - + if (RSCTL_COND_IS_UNIVERSAL(oper)) { return false; + } + + if (RSCTL_COND_1ARG(oper)) { + return arg[0]->isERSCTL(); + } + + if (RSCTL_COND_2ARG(oper)) { + return arg[0]->isERSCTL() && arg[1]->isERSCTL(); + } + + assert(0); + + return false; } std::string FormRSCTL::getActionsStr(void) const { - if (actions != nullptr) - { - std::string r = "[ "; - bool firstact = true; + 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; - } - else if (boolCtx != nullptr) - { - return "< " + boolCtx->toStr() + " >"; - } - else - { - FERROR("Context not specified. This should not happen."); - } + 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; + } + else if (boolCtx != nullptr) { + return "< " + boolCtx->toStr() + " >"; + } + else { + FERROR("Context not specified. This should not happen."); + } } void FormRSCTL::encodeActions(const SymRS *srs) { - if (RSCTL_COND_ACT(oper)) - { - if (actions_bdd != nullptr) forgetActionsBDD(); - actions_bdd = new BDD(srs->getBDDfalse()); - 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; - } - } - else if (boolCtx != nullptr) - { - *actions_bdd = boolCtx->getBDD(srs); - } - else - assert(0); + if (RSCTL_COND_ACT(oper)) { + if (actions_bdd != nullptr) { + forgetActionsBDD(); } - if (RSCTL_COND_1ARG(oper)) - { - arg[0]->encodeActions(srs); - } + actions_bdd = new BDD(srs->getBDDfalse()); + assert(actions != nullptr || boolCtx != nullptr); + assert(!(actions != nullptr && boolCtx != nullptr)); - if (RSCTL_COND_2ARG(oper)) - { - arg[0]->encodeActions(srs); - arg[1]->encodeActions(srs); + 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; + } } + else if (boolCtx != nullptr) { + *actions_bdd = boolCtx->getBDD(srs); + } + else { + assert(0); + } + } + + if (RSCTL_COND_1ARG(oper)) { + arg[0]->encodeActions(srs); + } + + if (RSCTL_COND_2ARG(oper)) { + arg[0]->encodeActions(srs); + arg[1]->encodeActions(srs); + } } diff --git a/formrsctl.hh b/formrsctl.hh index eac1723..14990e7 100644 --- a/formrsctl.hh +++ b/formrsctl.hh @@ -19,7 +19,7 @@ #define RSCTL_PV 0 // propositional variable #define RSCTL_AND 1 #define RSCTL_OR 2 -#define RSCTL_XOR 3 +#define RSCTL_XOR 3 #define RSCTL_NOT 4 #define RSCTL_IMPL 5 #define RSCTL_EG 11 // Existential... @@ -41,12 +41,12 @@ #define RSCTL_TF 50 // true/false /* For Boolean contexts: */ -#define BCTX_PV 60 -#define BCTX_AND 61 -#define BCTX_OR 62 -#define BCTX_XOR 63 -#define BCTX_NOT 64 -#define BCTX_TF 70 +#define BCTX_PV 60 +#define BCTX_AND 61 +#define BCTX_OR 62 +#define BCTX_XOR 63 +#define BCTX_NOT 64 +#define BCTX_TF 70 #define RSCTL_COND_1ARG(a) ((a) == RSCTL_NOT || (a) == RSCTL_EG || (a) == RSCTL_EF || (a) == RSCTL_EX || (a) == RSCTL_AG || (a) == RSCTL_AF || (a) == RSCTL_AX || (a) == RSCTL_EG_ACT || (a) == RSCTL_EF_ACT || (a) == RSCTL_EX_ACT || (a) == RSCTL_AG_ACT || (a) == RSCTL_AF_ACT || (a) == RSCTL_AX_ACT) @@ -71,75 +71,82 @@ typedef vector ActionsVec_f; class BoolContexts { - Oper oper; - BoolContexts *arg[2]; - std::string name; - bool tf; - -public: - - BoolContexts(std::string varName) - { - oper = BCTX_PV; - name = varName; - arg[0] = nullptr; - arg[1] = nullptr; - } - - /** - * @brief Constructor for true/false. - * - * @param val value of the logical constant - */ - BoolContexts(bool val) { - oper = BCTX_TF; - tf = val; - arg[0] = nullptr; - arg[1] = nullptr; - } + Oper oper; + BoolContexts *arg[2]; + std::string name; + bool tf; - /** - * @brief Constructor for one-argument formula. - */ - BoolContexts(Oper op, BoolContexts *form1) { - assert(op == BCTX_NOT); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - } + public: - /** - * @brief Constructor for two-argument formula. - */ - BoolContexts(Oper op, BoolContexts *form1, BoolContexts *form2) { - assert(BCTX_COND_2ARG(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - } - - ~BoolContexts() { - delete arg[0]; - delete arg[1]; - } - - std::string toStr(void) const; - - BDD getBDD(const SymRS *srs) const; - - Oper getOper(void) const { - assert(BCTX_IS_VALID(oper)); - return oper; - } - BoolContexts *getLeftSF(void) const { - assert(arg[0] != nullptr); - return arg[0]; - } - BoolContexts *getRightSF(void) const { - assert(BCTX_COND_2ARG(oper)); - assert(arg[1] != nullptr); - return arg[1]; - } + BoolContexts(std::string varName) + { + oper = BCTX_PV; + name = varName; + arg[0] = nullptr; + arg[1] = nullptr; + } + + /** + * @brief Constructor for true/false. + * + * @param val value of the logical constant + */ + BoolContexts(bool val) + { + oper = BCTX_TF; + tf = val; + arg[0] = nullptr; + arg[1] = nullptr; + } + + /** + * @brief Constructor for one-argument formula. + */ + BoolContexts(Oper op, BoolContexts *form1) + { + assert(op == BCTX_NOT); + oper = op; + arg[0] = form1; + arg[1] = nullptr; + } + + /** + * @brief Constructor for two-argument formula. + */ + BoolContexts(Oper op, BoolContexts *form1, BoolContexts *form2) + { + assert(BCTX_COND_2ARG(op)); + oper = op; + arg[0] = form1; + arg[1] = form2; + } + + ~BoolContexts() + { + delete arg[0]; + delete arg[1]; + } + + std::string toStr(void) const; + + BDD getBDD(const SymRS *srs) const; + + Oper getOper(void) const + { + assert(BCTX_IS_VALID(oper)); + return oper; + } + BoolContexts *getLeftSF(void) const + { + assert(arg[0] != nullptr); + return arg[0]; + } + BoolContexts *getRightSF(void) const + { + assert(BCTX_COND_2ARG(oper)); + assert(arg[1] != nullptr); + return arg[1]; + } }; class FormRSCTL @@ -151,23 +158,24 @@ class FormRSCTL BDD *bdd; ActionsVec_f *actions; BDD *actions_bdd; - BoolContexts *boolCtx; -public: + BoolContexts *boolCtx; + public: /** * @brief Constructor for propositional variable. * * @param varName variable name used mostly for printing the variable. * @param varBDD the BDD describing the set where the variable holds. */ - FormRSCTL(std::string varName) { - oper = RSCTL_PV; - name = varName; - arg[0] = nullptr; - arg[1] = nullptr; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(std::string varName) + { + oper = RSCTL_PV; + name = varName; + arg[0] = nullptr; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** @@ -175,156 +183,173 @@ public: * * @param val value of the logical constant */ - FormRSCTL(bool val) { - oper = RSCTL_TF; - tf = val; - arg[0] = nullptr; - arg[1] = nullptr; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(bool val) + { + oper = RSCTL_TF; + tf = val; + arg[0] = nullptr; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = nullptr; } /** * @brief Constructor for two-argument formula. */ - FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2) { - assert(RSCTL_COND_2ARG(op)); - assert(!RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2) + { + assert(RSCTL_COND_2ARG(op)); + assert(!RSCTL_COND_ACT(op)); + oper = op; + arg[0] = form1; + arg[1] = form2; + 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 != nullptr); - assert(RSCTL_COND_2ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - bdd = nullptr; - actions = acts; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) + { + assert(acts != nullptr); + assert(RSCTL_COND_2ARG(op)); + assert(RSCTL_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. - */ - FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) { - assert(bctx != nullptr); - assert(RSCTL_COND_2ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = bctx; - } + /** + * @brief Constructor for two-argument formula with Boolean context restrictions. + */ + FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) + { + assert(bctx != nullptr); + assert(RSCTL_COND_2ARG(op)); + assert(RSCTL_COND_ACT(op)); + oper = op; + arg[0] = form1; + arg[1] = form2; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = bctx; + } /** * @brief Constructor for one-argument formula. */ - FormRSCTL(Oper op, FormRSCTL *form1) { - assert(RSCTL_COND_1ARG(op)); - assert(!RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(Oper op, FormRSCTL *form1) + { + assert(RSCTL_COND_1ARG(op)); + assert(!RSCTL_COND_ACT(op)); + oper = op; + arg[0] = form1; + 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 != nullptr); - assert(RSCTL_COND_1ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - bdd = nullptr; - actions = acts; - actions_bdd = nullptr; - boolCtx = nullptr; + FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) + { + assert(acts != nullptr); + assert(RSCTL_COND_1ARG(op)); + assert(RSCTL_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. - */ - FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) { - assert(bctx != nullptr); - assert(RSCTL_COND_1ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - bdd = nullptr; - actions = nullptr; - actions_bdd = nullptr; - boolCtx = bctx; - } + /** + * @brief Constructor for one-argument formula with Boolean context restrictions. + */ + FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) + { + assert(bctx != nullptr); + assert(RSCTL_COND_1ARG(op)); + assert(RSCTL_COND_ACT(op)); + oper = op; + arg[0] = form1; + arg[1] = nullptr; + bdd = nullptr; + actions = nullptr; + actions_bdd = nullptr; + boolCtx = bctx; + } /** * @brief Destructor. */ - ~FormRSCTL() { - delete arg[0]; - delete arg[1]; - delete bdd; - delete actions; - delete actions_bdd; - delete boolCtx; + ~FormRSCTL() + { + delete arg[0]; + delete arg[1]; + delete bdd; + delete actions; + delete actions_bdd; + delete boolCtx; } std::string toStr(void) const; bool hasOper(Oper op) const; - const BDD *getBDD(void) const { - assert(oper == RSCTL_PV); - assert(bdd != nullptr); - return bdd; + const BDD *getBDD(void) const + { + assert(oper == RSCTL_PV); + assert(bdd != nullptr); + return bdd; } - const BDD *getActionsBDD(void) const { - assert(RSCTL_COND_ACT(oper)); - assert(actions_bdd != nullptr); - return actions_bdd; + const BDD *getActionsBDD(void) const + { + assert(RSCTL_COND_ACT(oper)); + assert(actions_bdd != nullptr); + return actions_bdd; } - Oper getOper(void) const { - assert(RSCTL_IS_VALID(oper)); - return oper; + Oper getOper(void) const + { + assert(RSCTL_IS_VALID(oper)); + return oper; } - FormRSCTL *getLeftSF(void) const { - assert(arg[0] != nullptr); - return arg[0]; + FormRSCTL *getLeftSF(void) const + { + assert(arg[0] != nullptr); + return arg[0]; } - FormRSCTL *getRightSF(void) const { - assert(RSCTL_COND_2ARG(oper)); - assert(arg[1] != nullptr); - return arg[1]; + FormRSCTL *getRightSF(void) const + { + assert(RSCTL_COND_2ARG(oper)); + assert(arg[1] != nullptr); + return arg[1]; } std::string getActionsStr(void) const; - bool getTF(void) const { - assert(oper == RSCTL_TF); - return tf; + bool getTF(void) const + { + assert(oper == RSCTL_TF); + return tf; } void encodeEntities(const SymRS *srs); void encodeActions(const SymRS *srs); - void forgetActionsBDD(void) { - if (actions_bdd != nullptr) delete actions_bdd; + void forgetActionsBDD(void) + { + if (actions_bdd != nullptr) { + delete actions_bdd; + } } bool isERSCTL(void) const; }; diff --git a/macro.hh b/macro.hh index dc44207..27934c8 100644 --- a/macro.hh +++ b/macro.hh @@ -7,8 +7,8 @@ /* Fatal error */ #define FERROR(s) \ { \ - std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \ - exit(1); \ + std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \ + exit(1); \ } #define WARNING(s) \ { \ @@ -18,25 +18,25 @@ #define VERB(s) \ assert(opts != nullptr); \ if (opts->verbose > 0) { \ - std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ + 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; \ + 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; \ + std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } #define VERB_LN(n,s) \ assert(opts != nullptr); \ if (opts->verbose >= (n)) { \ - std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ + std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \ } #endif diff --git a/main.cc b/main.cc index 25b3aa8..bba2658 100644 --- a/main.cc +++ b/main.cc @@ -10,236 +10,249 @@ int main(int argc, char **argv) { - rsin_driver driver; + rsin_driver driver; - Options *opts = new Options; - driver.setOptions(opts); + Options *opts = new Options; + driver.setOptions(opts); - bool show_reactions = false; - bool rstl_model_checking = false; - bool reach_states = false; - bool reach_states_succ = false; - bool bmc = true; - bool benchmarking = false; - bool usage_error = false; - bool print_parsed_sys = false; + bool show_reactions = false; + bool rstl_model_checking = false; + bool reach_states = false; + bool reach_states_succ = false; + bool bmc = true; + bool benchmarking = false; + bool usage_error = false; + bool print_parsed_sys = false; - static struct option long_options[] = - { - {"trace-parsing", no_argument, 0, 0 }, - {"trace-scanning", no_argument, 0, 0 }, - {0, 0, 0, 0 } - }; + static struct option long_options[] = { + {"trace-parsing", no_argument, 0, 0 }, + {"trace-scanning", no_argument, 0, 0 }, + {0, 0, 0, 0 } + }; - int c; - int option_index = 0; + int c; + int option_index = 0; - while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxzh", long_options, &option_index)) != -1) - { - switch (c) { - case 0: - printf("option %s", long_options[option_index].name); - if (optarg) - printf(" with arg %s", optarg); - printf("\n"); + while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxzh", long_options, + &option_index)) != -1) { + switch (c) { + case 0: + printf("option %s", long_options[option_index].name); - if (strcmp(long_options[option_index].name, "trace-parsing")) - driver.trace_parsing = true; - else if (strcmp(long_options[option_index].name, "trace-scanning")) - driver.trace_scanning = true; - - break; - //case 'b': - // printf("-b with %s\n", optarg); - // break; - case 'b': - bmc = false; - break; - case 'p': - opts->show_progress = true; - break; - case 'P': - print_parsed_sys = true; - break; - case 'r': - show_reactions = true; - break; - case 'c': - rstl_model_checking = true; - break; - case 'm': - opts->measure = true; - break; - case 'B': - benchmarking = true; - opts->measure = true; - break; - case 's': - reach_states = true; - break; - case 't': - reach_states_succ = true; - break; - case 'v': - opts->verbose++; - break; - case 'x': - opts->part_tr_rel = true; - break; - case 'z': - opts->reorder_reach = true; - opts->reorder_trans = true; - break; - case 'h': - usage_error = true; - break; - default: - usage_error = true; - break; + if (optarg) { + printf(" with arg %s", optarg); } - } - - std::string inputfile; - if (optind < argc) - { - inputfile = argv[optind]; - } - else - { - cout << "Missing input file" << endl; + + printf("\n"); + + if (strcmp(long_options[option_index].name, "trace-parsing")) { + driver.trace_parsing = true; + } + else if (strcmp(long_options[option_index].name, "trace-scanning")) { + driver.trace_scanning = true; + } + + break; + + //case 'b': + // printf("-b with %s\n", optarg); + // break; + case 'b': + bmc = false; + break; + + case 'p': + opts->show_progress = true; + break; + + case 'P': + print_parsed_sys = true; + break; + + case 'r': + show_reactions = true; + break; + + case 'c': + rstl_model_checking = true; + break; + + case 'm': + opts->measure = true; + break; + + case 'B': + benchmarking = true; + opts->measure = true; + break; + + case 's': + reach_states = true; + break; + + case 't': + reach_states_succ = true; + break; + + case 'v': + opts->verbose++; + break; + + case 'x': + opts->part_tr_rel = true; + break; + + case 'z': + opts->reorder_reach = true; + opts->reorder_trans = true; + break; + + case 'h': usage_error = true; + break; + + default: + usage_error = true; + break; + } + } + + std::string inputfile; + + if (optind < argc) { + inputfile = argv[optind]; + } + else { + cout << "Missing input file" << endl; + usage_error = true; + } + + if (usage_error) { + print_help(std::string(argv[0])); + return 100; + } + + if (!(reach_states || reach_states_succ || rstl_model_checking + || show_reactions || print_parsed_sys)) { + FERROR("No task specified: -c, -P, -r, or -s needs to be used"); + } + + if (opts->verbose > 0) { + cout << "Verbose level: " << opts->verbose << endl; + } + + VERB("Parsing " << inputfile); + + if (driver.parse(inputfile)) { + 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(); + } + + if (print_parsed_sys) { + rs.printSystem(); + } + + if (reach_states || reach_states_succ || rstl_model_checking) { + SymRS srs(&rs, opts); + + ModelChecker mc(&srs, opts); + + if (reach_states) { + mc.printReach(); } - if (usage_error) - { - print_help(std::string(argv[0])); - return 100; + if (reach_states_succ) { + mc.printReachWithSucc(); } - if (!(reach_states || reach_states_succ || rstl_model_checking || show_reactions || print_parsed_sys)) - { - FERROR("No task specified: -c, -P, -r, or -s needs to be used"); + if (rstl_model_checking) { + if (bmc) { + cout << "Using BDD-based Bounded Model Checking" << endl; + mc.checkRSCTL(driver.getFormRSCTL()); + } + else { + mc.checkRSCTLfull(driver.getFormRSCTL()); + } } + } + + if (opts->measure) { + cout << endl << std::setprecision(4) + << "Encoding time: " << opts->enc_time << " sec" << endl + << "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; + + if (benchmarking) { + cout << std::setprecision(4) + << "STAT; " << opts->enc_time + << " ; " << opts->ver_time + << " ; " << opts->enc_mem + << " ; " << opts->ver_mem + << " ; " << opts->enc_time + opts->ver_time << endl; - if (opts->verbose > 0) - { - cout << "Verbose level: " << opts->verbose << endl; } + } - VERB("Parsing " << inputfile); + delete opts; - if (driver.parse(inputfile)) - { - 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(); - - if (print_parsed_sys) - rs.printSystem(); - - if (reach_states || reach_states_succ || rstl_model_checking) - { - SymRS srs(&rs, opts); - - ModelChecker mc(&srs, opts); - - if (reach_states) - { - mc.printReach(); - } - if (reach_states_succ) - { - mc.printReachWithSucc(); - } - - if (rstl_model_checking) - { - if (bmc) - { - cout << "Using BDD-based Bounded Model Checking" << endl; - mc.checkRSCTL(driver.getFormRSCTL()); - } - else - { - mc.checkRSCTLfull(driver.getFormRSCTL()); - } - } - } - - if (opts->measure) - { - cout << endl << std::setprecision(4) - << "Encoding time: " << opts->enc_time << " sec" << endl - << "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; - if (benchmarking) - { - cout << std::setprecision(4) - << "STAT; " << opts->enc_time - << " ; " << opts->ver_time - << " ; " << opts->enc_mem - << " ; " << opts->ver_mem - << " ; " << opts->enc_time+opts->ver_time << endl; - - } - } - - delete opts; - - return 0; + return 0; } void print_help(std::string path_str) { - cout << endl - << " ------------------------------------" << endl - << " -- Reaction Systems Model Checker --" << endl - << " ------------------------------------" << endl - << endl - << " Version: " << VERSION << endl - << " Contact: " << AUTHOR << endl - << endl + cout << endl + << " ------------------------------------" << endl + << " -- Reaction Systems Model Checker --" << endl + << " ------------------------------------" << endl + << endl + << " Version: " << VERSION << endl + << " Contact: " << AUTHOR << endl + << endl #ifndef PUBLIC_RELEASE - << " ###################################" << endl - << " THIS IS A PRIVATE VERSION OF RSMC " << endl - << " PLEASE, DO NOT DISTRIBUTE " << endl - << " ###################################" << endl - << endl + << " ###################################" << endl + << " THIS IS A PRIVATE VERSION OF RSMC " << endl + << " PLEASE, DO NOT DISTRIBUTE " << endl + << " ###################################" << endl + << endl #endif - << " Usage: " << path_str << " [options] " << endl << endl - << " TASKS:" << endl - << " -c -- perform RSCTL model checking" << endl - //<< " -f K -- generate SMT input for the depth K" << 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 - << endl; + << " Usage: " << path_str << " [options] " << endl << endl + << " TASKS:" << endl + << " -c -- perform RSCTL model checking" << endl + //<< " -f K -- generate SMT input for the depth K" << 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 + << endl; } /** EOF **/ diff --git a/mc.cc b/mc.cc index 2ec8873..80b5f2c 100644 --- a/mc.cc +++ b/mc.cc @@ -1,572 +1,567 @@ #include "mc.hh" ModelChecker::ModelChecker(SymRS *srs, Options *opts) - : using_ctx_aut(false) + : using_ctx_aut(false) { - this->srs = srs; - this->opts = opts; - - cuddMgr = srs->getCuddMgr(); - - initStates = srs->getEncInitStates(); - - totalStateVars = srs->getTotalStateVars(); - - pv = srs->getEncPV(); - pv_succ = srs->getEncPVsucc(); - pv_E = srs->getEncPV_E(); - pv_succ_E = srs->getEncPVsucc_E(); - pv_act_E = srs->getEncPVact_E(); + this->srs = srs; + this->opts = opts; - // - // Transition relations - // - // trp -- partitioned TR - // trm -- monolithic TR - // - // If we use trp, then trm is nullptr (same for trm) - // - trp = srs->getEncPartTrans(); - if (trp == nullptr) - trp_size = 0; - else - trp_size = trp->size(); - trm = srs->getEncMonoTrans(); - - if (srs->usingContextAutomaton()) - { - using_ctx_aut = true; - pv_ca = srs->getEncCtxAutPV(); - pv_ca_succ = srs->getEncCtxAutPVsucc(); - pv_ca_E = srs->getEncCtxAutPV_E(); - pv_ca_succ_E = srs->getEncCtxAutPVsucc_E(); - } - else - { - using_ctx_aut = false; - pv_ca = nullptr; - pv_ca_succ = nullptr; - pv_ca_E = nullptr; - pv_ca_succ_E = nullptr; - } - - // Initialise the set of reachable states - reach = nullptr; + cuddMgr = srs->getCuddMgr(); + + initStates = srs->getEncInitStates(); + + totalStateVars = srs->getTotalStateVars(); + + pv = srs->getEncPV(); + pv_succ = srs->getEncPVsucc(); + pv_E = srs->getEncPV_E(); + pv_succ_E = srs->getEncPVsucc_E(); + pv_act_E = srs->getEncPVact_E(); + + // + // Transition relations + // + // trp -- partitioned TR + // trm -- monolithic TR + // + // If we use trp, then trm is nullptr (same for trm) + // + trp = srs->getEncPartTrans(); + + if (trp == nullptr) { + trp_size = 0; + } + else { + trp_size = trp->size(); + } + + trm = srs->getEncMonoTrans(); + + if (srs->usingContextAutomaton()) { + using_ctx_aut = true; + pv_ca = srs->getEncCtxAutPV(); + pv_ca_succ = srs->getEncCtxAutPVsucc(); + pv_ca_E = srs->getEncCtxAutPV_E(); + pv_ca_succ_E = srs->getEncCtxAutPVsucc_E(); + } + else { + using_ctx_aut = false; + pv_ca = nullptr; + pv_ca_succ = nullptr; + pv_ca_E = nullptr; + pv_ca_succ_E = nullptr; + } + + // Initialise the set of reachable states + reach = nullptr; } inline BDD ModelChecker::getSucc(const BDD &states) { - BDD q = BDD_TRUE; + BDD q = BDD_TRUE; - VERB_L2("Computing successors"); - if (opts->part_tr_rel) - { - for (unsigned int i = 0; i < trp_size; ++i) - { - q *= states * (*trp)[i]; - } + VERB_L2("Computing successors"); + + if (opts->part_tr_rel) { + for (unsigned int i = 0; i < trp_size; ++i) { + q *= states * (*trp)[i]; } - else - { - q *= states * *trm; - } - q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); - q = q.ExistAbstract(*pv_act_E); - - return q; + } + else { + q *= states * *trm; + } + + q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); + q = q.ExistAbstract(*pv_act_E); + + return q; } inline BDD ModelChecker::getPreE(const BDD &states) { - BDD q = BDD_TRUE; - VERB_L2("Computing preE"); - BDD x = states.SwapVariables(*pv, *pv_succ); - if (opts->part_tr_rel) - { - for (unsigned int i = 0; i < trp_size; ++i) - q *= x * (*trp)[i]; + BDD q = BDD_TRUE; + VERB_L2("Computing preE"); + BDD x = states.SwapVariables(*pv, *pv_succ); + + if (opts->part_tr_rel) { + for (unsigned int i = 0; i < trp_size; ++i) { + q *= x * (*trp)[i]; } - else - { - q *= x * *trm; - } - q = q.ExistAbstract(*pv_succ_E); - q = q.ExistAbstract(*pv_act_E); - return q; + } + else { + q *= x * *trm; + } + + q = q.ExistAbstract(*pv_succ_E); + q = q.ExistAbstract(*pv_act_E); + return q; } inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts) { - BDD q = BDD_TRUE; - VERB_L2("Computing (context-restricted) preE"); - BDD x = states.SwapVariables(*pv, *pv_succ); - if (opts->part_tr_rel) - { - for (unsigned int i = 0; i < trp_size; ++i) - q *= x * (*trp)[i] * *contexts; + BDD q = BDD_TRUE; + VERB_L2("Computing (context-restricted) preE"); + BDD x = states.SwapVariables(*pv, *pv_succ); + + if (opts->part_tr_rel) { + for (unsigned int i = 0; i < trp_size; ++i) { + q *= x * (*trp)[i] * *contexts; } - else - { - q *= x * *trm * *contexts; - } - q = q.ExistAbstract(*pv_succ_E); - q = q.ExistAbstract(*pv_act_E); - return q; + } + else { + q *= x * *trm * *contexts; + } + + q = q.ExistAbstract(*pv_succ_E); + q = q.ExistAbstract(*pv_act_E); + return q; } void ModelChecker::dropCtxAutStatePart(BDD &states) { - states = states.ExistAbstract(*pv_ca_E); + states = states.ExistAbstract(*pv_ca_E); } void ModelChecker::printReach(void) { - VERB_LN(2, "Printing/generating reachable states"); - - if (opts->measure) - opts->ver_time = cpuTime(); + VERB_LN(2, "Printing/generating reachable states"); - assert(initStates != nullptr); - - BDD *reach = new BDD(*initStates); - BDD reach_p = BDD_FALSE; + if (opts->measure) { + opts->ver_time = cpuTime(); + } - unsigned int k = 0; + assert(initStates != nullptr); - while (*reach != reach_p) - { - if (opts->show_progress) - { - cout << "\rIteration " << ++k << flush; - } - reach_p = *reach; - *reach += getSucc(*reach); + BDD *reach = new BDD(*initStates); + BDD reach_p = BDD_FALSE; + + unsigned int k = 0; + + while (*reach != reach_p) { + if (opts->show_progress) { + cout << "\rIteration " << ++k << flush; } - - dropCtxAutStatePart(*reach); - srs->printDecodedRctSysStates(*reach); + reach_p = *reach; + *reach += getSucc(*reach); + } - cleanup(); + dropCtxAutStatePart(*reach); - if (opts->measure) - { - opts->ver_time = cpuTime() - opts->ver_time; - opts->ver_mem = memUsed(); - } + srs->printDecodedRctSysStates(*reach); + + cleanup(); + + if (opts->measure) { + opts->ver_time = cpuTime() - opts->ver_time; + opts->ver_mem = memUsed(); + } } void ModelChecker::printReachWithSucc(void) { - VERB_LN(2, "Printing/generating reachable states (with successors)"); - - BDD *reach = new BDD(*initStates); - BDD reach_p = cuddMgr->bddZero(); + VERB_LN(2, "Printing/generating reachable states (with successors)"); - while (*reach != reach_p) - { - reach_p = *reach; - BDD newStates = getSucc(*reach) - *reach; - *reach += newStates; + BDD *reach = new BDD(*initStates); + BDD reach_p = cuddMgr->bddZero(); - } + while (*reach != reach_p) { + reach_p = *reach; + BDD newStates = getSucc(*reach) - *reach; + *reach += newStates; - BDD unproc = *reach; - while (!unproc.IsZero()) - { - BDD t; - t = unproc.PickOneMinterm(*pv); - cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl; - srs->printDecodedRctSysStates(getSucc(t)); - unproc -= t; - } - - cleanup(); + } + + BDD unproc = *reach; + + while (!unproc.IsZero()) { + BDD t; + t = unproc.PickOneMinterm(*pv); + cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl; + srs->printDecodedRctSysStates(getSucc(t)); + unproc -= t; + } + + cleanup(); } bool ModelChecker::checkReach(const Entities testState) { - if (opts->measure) - opts->ver_time = cpuTime(); + if (opts->measure) { + opts->ver_time = cpuTime(); + } - BDD st = srs->getEncState(testState); + BDD st = srs->getEncState(testState); - BDD reach = *initStates; - BDD reach_p = cuddMgr->bddZero(); + BDD reach = *initStates; + BDD reach_p = cuddMgr->bddZero(); - while (reach != reach_p) - { - if (reach * st != cuddMgr->bddZero()) - { - cleanup(); - return true; - } - reach_p = reach; - reach += getSucc(reach); + while (reach != reach_p) { + if (reach * st != cuddMgr->bddZero()) { + cleanup(); + return true; } - cleanup(); + reach_p = reach; + reach += getSucc(reach); + } - if (opts->measure) - { - opts->ver_time = cpuTime() - opts->ver_time; - opts->ver_mem = memUsed(); - } + cleanup(); - return false; + if (opts->measure) { + opts->ver_time = cpuTime() - opts->ver_time; + opts->ver_mem = memUsed(); + } + + return false; } BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form) { - assert(reach != nullptr); - Oper oper = form->getOper(); - if (oper == RSCTL_PV) - { - return *form->getBDD() * *reach; - } - else if (oper == RSCTL_TF) - { - if (form->getTF() == true) - return *reach; - else - return cuddMgr->bddZero(); - } - else if (oper == RSCTL_AND) - { - return getStatesRSCTL(form->getLeftSF()) * getStatesRSCTL(form->getRightSF()); - } - else if (oper == RSCTL_OR) - { - return getStatesRSCTL(form->getLeftSF()) + getStatesRSCTL(form->getRightSF()); - } - else if (oper == RSCTL_XOR) - { - return getStatesRSCTL(form->getLeftSF()) ^ getStatesRSCTL(form->getRightSF()); - } - else if (oper == RSCTL_IMPL) - { - return (!getStatesRSCTL(form->getLeftSF()) * *reach) + getStatesRSCTL(form->getRightSF()); - } - else if (oper == RSCTL_NOT) - { - return !getStatesRSCTL(form->getLeftSF()) * *reach; - } - else if (oper == RSCTL_EX) - { - return getPreE(getStatesRSCTL(form->getLeftSF())) * *reach; - } - else if (oper == RSCTL_EG) - { - return statesEG(getStatesRSCTL(form->getLeftSF())); - } - else if (oper == RSCTL_EU) - { - return statesEU( - getStatesRSCTL(form->getLeftSF()), - getStatesRSCTL(form->getRightSF()) - ); - } - else if (oper == RSCTL_EF) - { - return statesEF(getStatesRSCTL(form->getLeftSF())); - } - else if (oper == RSCTL_AX) - { - return !getPreE(!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; - } - else if (oper == RSCTL_AG) - { - return !statesEF( - !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; - } - else if (oper == RSCTL_AU) - { - BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach; - BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach; + assert(reach != nullptr); + Oper oper = form->getOper(); - BDD x = !statesEU(ng, ng * nf) * *reach; - if (!x.IsZero()) - x = x * !statesEG(ng) * *reach; + if (oper == RSCTL_PV) { + return *form->getBDD() * *reach; + } + else if (oper == RSCTL_TF) { + if (form->getTF() == true) { + return *reach; + } + else { + return cuddMgr->bddZero(); + } + } + else if (oper == RSCTL_AND) { + return getStatesRSCTL(form->getLeftSF()) * getStatesRSCTL(form->getRightSF()); + } + else if (oper == RSCTL_OR) { + return getStatesRSCTL(form->getLeftSF()) + getStatesRSCTL(form->getRightSF()); + } + else if (oper == RSCTL_XOR) { + return getStatesRSCTL(form->getLeftSF()) ^ getStatesRSCTL(form->getRightSF()); + } + else if (oper == RSCTL_IMPL) { + return (!getStatesRSCTL(form->getLeftSF()) * *reach) + getStatesRSCTL( + form->getRightSF()); + } + else if (oper == RSCTL_NOT) { + return !getStatesRSCTL(form->getLeftSF()) * *reach; + } + else if (oper == RSCTL_EX) { + return getPreE(getStatesRSCTL(form->getLeftSF())) * *reach; + } + else if (oper == RSCTL_EG) { + return statesEG(getStatesRSCTL(form->getLeftSF())); + } + else if (oper == RSCTL_EU) { + return statesEU( + getStatesRSCTL(form->getLeftSF()), + getStatesRSCTL(form->getRightSF()) + ); + } + else if (oper == RSCTL_EF) { + return statesEF(getStatesRSCTL(form->getLeftSF())); + } + else if (oper == RSCTL_AX) { + return !getPreE(!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + } + else if (oper == RSCTL_AG) { + return !statesEF( + !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + } + else if (oper == RSCTL_AU) { + BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach; + BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach; - return x; - } - else if (oper == RSCTL_AF) - { - return !statesEG( - !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; - } - /***** CONTEXT RESTRICTIONS: ******/ - else if (oper == RSCTL_EX_ACT) - { - return getPreEctx(getStatesRSCTL(form->getLeftSF()), form->getActionsBDD()) * *reach; - } - else if (oper == RSCTL_EG_ACT) - { - return statesEGctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF())); /***** EG? *****/ - } - else if (oper == RSCTL_EU_ACT) - { - return statesEUctx( - form->getActionsBDD(), - getStatesRSCTL(form->getLeftSF()), - getStatesRSCTL(form->getRightSF()) - ); - } - else if (oper == RSCTL_EF_ACT) - { - return statesEFctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF())); - } - else if (oper == RSCTL_AX_ACT) - { - return !getPreEctx(!getStatesRSCTL(form->getLeftSF()) * *reach, form->getActionsBDD()) * *reach; - } - else if (oper == RSCTL_AG_ACT) - { - return !statesEFctx(form->getActionsBDD(), - !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; - } - else if (oper == RSCTL_AU_ACT) - { - BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach; - BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach; + BDD x = !statesEU(ng, ng * nf) * *reach; - BDD x = !statesEUctx(form->getActionsBDD(), ng, ng * nf) * *reach; - if (!x.IsZero()) - x = x * !statesEGctx(form->getActionsBDD(), ng) * *reach; - - return x; - } - else if (oper == RSCTL_AF_ACT) - { - return !statesEGctx(form->getActionsBDD(), - !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + if (!x.IsZero()) { + x = x * !statesEG(ng) * *reach; } - assert(0); // Should never happen - return BDD_FALSE; + return x; + } + else if (oper == RSCTL_AF) { + return !statesEG( + !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + } + /***** CONTEXT RESTRICTIONS: ******/ + else if (oper == RSCTL_EX_ACT) { + return getPreEctx(getStatesRSCTL(form->getLeftSF()), + form->getActionsBDD()) * *reach; + } + else if (oper == RSCTL_EG_ACT) { + return statesEGctx(form->getActionsBDD(), + getStatesRSCTL(form->getLeftSF())); /***** EG? *****/ + } + else if (oper == RSCTL_EU_ACT) { + return statesEUctx( + form->getActionsBDD(), + getStatesRSCTL(form->getLeftSF()), + getStatesRSCTL(form->getRightSF()) + ); + } + else if (oper == RSCTL_EF_ACT) { + return statesEFctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF())); + } + else if (oper == RSCTL_AX_ACT) { + return !getPreEctx(!getStatesRSCTL(form->getLeftSF()) * *reach, + form->getActionsBDD()) * *reach; + } + else if (oper == RSCTL_AG_ACT) { + return !statesEFctx(form->getActionsBDD(), + !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + } + else if (oper == RSCTL_AU_ACT) { + BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach; + BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach; + + BDD x = !statesEUctx(form->getActionsBDD(), ng, ng * nf) * *reach; + + if (!x.IsZero()) { + x = x * !statesEGctx(form->getActionsBDD(), ng) * *reach; + } + + return x; + } + else if (oper == RSCTL_AF_ACT) { + return !statesEGctx(form->getActionsBDD(), + !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach; + } + + assert(0); // Should never happen + return BDD_FALSE; } BDD ModelChecker::statesEG(const BDD &states) { - BDD x = states; - BDD x_p = cuddMgr->bddZero(); - while (x != x_p) - { - x_p = x; - x = x * getPreE(x); - } - return x; + BDD x = states; + BDD x_p = cuddMgr->bddZero(); + + while (x != x_p) { + x_p = x; + x = x * getPreE(x); + } + + return x; } BDD ModelChecker::statesEU(const BDD &statesA, const BDD &statesB) { - BDD x = statesA; - BDD x_p = *reach; - while (x != x_p) - { - x_p = x; - x = x + (statesA * getPreE(x)); - } - return x; + BDD x = statesA; + BDD x_p = *reach; + + while (x != x_p) { + x_p = x; + x = x + (statesA * getPreE(x)); + } + + return x; } BDD ModelChecker::statesEF(const BDD &states) { - BDD x = states; - BDD x_p = *reach; - while (x != x_p) - { - x_p = x; - x = x + (*reach * getPreE(x)); - } - return x; + BDD x = states; + BDD x_p = *reach; + + while (x != x_p) { + x_p = x; + x = x + (*reach * getPreE(x)); + } + + return x; } BDD ModelChecker::statesEGctx(const BDD *contexts, const BDD &states) { - BDD x = states; - BDD x_p = cuddMgr->bddZero(); - while (x != x_p) - { - x_p = x; - x = x * getPreEctx(x, contexts); - } - return x; + BDD x = states; + BDD x_p = cuddMgr->bddZero(); + + while (x != x_p) { + x_p = x; + x = x * getPreEctx(x, contexts); + } + + return x; } -BDD ModelChecker::statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB) +BDD ModelChecker::statesEUctx(const BDD *contexts, const BDD &statesA, + const BDD &statesB) { - BDD x = statesA; - BDD x_p = *reach; - while (x != x_p) - { - x_p = x; - x = x + (statesA * getPreEctx(x, contexts)); - } - return x; + BDD x = statesA; + BDD x_p = *reach; + + while (x != x_p) { + x_p = x; + x = x + (statesA * getPreEctx(x, contexts)); + } + + return x; } BDD ModelChecker::statesEFctx(const BDD *contexts, const BDD &states) { - BDD x = states; - BDD x_p = *reach; - while (x != x_p) - { - x_p = x; - x = x + (*reach * getPreEctx(x, contexts)); - } - return x; + BDD x = states; + BDD x_p = *reach; + + while (x != x_p) { + x_p = x; + x = x + (*reach * getPreEctx(x, contexts)); + } + + return x; } bool ModelChecker::checkRSCTL(FormRSCTL *form) { - if (form->isERSCTL()) - return checkRSCTLbmc(form); - else - return checkRSCTLfull(form); + if (form->isERSCTL()) { + return checkRSCTLbmc(form); + } + else { + return checkRSCTLfull(form); + } } bool ModelChecker::checkRSCTLfull(FormRSCTL *form) { - if (opts->measure) - opts->ver_time = cpuTime(); + if (opts->measure) { + opts->ver_time = cpuTime(); + } - assert(form != nullptr); + assert(form != nullptr); - bool result = false; + bool result = false; - VERB("Model checking for RSCTL formula: " << form->toStr()); + VERB("Model checking for RSCTL formula: " << form->toStr()); - VERB("Processing the formula: encoding entities"); - form->encodeEntities(srs); - VERB("Entities encoded"); + VERB("Processing the formula: encoding entities"); + form->encodeEntities(srs); + VERB("Entities encoded"); - VERB("Processing the formula: encoding actions/contexts"); - form->encodeActions(srs); - VERB("Contexts encoded"); + VERB("Processing the formula: encoding actions/contexts"); + form->encodeActions(srs); + VERB("Contexts encoded"); - assert(reach == nullptr); + assert(reach == nullptr); - reach = new BDD(*initStates); - BDD reach_p = cuddMgr->bddZero(); + reach = new BDD(*initStates); + BDD reach_p = cuddMgr->bddZero(); - VERB("Generating state space"); + VERB("Generating state space"); - unsigned int k = 0; + unsigned int k = 0; - while (*reach != reach_p) - { + while (*reach != reach_p) { - if (opts->show_progress) - { - cout << "\rIteration " << ++k << flush; - } - - if (opts->reorder_reach) - { - VERB_L2("Reordering") - Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); - } - - reach_p = *reach; - *reach += getSucc(*reach); + if (opts->show_progress) { + cout << "\rIteration " << ++k << flush; } - if (opts->show_progress) cout << endl; - - VERB("Checking the formula"); - - //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero()) - if (*initStates * getStatesRSCTL(form) == *initStates) - { - result = true; - } - else - { - result = false; + if (opts->reorder_reach) { + VERB_L2("Reordering") + Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); } - cleanup(); + reach_p = *reach; + *reach += getSucc(*reach); + } - cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold") << endl; + if (opts->show_progress) { + cout << endl; + } - if (opts->measure) - { - opts->ver_time = cpuTime() - opts->ver_time; - opts->ver_mem = memUsed(); - } + VERB("Checking the formula"); - return result; + //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero()) + if (*initStates * getStatesRSCTL(form) == *initStates) { + result = true; + } + else { + result = false; + } + + cleanup(); + + cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold") + << endl; + + if (opts->measure) { + opts->ver_time = cpuTime() - opts->ver_time; + opts->ver_mem = memUsed(); + } + + return result; } bool ModelChecker::checkRSCTLbmc(FormRSCTL *form) { - if (opts->measure) - opts->ver_time = cpuTime(); + if (opts->measure) { + opts->ver_time = cpuTime(); + } - assert(form != nullptr); + assert(form != nullptr); - if (!form->isERSCTL()) - { - FERROR("Formula " << form->toStr() << " is not syntactically an ERSCTL formula"); + if (!form->isERSCTL()) { + FERROR("Formula " << form->toStr() << + " is not syntactically an ERSCTL formula"); + } + + bool result = false; + + VERB("Bounded model checking for RSCTL formula: " << form->toStr()); + + VERB("Processing the formula: encoding entities"); + form->encodeEntities(srs); + VERB("Entities encoded"); + + VERB("Processing the formula: encoding actions/contexts"); + form->encodeActions(srs); + VERB("Contexts encoded"); + + assert(reach == nullptr); + + reach = new BDD(*initStates); + BDD reach_p = cuddMgr->bddZero(); + + unsigned int k = 0; + + while (*reach != reach_p) { + if (opts->show_progress) { + cout << "\rIteration " << ++k << flush; } - bool result = false; - - VERB("Bounded model checking for RSCTL formula: " << form->toStr()); - - VERB("Processing the formula: encoding entities"); - form->encodeEntities(srs); - VERB("Entities encoded"); - - VERB("Processing the formula: encoding actions/contexts"); - form->encodeActions(srs); - VERB("Contexts encoded"); - - assert(reach == nullptr); - - reach = new BDD(*initStates); - BDD reach_p = cuddMgr->bddZero(); - - unsigned int k = 0; - - while (*reach != reach_p) - { - if (opts->show_progress) - { - cout << "\rIteration " << ++k << flush; - } - - //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero()) - if (*initStates * getStatesRSCTL(form) == *initStates) - { - result = true; - break; - } - - reach_p = *reach; - *reach += getSucc(*reach); + //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero()) + if (*initStates * getStatesRSCTL(form) == *initStates) { + result = true; + break; } - if (opts->show_progress) cout << endl; + reach_p = *reach; + *reach += getSucc(*reach); + } - cleanup(); + if (opts->show_progress) { + cout << endl; + } - cout << "Formula " << form->toStr() << " " << (result ? "holds" : "does not hold") << endl; + cleanup(); - if (opts->measure) - { - opts->ver_time = cpuTime() - opts->ver_time; - opts->ver_mem = memUsed(); - } + cout << "Formula " << form->toStr() << " " << (result ? "holds" : + "does not hold") << endl; - return result; + if (opts->measure) { + opts->ver_time = cpuTime() - opts->ver_time; + opts->ver_mem = memUsed(); + } + + return result; } void ModelChecker::cleanup(void) { - delete reach; - reach = nullptr; + delete reach; + reach = nullptr; } /** EOF **/ \ No newline at end of file diff --git a/mc.hh b/mc.hh index 20d22fb..f6d7557 100644 --- a/mc.hh +++ b/mc.hh @@ -20,7 +20,7 @@ class ModelChecker SymRS *srs; Options *opts; Cudd *cuddMgr; - BDD *initStates; + BDD *initStates; vector *pv; vector *pv_succ; BDD *pv_E; @@ -29,21 +29,21 @@ class ModelChecker BDD *reach; vector *trp; BDD *trm; - - // Context Automaton - bool using_ctx_aut; - vector *pv_ca; - vector *pv_ca_succ; - BDD *pv_ca_E; - BDD *pv_ca_succ_E; - + + // Context Automaton + bool using_ctx_aut; + vector *pv_ca; + vector *pv_ca_succ; + BDD *pv_ca_E; + BDD *pv_ca_succ_E; + unsigned int trp_size; unsigned int totalStateVars; - + /** * @brief Abstracts away (in-place!) the context automaton states */ - void dropCtxAutStatePart(BDD &states); + void dropCtxAutStatePart(BDD &states); BDD getSucc(const BDD &states); BDD getPreE(const BDD &states); @@ -57,7 +57,7 @@ class ModelChecker BDD statesEFctx(const BDD *contexts, const BDD &states); void cleanup(void); -public: + public: ModelChecker(SymRS *srs, Options *opts); void printReach(void); diff --git a/memtime.hh b/memtime.hh index 1bcef66..fcc4a2f 100644 --- a/memtime.hh +++ b/memtime.hh @@ -29,39 +29,42 @@ typedef long long int64; static inline double cpuTime(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } static inline int memReadStat(void) { - char name[256]; - pid_t pid = getpid(); - sprintf(name, "/proc/%d/statm", pid); - FILE* in = fopen(name, "rb"); - if (in == nullptr) - { - return 0; + char name[256]; + pid_t pid = getpid(); + sprintf(name, "/proc/%d/statm", pid); + FILE *in = fopen(name, "rb"); + + if (in == nullptr) { + return 0; + } + + int value; + + for (int field = 0; field >= 0; --field) { + if (fscanf(in, "%d", &value) == EOF) { + FERROR("EOF"); } - int value; - for (int field = 0; field >= 0; --field) - { - if (fscanf(in, "%d", &value) == EOF) - FERROR("EOF"); - } - fclose(in); - return value; + } + + fclose(in); + return value; } static inline int64 memUsedInt64() { - return (int64)memReadStat() * (int64)getpagesize(); + return (int64)memReadStat() * (int64)getpagesize(); } static inline double memUsed() { - return memUsedInt64() / 1048576.0; + return memUsedInt64() / 1048576.0; } #endif diff --git a/options.hh b/options.hh index 0f494a0..e33af84 100644 --- a/options.hh +++ b/options.hh @@ -1,9 +1,10 @@ #ifndef RS_OPTIONS_HH #define RS_OPTIONS_HH -class Options { +class Options +{ -public: + public: unsigned int verbose; bool show_progress; bool measure; @@ -18,19 +19,19 @@ public: Options(void) { - verbose = 0; - show_progress = false; - measure = false; + verbose = 0; + show_progress = false; + measure = false; - part_tr_rel = false; + part_tr_rel = false; - reorder_reach = false; - reorder_trans = false; + reorder_reach = false; + reorder_trans = false; - enc_time = 0; - enc_mem = 0; - ver_time = 0; - ver_mem = 0; + enc_time = 0; + enc_mem = 0; + ver_time = 0; + ver_mem = 0; } }; diff --git a/rs.cc b/rs.cc index 4b844f4..684aa4d 100644 --- a/rs.cc +++ b/rs.cc @@ -9,299 +9,320 @@ #include "rs.hh" RctSys::RctSys(void) - : current_process_defined(false) + : current_process_defined(false) { - ctx_aut = nullptr; + ctx_aut = nullptr; } bool RctSys::hasEntity(std::string name) { - if (entities_names.find(name) == entities_names.end()) - return false; - else - return true; + if (entities_names.find(name) == entities_names.end()) { + return false; + } + else { + return true; + } } void RctSys::addEntity(std::string name) { - if (!hasEntity(name)) - { - Entity new_entity_id = entities_ids.size(); + if (!hasEntity(name)) { + Entity new_entity_id = entities_ids.size(); - VERB_L2("Adding entity: " << name << " index=" << new_entity_id); + VERB_L2("Adding entity: " << name << " index=" << new_entity_id); - entities_ids.push_back(name); - entities_names[name] = new_entity_id; - } + entities_ids.push_back(name); + entities_names[name] = new_entity_id; + } } std::string RctSys::getEntityName(Entity entityID) { - if (entityID < entities_ids.size()) - return entities_ids[entityID]; - else - { - FERROR("No such entity ID: " << entityID); - return "??"; - } + if (entityID < entities_ids.size()) { + return entities_ids[entityID]; + } + else { + FERROR("No such entity ID: " << entityID); + return "??"; + } } Entity RctSys::getEntityID(std::string name) { - if (!hasEntity(name)) - { - FERROR("No such entity: " << name); - } - return entities_names[name]; + if (!hasEntity(name)) { + FERROR("No such entity: " << name); + } + + return entities_names[name]; } void RctSys::setCurrentProcess(std::string processName) { - VERB_LN(2, "Current Process: " << processName); - - if (!hasProcess(processName)) - { - addProcess(processName); - } - - current_proc_id = getProcessID(processName); - current_process_defined = true; + VERB_LN(2, "Current Process: " << processName); + + if (!hasProcess(processName)) { + addProcess(processName); + } + + current_proc_id = getProcessID(processName); + current_process_defined = true; } void RctSys::addProcess(std::string processName) { - if (!hasProcess(processName)) - { - Process new_proc_id = processes_ids.size(); + if (!hasProcess(processName)) { + Process new_proc_id = processes_ids.size(); - VERB_L2("Adding process: " << processName << " index=" << new_proc_id); + VERB_L2("Adding process: " << processName << " index=" << new_proc_id); - processes_ids.push_back(processName); - processes_names[processName] = new_proc_id; - - // reactions for the new process - proc_reactions[new_proc_id] = Reactions(); - assert(proc_reactions.size() == new_proc_id+1); - } + processes_ids.push_back(processName); + processes_names[processName] = new_proc_id; + + // reactions for the new process + proc_reactions[new_proc_id] = Reactions(); + assert(proc_reactions.size() == new_proc_id + 1); + } } bool RctSys::hasProcess(std::string processName) { - if (processes_names.find(processName) == processes_names.end()) - return false; - else - return true; + if (processes_names.find(processName) == processes_names.end()) { + return false; + } + else { + return true; + } } Process RctSys::getProcessID(std::string processName) { - if (!hasProcess(processName)) - { - FERROR("No such process: " << processName); - } - return processes_names[processName]; + if (!hasProcess(processName)) { + FERROR("No such process: " << processName); + } + + return processes_names[processName]; } std::string RctSys::getProcessName(Process processID) { - if (processID < processes_ids.size()) - return processes_ids[processID]; - else - { - FERROR("No such process ID: " << processID); - } + if (processID < processes_ids.size()) { + return processes_ids[processID]; + } + else { + FERROR("No such process ID: " << processID); + } } void RctSys::pushReactant(std::string entityName) { - if (!hasEntity(entityName)) - addEntity(entityName); - tmpReactants.insert(getEntityID(entityName)); + if (!hasEntity(entityName)) { + addEntity(entityName); + } + + tmpReactants.insert(getEntityID(entityName)); } void RctSys::pushInhibitor(std::string entityName) { - if (!hasEntity(entityName)) - addEntity(entityName); - tmpInhibitors.insert(getEntityID(entityName)); + if (!hasEntity(entityName)) { + addEntity(entityName); + } + + tmpInhibitors.insert(getEntityID(entityName)); } void RctSys::pushProduct(std::string entityName) { - if (!hasEntity(entityName)) - addEntity(entityName); - tmpProducts.insert(getEntityID(entityName)); + if (!hasEntity(entityName)) { + addEntity(entityName); + } + + tmpProducts.insert(getEntityID(entityName)); } void RctSys::addReactionForCurrentProcess(Reaction reaction) { - if (!current_process_defined) - { - FERROR("Internal error. Current process is not set!"); - } - proc_reactions[current_proc_id].push_back(reaction); + if (!current_process_defined) { + FERROR("Internal error. Current process is not set!"); + } + + proc_reactions[current_proc_id].push_back(reaction); } void RctSys::commitReaction(void) { - VERB_L3("Saving reaction"); + VERB_L3("Saving reaction"); - Reaction r; + Reaction r; - r.rctt = tmpReactants; - r.inhib = tmpInhibitors; - r.prod = tmpProducts; + r.rctt = tmpReactants; + r.inhib = tmpInhibitors; + r.prod = tmpProducts; - addReactionForCurrentProcess(r); + addReactionForCurrentProcess(r); - tmpReactants.clear(); - tmpInhibitors.clear(); - tmpProducts.clear(); + tmpReactants.clear(); + tmpInhibitors.clear(); + tmpProducts.clear(); } std::string RctSys::entitiesToStr(const Entities &entities) { - std::string s = " "; - for (auto a = entities.begin(); a != entities.end(); ++a) - { - s += entityToStr(*a) + " "; - } - return s; + std::string s = " "; + + for (auto a = entities.begin(); a != entities.end(); ++a) { + s += entityToStr(*a) + " "; + } + + return s; } void RctSys::showReactions(void) { - cout << "# Reactions:" << endl; - - for (unsigned int proc_id = 0; proc_id < processes_ids.size(); ++proc_id) - { - cout << endl; - cout << " . proc = \"" << getProcessName(proc_id) << "\":" << endl; - for (const auto &r : proc_reactions[proc_id]) - { - cout << " * (R={" << entitiesToStr(r.rctt) << "}," - << "I={" << entitiesToStr(r.inhib) << "}," - << "P={" << entitiesToStr(r.prod) << "})" << endl; - } - } - cout << endl; + cout << "# Reactions:" << endl; + + for (unsigned int proc_id = 0; proc_id < processes_ids.size(); ++proc_id) { + cout << endl; + cout << " . proc = \"" << getProcessName(proc_id) << "\":" << endl; + + for (const auto &r : proc_reactions[proc_id]) { + cout << " * (R={" << entitiesToStr(r.rctt) << "}," + << "I={" << entitiesToStr(r.inhib) << "}," + << "P={" << entitiesToStr(r.prod) << "})" << endl; + } + } + + cout << endl; } void RctSys::pushStateEntity(std::string entityName) { - if (!hasEntity(entityName)) - { - FERROR("No such entity: " << entityName); - } - tmpState.insert(getEntityID(entityName)); + if (!hasEntity(entityName)) { + FERROR("No such entity: " << entityName); + } + + tmpState.insert(getEntityID(entityName)); } void RctSys::commitInitState(void) { - if (ctx_aut != nullptr) - { - FERROR("Initial RS states must not be used with context automaton"); - } - initStates.insert(tmpState); - tmpState.clear(); + if (ctx_aut != nullptr) { + FERROR("Initial RS states must not be used with context automaton"); + } + + initStates.insert(tmpState); + tmpState.clear(); } void RctSys::addActionEntity(std::string entityName) { - if (!hasEntity(entityName)) - addEntity(entityName); - actionEntities.insert(getEntityID(entityName)); + if (!hasEntity(entityName)) { + addEntity(entityName); + } + + actionEntities.insert(getEntityID(entityName)); } void RctSys::addActionEntity(Entity entity) { - if (!isActionEntity(entity)) - actionEntities.insert(entity); + if (!isActionEntity(entity)) { + actionEntities.insert(entity); + } } bool RctSys::isActionEntity(Entity entity) { - if (actionEntities.count(entity) > 0) - return true; - else - return false; + if (actionEntities.count(entity) > 0) { + return true; + } + else { + return false; + } } void RctSys::showActionEntities(void) { - cout << "# Context entities:"; - for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a) - { - cout << " " << getEntityName(*a); - } - cout << endl; + cout << "# Context entities:"; + + for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a) { + cout << " " << getEntityName(*a); + } + + cout << endl; } void RctSys::showInitialStates(void) { - cout << "# Initial states:" << endl; - for (auto s = initStates.begin(); s != initStates.end(); ++s) - { - cout << " *"; - for (auto a = s->begin(); a != s->end(); ++a) - { - cout << " " << getEntityName(*a); - } - cout << endl; + cout << "# Initial states:" << endl; + + for (auto s = initStates.begin(); s != initStates.end(); ++s) { + cout << " *"; + + for (auto a = s->begin(); a != s->end(); ++a) { + cout << " " << getEntityName(*a); } + + cout << endl; + } } void RctSys::printSystem(void) { - if (!usingContextAutomaton()) - showInitialStates(); - showActionEntities(); - showReactions(); - - if (ctx_aut != nullptr) ctx_aut->printAutomaton(); + if (!usingContextAutomaton()) { + showInitialStates(); + } + + showActionEntities(); + showReactions(); + + if (ctx_aut != nullptr) { + ctx_aut->printAutomaton(); + } } void RctSys::ctxAutEnable(void) { - assert(ctx_aut == nullptr); - if (initStatesDefined()) - { - FERROR("Initial states must not be defined if using context automaton"); - } - ctx_aut = new CtxAut(opts, this); + assert(ctx_aut == nullptr); + + if (initStatesDefined()) { + FERROR("Initial states must not be defined if using context automaton"); + } + + ctx_aut = new CtxAut(opts, this); } void RctSys::ctxAutAddState(std::string stateName) { - assert(ctx_aut != nullptr); - ctx_aut->addState(stateName); + assert(ctx_aut != nullptr); + ctx_aut->addState(stateName); } void RctSys::ctxAutSetInitState(std::string stateName) { - assert(ctx_aut != nullptr); - ctx_aut->setInitState(stateName); + assert(ctx_aut != nullptr); + ctx_aut->setInitState(stateName); } -void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateName) +void RctSys::ctxAutAddTransition(std::string srcStateName, + std::string dstStateName) { - assert(ctx_aut != nullptr); - ctx_aut->addTransition(srcStateName, dstStateName); + assert(ctx_aut != nullptr); + ctx_aut->addTransition(srcStateName, dstStateName); } void RctSys::ctxAutPushNamedContextEntity(std::string entityName) { - assert(ctx_aut != nullptr); - - Entity entity_id = getEntityID(entityName); + assert(ctx_aut != nullptr); - // - // We mark the entity as an action entity - // - // This step is required to ensure the minimal number of - // BDD variables used in the encoding of the context sets - // - addActionEntity(entity_id); - - ctx_aut->pushContextEntity(entity_id); + Entity entity_id = getEntityID(entityName); + + // + // We mark the entity as an action entity + // + // This step is required to ensure the minimal number of + // BDD variables used in the encoding of the context sets + // + addActionEntity(entity_id); + + ctx_aut->pushContextEntity(entity_id); } /** EOF **/ diff --git a/rs.hh b/rs.hh index 350d336..c1f184a 100644 --- a/rs.hh +++ b/rs.hh @@ -28,82 +28,106 @@ class CtxAut; class RctSys { - friend class SymRS; - friend class SymRSstate; + friend class SymRS; + friend class SymRSstate; - public: - RctSys(void); - - void setOptions(Options *opts) { this->opts = opts; } - bool hasEntity(std::string entityName); - void addEntity(std::string entityName); - std::string getEntityName(Entity entityID); - - void setCurrentProcess(std::string processName); - void addProcess(std::string processName); - bool hasProcess(std::string processName); - Process getProcessID(std::string processName); - std::string getProcessName(Process processID); - - void addReactionForCurrentProcess(Reaction reaction); - - void pushReactant(std::string entityName); - void pushInhibitor(std::string entityName); - void pushProduct(std::string entityName); - void commitReaction(void); - std::string entityToStr(const Entity entity) { return entities_ids[entity]; } - std::string entitiesToStr(const Entities &entities); - void showReactions(void); - void pushStateEntity(std::string entityName); - void commitInitState(void); - void addActionEntity(std::string entityName); - void addActionEntity(Entity entity); - bool isActionEntity(Entity entity); - void resetInitStates(void) { initStates.clear(); } - unsigned int getEntitiesSize(void) { return entities_ids.size(); } - unsigned int getReactionsSize(void) { return reactions.size(); } - unsigned int getActionsSize(void) { return actionEntities.size(); } - void showInitialStates(void); - void showActionEntities(void); - void printSystem(void); + public: + RctSys(void); - void ctxAutEnable(void); - void ctxAutAddState(std::string stateName); - void ctxAutSetInitState(std::string stateName); - void ctxAutAddTransition(std::string srcStateName, std::string dstStateName); - void ctxAutPushNamedContextEntity(std::string entity_name); - - bool initStatesDefined(void) { return initStates.size() != 0; } - bool usingContextAutomaton(void) { return ctx_aut != nullptr; } - - private: - Reactions reactions; // TODO: to be removed later - ReactionsForProc proc_reactions; - - EntitiesSets initStates; + void setOptions(Options *opts) + { + this->opts = opts; + } + bool hasEntity(std::string entityName); + void addEntity(std::string entityName); + std::string getEntityName(Entity entityID); - Entities actionEntities; + void setCurrentProcess(std::string processName); + void addProcess(std::string processName); + bool hasProcess(std::string processName); + Process getProcessID(std::string processName); + std::string getProcessName(Process processID); - CtxAut *ctx_aut; + void addReactionForCurrentProcess(Reaction reaction); - EntitiesById entities_ids; - EntitiesByName entities_names; + void pushReactant(std::string entityName); + void pushInhibitor(std::string entityName); + void pushProduct(std::string entityName); + void commitReaction(void); + std::string entityToStr(const Entity entity) + { + return entities_ids[entity]; + } + std::string entitiesToStr(const Entities &entities); + void showReactions(void); + void pushStateEntity(std::string entityName); + void commitInitState(void); + void addActionEntity(std::string entityName); + void addActionEntity(Entity entity); + bool isActionEntity(Entity entity); + void resetInitStates(void) + { + initStates.clear(); + } + unsigned int getEntitiesSize(void) + { + return entities_ids.size(); + } + unsigned int getReactionsSize(void) + { + return reactions.size(); + } + unsigned int getActionsSize(void) + { + return actionEntities.size(); + } + void showInitialStates(void); + void showActionEntities(void); + void printSystem(void); - ProcessesById processes_ids; - ProcessesByName processes_names; - - Process current_proc_id; - bool current_process_defined; + void ctxAutEnable(void); + void ctxAutAddState(std::string stateName); + void ctxAutSetInitState(std::string stateName); + void ctxAutAddTransition(std::string srcStateName, std::string dstStateName); + void ctxAutPushNamedContextEntity(std::string entity_name); - Entities tmpReactants; - Entities tmpInhibitors; - Entities tmpProducts; + bool initStatesDefined(void) + { + return initStates.size() != 0; + } + bool usingContextAutomaton(void) + { + return ctx_aut != nullptr; + } - Entities tmpState; + private: + Reactions reactions; // TODO: to be removed later + ReactionsForProc proc_reactions; - Options *opts; + EntitiesSets initStates; - Entity getEntityID(std::string entityName); + Entities actionEntities; + + CtxAut *ctx_aut; + + EntitiesById entities_ids; + EntitiesByName entities_names; + + ProcessesById processes_ids; + ProcessesByName processes_names; + + Process current_proc_id; + bool current_process_defined; + + Entities tmpReactants; + Entities tmpInhibitors; + Entities tmpProducts; + + Entities tmpState; + + Options *opts; + + Entity getEntityID(std::string entityName); }; diff --git a/rsin_driver.cc b/rsin_driver.cc index c78679a..ddc5352 100644 --- a/rsin_driver.cc +++ b/rsin_driver.cc @@ -2,61 +2,60 @@ #include "rsin_parser.hh" rsin_driver::rsin_driver(void) -: trace_scanning(false), trace_parsing(false) + : trace_scanning(false), trace_parsing(false) { - initialise(); + initialise(); } rsin_driver::rsin_driver(RctSys *rs) -: trace_scanning(false), trace_parsing(false) + : trace_scanning(false), trace_parsing(false) { - initialise(); - this->rs = rs; + initialise(); + this->rs = rs; } void rsin_driver::initialise(void) { - rs = nullptr; - rsctlform = nullptr; - opts = nullptr; - use_ctx_aut = false; - use_concentrations = false; + rs = nullptr; + rsctlform = nullptr; + opts = nullptr; + use_ctx_aut = false; + use_concentrations = false; } rsin_driver::~rsin_driver () { - // placeholder + // placeholder } int rsin_driver::parse(const std::string &f) { - file = f; - scan_begin(); - yy::rsin_parser parser(*this); - parser.set_debug_level(trace_parsing); - int res = parser.parse(); - scan_end(); - return res; + file = f; + scan_begin(); + yy::rsin_parser parser(*this); + parser.set_debug_level(trace_parsing); + int res = parser.parse(); + scan_end(); + return res; } void rsin_driver::error(const yy::location &l, const std::string &m) { - std::cerr << l << ": " << m << std::endl; + std::cerr << l << ": " << m << std::endl; } void rsin_driver::error(const std::string &m) { - std::cerr << m << std::endl; + std::cerr << m << std::endl; } FormRSCTL *rsin_driver::getFormRSCTL(void) { - if (rsctlform == nullptr) - { - FERROR("RSCTL formula was not supplied!"); - } + if (rsctlform == nullptr) { + FERROR("RSCTL formula was not supplied!"); + } - return rsctlform; + return rsctlform; } // @@ -64,40 +63,40 @@ FormRSCTL *rsin_driver::getFormRSCTL(void) // void rsin_driver::ensureOptionsAllowed(void) { - if (rs != nullptr) - { - FERROR("Options cannot be set/modified after the reaction system is initialised") - } + if (rs != nullptr) { + FERROR("Options cannot be set/modified after the reaction system is initialised") + } } void rsin_driver::ensureReactionSystemReady(void) { - if (rs == nullptr) - setupReactionSystem(); + if (rs == nullptr) { + setupReactionSystem(); + } } void rsin_driver::setupReactionSystem(void) { - assert(rs == nullptr); - rs = new RctSys; - - if (use_ctx_aut) VERB("Using RS with CA") - else VERB("Using ordinary RS") + assert(rs == nullptr); + rs = new RctSys; - rs->setOptions(opts); + if (use_ctx_aut) VERB("Using RS with CA") + else VERB("Using ordinary RS") + + rs->setOptions(opts); } RctSys *rsin_driver::getReactionSystem(void) { - ensureReactionSystemReady(); - assert(rs != nullptr); - return rs; + ensureReactionSystemReady(); + assert(rs != nullptr); + return rs; } void rsin_driver::useContextAutomaton(void) { - ensureOptionsAllowed(); - use_ctx_aut = true; - getReactionSystem()->ctxAutEnable(); + ensureOptionsAllowed(); + use_ctx_aut = true; + getReactionSystem()->ctxAutEnable(); } diff --git a/rsin_driver.hh b/rsin_driver.hh index f150146..04a8aa2 100644 --- a/rsin_driver.hh +++ b/rsin_driver.hh @@ -19,7 +19,7 @@ YY_DECL; // Conducting the whole scanning an parsing of RS class rsin_driver { -public: + public: rsin_driver(void); rsin_driver(RctSys *rs); virtual ~rsin_driver(); @@ -27,10 +27,10 @@ public: //std::map variables; FormRSCTL *rsctlform; Options *opts; - - // options in configuration file: - bool use_ctx_aut; - bool use_concentrations; + + // options in configuration file: + bool use_ctx_aut; + bool use_concentrations; // Handling the scanner void scan_begin(); @@ -41,28 +41,38 @@ public: std::string file; bool trace_parsing; - void setOptions(Options *opts) { this->opts = opts; }; - 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); - void useConcentrations(void) { ensureOptionsAllowed(); use_concentrations = true; }; - - void ensureReactionSystemReady(void); - void setupReactionSystem(void); - - RctSys *getReactionSystem(void); - CtxAut *getCtxAut(void); + void ensureOptionsAllowed(void); + void useContextAutomaton(void); + void useConcentrations(void) + { + ensureOptionsAllowed(); + use_concentrations = true; + }; + + void ensureReactionSystemReady(void); + void setupReactionSystem(void); + + RctSys *getReactionSystem(void); + CtxAut *getCtxAut(void); // Error handling. void error(const yy::location &l, const std::string &m); void error(const std::string &m); - -private: + + private: RctSys *rs; - void initialise(void); + void initialise(void); }; #endif diff --git a/symrs.cc b/symrs.cc index 6440e93..aef6158 100644 --- a/symrs.cc +++ b/symrs.cc @@ -8,593 +8,583 @@ SymRS::SymRS(RctSys *rs, Options *opts) { - this->rs = rs; - this->opts = opts; - totalRctSysStateVars = rs->getEntitiesSize(); - totalReactions = rs->getReactionsSize(); - totalActions = rs->getActionsSize(); - - totalCtxAutStateVars = getCtxAutStateEncodingSize(); - - totalStateVars = totalRctSysStateVars + totalCtxAutStateVars; - - partTrans = nullptr; - monoTrans = nullptr; - - pv_ca = nullptr; - pv_ca_succ = nullptr; - tr_ca = nullptr; + this->rs = rs; + this->opts = opts; + totalRctSysStateVars = rs->getEntitiesSize(); + totalReactions = rs->getReactionsSize(); + totalActions = rs->getActionsSize(); - encode(); + totalCtxAutStateVars = getCtxAutStateEncodingSize(); + + totalStateVars = totalRctSysStateVars + totalCtxAutStateVars; + + partTrans = nullptr; + monoTrans = nullptr; + + pv_ca = nullptr; + pv_ca_succ = nullptr; + tr_ca = nullptr; + + encode(); } BDD SymRS::encEntity_raw(Entity entity, bool succ) const { - BDD r; + BDD r; - if (succ) - r = (*pv_succ)[entity]; - else - r = (*pv)[entity]; + if (succ) { + r = (*pv_succ)[entity]; + } + else { + r = (*pv)[entity]; + } - return r; + return r; } BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ) { - BDD r = BDD_TRUE; + BDD r = BDD_TRUE; - for (const auto &entity : entities) - { - if (succ) r *= encEntitySucc(entity); - else r *= encEntity(entity); + for (const auto &entity : entities) { + if (succ) { + r *= encEntitySucc(entity); } + else { + r *= encEntity(entity); + } + } - return r; + return r; } BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ) { - BDD r = BDD_FALSE; + BDD r = BDD_FALSE; - for (const auto &entity : entities) - { - if (succ) r += encEntitySucc(entity); - else r += encEntity(entity); + for (const auto &entity : entities) { + if (succ) { + r += encEntitySucc(entity); } + else { + r += encEntity(entity); + } + } - return r; + return r; } BDD SymRS::encStateActEntitiesConj(const Entities &entities) { - BDD r = BDD_TRUE; + BDD r = BDD_TRUE; - for (const auto &entity : entities) - { - BDD state_act = encEntity(entity); - int actEntity; - - // if entity is also an action entity, we include it in the encoding - if ((actEntity = getMappedStateToActID(entity)) >= 0) - state_act += encActEntity(actEntity); - - r *= state_act; + for (const auto &entity : entities) { + BDD state_act = encEntity(entity); + int actEntity; + + // if entity is also an action entity, we include it in the encoding + if ((actEntity = getMappedStateToActID(entity)) >= 0) { + state_act += encActEntity(actEntity); } - return r; + r *= state_act; + } + + return r; } BDD SymRS::encStateActEntitiesDisj(const Entities &entities) { - BDD r = BDD_FALSE; + BDD r = BDD_FALSE; - for (const auto &entity : entities) - { - BDD state_act = encEntity(entity); - int actEntity; + for (const auto &entity : entities) { + BDD state_act = encEntity(entity); + int actEntity; - // if entity is also an aciton entity, we include it in the encoding - if ((actEntity = getMappedStateToActID(entity)) >= 0) - state_act += encActEntity(actEntity); - - r += state_act; + // if entity is also an aciton entity, we include it in the encoding + if ((actEntity = getMappedStateToActID(entity)) >= 0) { + state_act += encActEntity(actEntity); } - return r; + r += state_act; + } + + return r; } BDD SymRS::encActEntitiesConj(const Entities &entities) { - BDD r = BDD_TRUE; + BDD r = BDD_TRUE; - for (const auto &entity : entities) - { - Entity actEntity = getMappedStateToActID(entity); - r *= encActEntity(actEntity); - } + for (const auto &entity : entities) { + Entity actEntity = getMappedStateToActID(entity); + r *= encActEntity(actEntity); + } - return r; + return r; } BDD SymRS::compState(const BDD &state) const { - BDD s = state; + BDD s = state; - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) - { - if (!(*pv)[i] * state != cuddMgr->bddZero()) - s *= !(*pv)[i]; + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { + if (!(*pv)[i] * state != cuddMgr->bddZero()) { + s *= !(*pv)[i]; } + } - return s; + return s; } BDD SymRS::compContext(const BDD &context) const { - BDD c = context; + BDD c = context; - for (unsigned int i = 0; i < totalActions; ++i) - { - if (!(*pv_act)[i] * context != cuddMgr->bddZero()) - c *= !(*pv_act)[i]; + for (unsigned int i = 0; i < totalActions; ++i) { + if (!(*pv_act)[i] * context != cuddMgr->bddZero()) { + c *= !(*pv_act)[i]; } + } - return c; + return c; } std::string SymRS::decodedRctSysStateToStr(const BDD &state) { - std::string s = "{ "; - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) - { - if (!(encEntity(i) * state).IsZero()) - { - s += rs->entityToStr(i) + " "; - } + std::string s = "{ "; + + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { + if (!(encEntity(i) * state).IsZero()) { + s += rs->entityToStr(i) + " "; } - s += "}"; - return s; + } + + s += "}"; + return s; } void SymRS::printDecodedRctSysStates(const BDD &states) { - BDD unproc = states; - while (!unproc.IsZero()) - { - BDD t = unproc.PickOneMinterm(*pv_rs); - cout << decodedRctSysStateToStr(t) << endl; - if (opts->verbose > 9) { - t.PrintMinterm(); - cout << endl; - } - unproc -= t; + BDD unproc = states; + + while (!unproc.IsZero()) { + BDD t = unproc.PickOneMinterm(*pv_rs); + cout << decodedRctSysStateToStr(t) << endl; + + if (opts->verbose > 9) { + t.PrintMinterm(); + cout << endl; } + + unproc -= t; + } } void SymRS::initBDDvars(void) { - VERB("Initialising CUDD"); - - cuddMgr = new Cudd(0,0); + VERB("Initialising CUDD"); - VERB("Preparing BDD variables"); + cuddMgr = new Cudd(0, 0); - // used for bddVar - unsigned int bdd_var_idx = 0; - - // used for pv, pv_succ - unsigned int global_state_idx = 0; + VERB("Preparing BDD variables"); - // Variables for reaction system with CA (if used) - pv = new vector(totalStateVars); - pv_succ = new vector(totalStateVars); - pv_E = new BDD(BDD_TRUE); - pv_succ_E = new BDD(BDD_TRUE); - - // Reaction system (no actions, no CA) - pv_rs = new vector(totalRctSysStateVars); - pv_rs_succ = new vector(totalRctSysStateVars); - pv_rs_E = new BDD(BDD_TRUE); - pv_rs_succ_E = new BDD(BDD_TRUE); + // used for bddVar + unsigned int bdd_var_idx = 0; - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) - { - (*pv_rs)[i] = cuddMgr->bddVar(bdd_var_idx++); - (*pv_rs_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); - *pv_rs_E *= (*pv_rs)[i]; - *pv_rs_succ_E *= (*pv_rs_succ)[i]; - - (*pv)[global_state_idx] = (*pv_rs)[i]; - (*pv_succ)[global_state_idx] = (*pv_rs_succ)[i]; - ++global_state_idx; - } + // used for pv, pv_succ + unsigned int global_state_idx = 0; - // CA - if (usingContextAutomaton()) - { - VERB("Context automaton variables"); + // Variables for reaction system with CA (if used) + pv = new vector(totalStateVars); + pv_succ = new vector(totalStateVars); + pv_E = new BDD(BDD_TRUE); + pv_succ_E = new BDD(BDD_TRUE); - pv_ca = new vector(totalCtxAutStateVars); - pv_ca_succ = new vector(totalCtxAutStateVars); - pv_ca_E = new BDD(BDD_TRUE); - pv_ca_succ_E = new BDD(BDD_TRUE); + // Reaction system (no actions, no CA) + pv_rs = new vector(totalRctSysStateVars); + pv_rs_succ = new vector(totalRctSysStateVars); + pv_rs_E = new BDD(BDD_TRUE); + pv_rs_succ_E = new BDD(BDD_TRUE); - for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) - { - (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++); - (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); - *pv_ca_E *= (*pv_ca)[i]; - *pv_ca_succ_E *= (*pv_ca_succ)[i]; - - (*pv)[global_state_idx] = (*pv_ca)[i]; - (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i]; - ++global_state_idx; - } - } - - // Actions/Contexts - pv_act = new vector(totalActions); - pv_act_E = new BDD(BDD_TRUE); - - for (unsigned int i = 0; i < totalActions; ++i) - { - (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++); - *pv_act_E *= (*pv_act)[i]; + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { + (*pv_rs)[i] = cuddMgr->bddVar(bdd_var_idx++); + (*pv_rs_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); + *pv_rs_E *= (*pv_rs)[i]; + *pv_rs_succ_E *= (*pv_rs_succ)[i]; + + (*pv)[global_state_idx] = (*pv_rs)[i]; + (*pv_succ)[global_state_idx] = (*pv_rs_succ)[i]; + ++global_state_idx; + } + + // CA + if (usingContextAutomaton()) { + VERB("Context automaton variables"); + + pv_ca = new vector(totalCtxAutStateVars); + pv_ca_succ = new vector(totalCtxAutStateVars); + pv_ca_E = new BDD(BDD_TRUE); + pv_ca_succ_E = new BDD(BDD_TRUE); + + for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) { + (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++); + (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++); + *pv_ca_E *= (*pv_ca)[i]; + *pv_ca_succ_E *= (*pv_ca_succ)[i]; + + (*pv)[global_state_idx] = (*pv_ca)[i]; + (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i]; + ++global_state_idx; } - - // Quantification BDDs - - *pv_E = *pv_rs_E; - *pv_succ_E = *pv_rs_succ_E; - - if (usingContextAutomaton()) - { - *pv_E *= *pv_ca_E; - *pv_succ_E *= *pv_ca_succ_E; - } + } - VERB("All BDD variables ready"); + // Actions/Contexts + pv_act = new vector(totalActions); + pv_act_E = new BDD(BDD_TRUE); + + for (unsigned int i = 0; i < totalActions; ++i) { + (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++); + *pv_act_E *= (*pv_act)[i]; + } + + // Quantification BDDs + + *pv_E = *pv_rs_E; + *pv_succ_E = *pv_rs_succ_E; + + if (usingContextAutomaton()) { + *pv_E *= *pv_ca_E; + *pv_succ_E *= *pv_ca_succ_E; + } + + VERB("All BDD variables ready"); } void SymRS::encodeTransitions(void) { - DecompReactions dr; + DecompReactions dr; - VERB("Decomposing reactions"); - for (unsigned int i = 0; i < totalReactions; ++i) - { - ReactionCond cond; - cond.rctt = rs->reactions[i].rctt; - cond.inhib = rs->reactions[i].inhib; - - for (Entities::iterator p = rs->reactions[i].prod.begin(); - p != rs->reactions[i].prod.end(); ++p) - { - dr[*p].push_back(cond); - } + VERB("Decomposing reactions"); + + for (unsigned int i = 0; i < totalReactions; ++i) { + ReactionCond cond; + cond.rctt = rs->reactions[i].rctt; + cond.inhib = rs->reactions[i].inhib; + + for (Entities::iterator p = rs->reactions[i].prod.begin(); + p != rs->reactions[i].prod.end(); ++p) { + dr[*p].push_back(cond); + } + } + + VERB("Encoding reactions"); + + if (opts->part_tr_rel) { + VERB("Using partitioned transition relation encoding"); + partTrans = new vector(totalRctSysStateVars); + } + else { + VERB("Using monolithic transition relation encoding"); + monoTrans = new BDD(BDD_TRUE); + } + + for (unsigned int p = 0; p < totalRctSysStateVars; ++p) { + VERB_L3("Encoding for successor " << p); + + DecompReactions::iterator di; + + if ((di = dr.find(p)) == dr.end()) { + // there is no reaction producing p: + if (opts->part_tr_rel) { + (*partTrans)[p] = !encEntitySucc(p); + } + else { + *monoTrans *= !encEntitySucc(p); + } + } + else { + // di - reactions producing p + + BDD conditions = BDD_FALSE; + + assert(di->second.size() > 0); + + for (unsigned int j = 0; j < di->second.size(); ++j) { + conditions += encStateActEntitiesConj(di->second[j].rctt) * + !encStateActEntitiesDisj(di->second[j].inhib); + } + + if (opts->part_tr_rel) { + (*partTrans)[p] = conditions * encEntitySucc(p); + (*partTrans)[p] += !conditions * !encEntitySucc(p); + } + else { + *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc( + p)); + } } - VERB("Encoding reactions"); - - if (opts->part_tr_rel) - { - VERB("Using partitioned transition relation encoding"); - partTrans = new vector(totalRctSysStateVars); - } - else - { - VERB("Using monolithic transition relation encoding"); - monoTrans = new BDD(BDD_TRUE); + if (opts->reorder_trans) { + VERB_L2("Reordering"); + Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); } - for (unsigned int p = 0; p < totalRctSysStateVars; ++p) - { - VERB_L3("Encoding for successor " << p); + } - DecompReactions::iterator di; + VERB("Reactions ready"); - if ((di = dr.find(p)) == dr.end()) - { - // there is no reaction producing p: - if (opts->part_tr_rel) - (*partTrans)[p] = !encEntitySucc(p); - else - { - *monoTrans *= !encEntitySucc(p); - } - } - else - { - // di - reactions producing p - - BDD conditions = BDD_FALSE; - - assert(di->second.size() > 0); - - for (unsigned int j = 0; j < di->second.size(); ++j) - { - conditions += encStateActEntitiesConj(di->second[j].rctt) * !encStateActEntitiesDisj(di->second[j].inhib); - } - - if (opts->part_tr_rel) - { - (*partTrans)[p] = conditions * encEntitySucc(p); - (*partTrans)[p] += !conditions * !encEntitySucc(p); - } - else - { - *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc(p)); - } - } - if (opts->reorder_trans) - { - VERB_L2("Reordering"); - Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000); - } + if (usingContextAutomaton()) { + VERB("Augmenting transition relation encoding with the transition relation for context automaton"); + if (opts->part_tr_rel) { + assert(0); } + else { + assert(tr_ca != nullptr); + *monoTrans *= *tr_ca; + } + } - VERB("Reactions ready"); - - if (usingContextAutomaton()) - { - VERB("Augmenting transition relation encoding with the transition relation for context automaton"); - if (opts->part_tr_rel) - { - assert(0); - } - else - { - assert(tr_ca != nullptr); - *monoTrans *= *tr_ca; - } - } - - VERB("Transition relation encoded") + VERB("Transition relation encoded") } BDD SymRS::getEncState(const Entities &entities) { - assert(0); - //BDD state = compState(encEntitiesConj(rs->initState)); - //for (RctSys::Entities::iterator at = rs->actionEntities.begin(); at != rs->actionEntities.end(); ++at) - //{ - // state = state.ExistAbstract(encEntity(*at)); - //} - return BDD_FALSE; + assert(0); + //BDD state = compState(encEntitiesConj(rs->initState)); + //for (RctSys::Entities::iterator at = rs->actionEntities.begin(); at != rs->actionEntities.end(); ++at) + //{ + // state = state.ExistAbstract(encEntity(*at)); + //} + return BDD_FALSE; } BDD SymRS::encNoContext(void) { - BDD noContextBDD = BDD_TRUE; + BDD noContextBDD = BDD_TRUE; - for (unsigned int i = 0; i < totalActions; ++i) - { - noContextBDD *= !(*pv_act)[i]; - } + for (unsigned int i = 0; i < totalActions; ++i) { + noContextBDD *= !(*pv_act)[i]; + } - return noContextBDD; + return noContextBDD; } void SymRS::encodeInitStates(void) { - if (usingContextAutomaton()) - { - VERB("Encoding initial states (using context automaton)"); - encodeInitStatesForCtxAut(); - } - else - { - VERB("Encoding initial states (for the action entities method -- no CA)"); - encodeInitStatesNoCtxAut(); - } - VERB("Initial states encoded"); + if (usingContextAutomaton()) { + VERB("Encoding initial states (using context automaton)"); + encodeInitStatesForCtxAut(); + } + else { + VERB("Encoding initial states (for the action entities method -- no CA)"); + encodeInitStatesNoCtxAut(); + } + + VERB("Initial states encoded"); } void SymRS::encodeInitStatesForCtxAut(void) { - initStates = new BDD(BDD_TRUE); + initStates = new BDD(BDD_TRUE); - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) - { - *initStates *= !(*pv)[i]; - } + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { + *initStates *= !(*pv)[i]; + } - *initStates *= getEncCtxAutInitState(); + *initStates *= getEncCtxAutInitState(); } void SymRS::encodeInitStatesNoCtxAut(void) { #ifndef NDEBUG - if (opts->part_tr_rel) - assert(partTrans != nullptr); + + if (opts->part_tr_rel) { + assert(partTrans != nullptr); + } + #endif - initStates = new BDD(BDD_FALSE); - - for (auto state = rs->initStates.begin(); - state != rs->initStates.end(); - ++state) - { - VERB("Encoding a single inital state"); - BDD newInitState = compState(encEntitiesConj(*state)); - BDD q = BDD_TRUE; - if (opts->part_tr_rel) - { - for (unsigned int i = 0; i < partTrans->size(); ++i) - { - q *= newInitState * (*partTrans)[i] * encNoContext(); - } - } - else - { - q *= newInitState * *monoTrans * encNoContext(); - } - - q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); - q = q.ExistAbstract(*pv_act_E); + initStates = new BDD(BDD_FALSE); - *initStates += q; + for (auto state = rs->initStates.begin(); + state != rs->initStates.end(); + ++state) { + VERB("Encoding a single inital state"); + BDD newInitState = compState(encEntitiesConj(*state)); + BDD q = BDD_TRUE; + + if (opts->part_tr_rel) { + for (unsigned int i = 0; i < partTrans->size(); ++i) { + q *= newInitState * (*partTrans)[i] * encNoContext(); + } } + else { + q *= newInitState * *monoTrans * encNoContext(); + } + + q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv); + q = q.ExistAbstract(*pv_act_E); + + *initStates += q; + } } void SymRS::mapStateToAct(void) { - VERB("Mapping state variables to action variables"); - unsigned int j = 0; - for (unsigned int i = 0; i < totalRctSysStateVars; ++i) - { - if (rs->isActionEntity(i)) { - stateToAct.push_back(j++); - } - else - { - stateToAct.push_back(-1); - } + VERB("Mapping state variables to action variables"); + unsigned int j = 0; + + for (unsigned int i = 0; i < totalRctSysStateVars; ++i) { + if (rs->isActionEntity(i)) { + stateToAct.push_back(j++); } - const unsigned int verbosity_level = 9; - if (opts->verbose > verbosity_level) - { - for (unsigned int i = 0; i < stateToAct.size(); ++i) - { - cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << stateToAct[i] << endl; - } + else { + stateToAct.push_back(-1); } + } + + const unsigned int verbosity_level = 9; + + if (opts->verbose > verbosity_level) { + for (unsigned int i = 0; i < stateToAct.size(); ++i) { + cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << + stateToAct[i] << endl; + } + } } void SymRS::encode(void) { - VERB("Encoding..."); + VERB("Encoding..."); - if (opts->measure) - { - opts->enc_time = cpuTime(); - opts->enc_mem = memUsed(); - } + if (opts->measure) { + opts->enc_time = cpuTime(); + opts->enc_mem = memUsed(); + } - mapStateToAct(); + mapStateToAct(); - initBDDvars(); - - if (usingContextAutomaton()) - { - encodeCtxAutTrans(); - } - else - { - VERB_LN(3, "Not using context automata, not encoding TR for CA") - } - - encodeTransitions(); - encodeInitStates(); + initBDDvars(); - if (opts->measure) - { - opts->enc_time = cpuTime() - opts->enc_time; - opts->enc_mem = memUsed() - opts->enc_mem; - } + if (usingContextAutomaton()) { + encodeCtxAutTrans(); + } + else { + VERB_LN(3, "Not using context automata, not encoding TR for CA") + } - VERB("Encoding done"); + encodeTransitions(); + encodeInitStates(); + + if (opts->measure) { + opts->enc_time = cpuTime() - opts->enc_time; + opts->enc_mem = memUsed() - opts->enc_mem; + } + + VERB("Encoding done"); } -BDD SymRS::encActStrEntity(std::string name) const +BDD SymRS::encActStrEntity(std::string name) const { - int id = getMappedStateToActID(rs->getEntityID(name)); - if (id < 0) - { - FERROR("Entity \"" << name << "\" not defined as context entity"); - return BDD_FALSE; - } else { - return encActEntity(getMappedStateToActID(rs->getEntityID(name))); - } + int id = getMappedStateToActID(rs->getEntityID(name)); + + if (id < 0) { + FERROR("Entity \"" << name << "\" not defined as context entity"); + return BDD_FALSE; + } + else { + return encActEntity(getMappedStateToActID(rs->getEntityID(name))); + } } size_t SymRS::getCtxAutStateEncodingSize(void) { - if (!usingContextAutomaton()) return 0; - - assert(rs->ctx_aut != nullptr); - - size_t bitCount = 0; - size_t bitCountMaxVal = 1; - size_t numStates = rs->ctx_aut->statesCount(); - while (bitCountMaxVal <= numStates) - { - bitCount++; - bitCountMaxVal *= 2; - } - - VERB_LN(3, "Bits required for CA: " << bitCount); - return bitCount; + if (!usingContextAutomaton()) { + return 0; + } + + assert(rs->ctx_aut != nullptr); + + size_t bitCount = 0; + size_t bitCountMaxVal = 1; + size_t numStates = rs->ctx_aut->statesCount(); + + while (bitCountMaxVal <= numStates) { + bitCount++; + bitCountMaxVal *= 2; + } + + VERB_LN(3, "Bits required for CA: " << bitCount); + return bitCount; } BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const -{ - // select appropriate BDD vector - vector *enc_vec; - if (succ) - enc_vec = pv_ca_succ; - else - enc_vec = pv_ca; +{ + // select appropriate BDD vector + vector *enc_vec; - assert(enc_vec != nullptr); - - BDD r = BDD_TRUE; - State val = state_id; + if (succ) { + enc_vec = pv_ca_succ; + } + else { + enc_vec = pv_ca; + } - for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) - { - if (val != 0) - { - if (val % 2 == 1) - { - r *= (*enc_vec)[i]; - } - else - { - r *= !(*enc_vec)[i]; - } - val /= 2; - } - else - r *= !(*enc_vec)[i]; - } + assert(enc_vec != nullptr); - return r; + BDD r = BDD_TRUE; + State val = state_id; + + for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) { + if (val != 0) { + if (val % 2 == 1) { + r *= (*enc_vec)[i]; + } + else { + r *= !(*enc_vec)[i]; + } + + val /= 2; + } + else { + r *= !(*enc_vec)[i]; + } + } + + return r; } BDD SymRS::getEncCtxAutInitState(void) { - VERB_LN(2, "Encoding context automaton's initial state"); - - State state = rs->ctx_aut->getInitState(); + VERB_LN(2, "Encoding context automaton's initial state"); - return encCtxAutState(state); + State state = rs->ctx_aut->getInitState(); + + return encCtxAutState(state); } void SymRS::encodeCtxAutTrans(void) { - VERB_LN(2, "Encoding context automaton's transition relation"); + VERB_LN(2, "Encoding context automaton's transition relation"); - if (tr_ca != nullptr) - { - VERB_LN(1, "Encoding for context automaton already present, not replacing") - return; - } - - tr_ca = new BDD(BDD_FALSE); + if (tr_ca != nullptr) { + VERB_LN(1, "Encoding for context automaton already present, not replacing") + return; + } - for (auto &t : rs->ctx_aut->transitions) - { - VERB_LN(2, "Encoding CA transition " << rs->ctx_aut->getStateName(t.src_state) - << " -> " << rs->ctx_aut->getStateName(t.dst_state)); - BDD enc_src = encCtxAutState(t.src_state); - BDD enc_dst = encCtxAutStateSucc(t.dst_state); - BDD enc_ctx = compContext(encActEntitiesConj(t.ctx)); - - *tr_ca += enc_src * enc_ctx * enc_dst; - } + tr_ca = new BDD(BDD_FALSE); + + for (auto &t : rs->ctx_aut->transitions) { + VERB_LN(2, "Encoding CA transition " << rs->ctx_aut->getStateName(t.src_state) + << " -> " << rs->ctx_aut->getStateName(t.dst_state)); + BDD enc_src = encCtxAutState(t.src_state); + BDD enc_dst = encCtxAutStateSucc(t.dst_state); + BDD enc_ctx = compContext(encActEntitiesConj(t.ctx)); + + *tr_ca += enc_src * enc_ctx * enc_dst; + } } /** EOF **/ diff --git a/symrs.hh b/symrs.hh index 376c559..060b819 100644 --- a/symrs.hh +++ b/symrs.hh @@ -36,11 +36,11 @@ class SymRS Cudd *cuddMgr; Options *opts; - // Mapping: entity ID -> action/context entity ID + // Mapping: entity ID -> action/context entity ID StateEntityToAction stateToAct; BDD *initStates; - + vector *pv; vector *pv_succ; BDD *pv_E; @@ -55,12 +55,12 @@ class SymRS BDD *monoTrans; - // Context automaton - vector *pv_ca; - vector *pv_ca_succ; - BDD *pv_ca_E; - BDD *pv_ca_succ_E; - BDD *tr_ca; + // Context automaton + vector *pv_ca; + vector *pv_ca_succ; + BDD *pv_ca_E; + BDD *pv_ca_succ_E; + BDD *tr_ca; vector *pv_act; BDD *pv_act_E; @@ -69,37 +69,44 @@ class SymRS unsigned int totalReactions; unsigned int totalRctSysStateVars; unsigned int totalActions; - unsigned int totalCtxAutStateVars; - + unsigned int totalCtxAutStateVars; + BDD encEntity_raw(Entity entity, bool succ) const; - BDD encEntity(Entity entity) const { - return encEntity_raw(entity, false); + BDD encEntity(Entity entity) const + { + return encEntity_raw(entity, false); } - BDD encActEntity(Entity entity) const { - assert(entity < pv_act->size()); - return (*pv_act)[entity]; + BDD encActEntity(Entity entity) const + { + assert(entity < pv_act->size()); + return (*pv_act)[entity]; } - BDD encEntitySucc(Entity entity) const { - return encEntity_raw(entity, true); + BDD encEntitySucc(Entity entity) const + { + return encEntity_raw(entity, true); } BDD encEntitiesConj_raw(const Entities &entities, bool succ); - BDD encEntitiesConj(const Entities &entities) { - return encEntitiesConj_raw(entities, false); + BDD encEntitiesConj(const Entities &entities) + { + return encEntitiesConj_raw(entities, false); } - BDD encEntitiesConjSucc(const Entities &entities) { - return encEntitiesConj_raw(entities, true); + BDD encEntitiesConjSucc(const Entities &entities) + { + return encEntitiesConj_raw(entities, true); } BDD encEntitiesDisj_raw(const Entities &entities, bool succ); - BDD encEntitiesDisj(const Entities &entities) { - return encEntitiesDisj_raw(entities, false); + BDD encEntitiesDisj(const Entities &entities) + { + return encEntitiesDisj_raw(entities, false); } - BDD encEntitiesDisjSucc(const Entities &entities) { - return encEntitiesDisj_raw(entities, true); + BDD encEntitiesDisjSucc(const Entities &entities) + { + return encEntitiesDisj_raw(entities, true); } BDD encStateActEntitiesConj(const Entities &entities); BDD encStateActEntitiesDisj(const Entities &entities); - BDD encActEntitiesConj(const Entities &entities); + BDD encActEntitiesConj(const Entities &entities); /** * @brief Complements an encoding of a given state by negating all the variables that are not set to true @@ -113,122 +120,186 @@ class SymRS std::string decodedRctSysStateToStr(const BDD &state); void printDecodedRctSysStates(const BDD &states); - BDD encNoContext(void); + BDD encNoContext(void); void initBDDvars(void); void encodeTransitions(void); void encodeTransitions_old(void); void encodeInitStates(void); - void encodeInitStatesForCtxAut(void); - void encodeInitStatesNoCtxAut(void); + void encodeInitStatesForCtxAut(void); + void encodeInitStatesNoCtxAut(void); void mapStateToAct(void); void encode(void); - int getMappedStateToActID(int stateID) const - { - assert(stateID < static_cast(totalRctSysStateVars)); - return stateToAct[stateID]; - } - - size_t getCtxAutStateEncodingSize(void); - -public: - SymRS(RctSys *rs, Options *opts); - - vector *getEncPV(void) { return pv; } - vector *getEncPVsucc(void) { return pv_succ; } - BDD *getEncPV_E(void) { return pv_E; } - BDD *getEncPVsucc_E(void) { return pv_succ_E; } - BDD *getEncPVact_E(void) { return pv_act_E; } - vector *getEncPartTrans(void) { return partTrans; } - BDD *getEncMonoTrans(void) { return monoTrans; } - BDD getEncState(const Entities &entities); - BDD *getEncInitStates(void) { return initStates; } - Cudd *getCuddMgr(void) { return cuddMgr; } - unsigned int getTotalStateVars(void) { return totalStateVars; } - unsigned int getTotalRctSysStateVars(void) { return totalRctSysStateVars; } - BDD encEntity(std::string name) const { - return encEntity(rs->getEntityID(name)); + int getMappedStateToActID(int stateID) const + { + assert(stateID < static_cast(totalRctSysStateVars)); + return stateToAct[stateID]; } - + + size_t getCtxAutStateEncodingSize(void); + + public: + SymRS(RctSys *rs, Options *opts); + + vector *getEncPV(void) + { + return pv; + } + vector *getEncPVsucc(void) + { + return pv_succ; + } + BDD *getEncPV_E(void) + { + return pv_E; + } + BDD *getEncPVsucc_E(void) + { + return pv_succ_E; + } + BDD *getEncPVact_E(void) + { + return pv_act_E; + } + vector *getEncPartTrans(void) + { + return partTrans; + } + BDD *getEncMonoTrans(void) + { + return monoTrans; + } + BDD getEncState(const Entities &entities); + BDD *getEncInitStates(void) + { + return initStates; + } + Cudd *getCuddMgr(void) + { + return cuddMgr; + } + unsigned int getTotalStateVars(void) + { + return totalStateVars; + } + unsigned int getTotalRctSysStateVars(void) + { + return totalRctSysStateVars; + } + BDD encEntity(std::string name) const + { + return encEntity(rs->getEntityID(name)); + } + BDD encActStrEntity(std::string name) const; - BDD getBDDtrue(void) const { return BDD_TRUE; } - BDD getBDDfalse(void) const { return BDD_FALSE; } - + BDD getBDDtrue(void) const + { + return BDD_TRUE; + } + BDD getBDDfalse(void) const + { + return BDD_FALSE; + } + /** * @brief Checks if context automaton is used * * @return True if CA is used */ - bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; } - + bool usingContextAutomaton(void) + { + return rs->ctx_aut != nullptr; + } + /** * @brief Encodes a context automaton's state * * @return Returns the encoded state */ - BDD encCtxAutState_raw(State state_id, bool succ) const; + BDD encCtxAutState_raw(State state_id, bool succ) const; - /** + /** * @brief Encodes a context automaton's state (as predecessor/non-primed) * * @return Returns the encoded state */ - BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); } - + BDD encCtxAutState(State state_id) const + { + return encCtxAutState_raw(state_id, false); + } + /** * @brief Encodes a context automaton's state (as successor/primed) * * @return Returns the encoded state */ - BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); } - + BDD encCtxAutStateSucc(State state_id) const + { + return encCtxAutState_raw(state_id, true); + } + /** * @brief Encodes the initial state of context automaton * * @return Returns the encoded state(s) */ - BDD getEncCtxAutInitState(void); - + BDD getEncCtxAutInitState(void); + /** * @brief Getter for context automaton's state variables (predecessor/non-primed) * * @return Returns a vector of BDDs */ - vector *getEncCtxAutPV(void) { return pv_ca; } + vector *getEncCtxAutPV(void) + { + return pv_ca; + } /** * @brief Getter for context automaton's successor (primed) state variables * * @return Returns a vector of BDDs */ - vector *getEncCtxAutPVsucc(void) { return pv_ca_succ; } + vector *getEncCtxAutPVsucc(void) + { + return pv_ca_succ; + } /** * @brief Getter for context automaton's quantification BDD (for non-primed vars) * - * @return Returns a BDD for quantification + * @return Returns a BDD for quantification */ - BDD *getEncCtxAutPV_E(void) { return pv_ca_E; } + BDD *getEncCtxAutPV_E(void) + { + return pv_ca_E; + } /** * @brief Getter for context automaton's quantification BDD (for primed vars) * - * @return Returns a BDD for quantification + * @return Returns a BDD for quantification */ - BDD *getEncCtxAutPVsucc_E(void) { return pv_ca_succ_E; } + BDD *getEncCtxAutPVsucc_E(void) + { + return pv_ca_succ_E; + } /** * @brief Encodes the monolithic transition relation - */ - void encodeCtxAutTrans(void); - + */ + void encodeCtxAutTrans(void); + /** * @brief Getter for context automaton's transition relation * * @return Returns a BDD encoding the transition relation - */ - BDD *getEncCtxAutTrans(void) { return tr_ca; } + */ + BDD *getEncCtxAutTrans(void) + { + return tr_ca; + } }; #endif diff --git a/types.hh b/types.hh index b431fa0..b580b95 100644 --- a/types.hh +++ b/types.hh @@ -17,9 +17,9 @@ typedef unsigned int Entity; typedef std::set Entities; struct Reaction { - Entities rctt; - Entities inhib; - Entities prod; + Entities rctt; + Entities inhib; + Entities prod; }; typedef unsigned int Process; @@ -40,18 +40,18 @@ typedef std::map StatesByName; typedef std::map EntitiesForProc; struct ReactionCond { - Entities rctt; - Entities inhib; + Entities rctt; + Entities inhib; }; typedef std::vector ReactionConds; -typedef std::map DecompReactions; +typedef std::map DecompReactions; typedef std::vector StateEntityToAction; struct CtxAutTransition { - State src_state; - Entities ctx; - State dst_state; + State src_state; + Entities ctx; + State dst_state; }; typedef std::vector CtxAutTransitions;