diff --git a/Makefile b/Makefile index 5a7fa4f..a75b776 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT) #CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g LDLIBS = $(CUDD_INCLUDE) -OBJ = rs.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o +OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o all: main diff --git a/mc.cc b/mc.cc index 850e56f..6a2c7c3 100644 --- a/mc.cc +++ b/mc.cc @@ -117,7 +117,7 @@ void ModelChecker::printReachWithSucc(void) cleanup(); } -bool ModelChecker::checkReach(const RctSys::Entities testState) +bool ModelChecker::checkReach(const Entities testState) { if (opts->measure) opts->ver_time = cpuTime(); diff --git a/mc.hh b/mc.hh index 35f1e7f..e2ddf5f 100644 --- a/mc.hh +++ b/mc.hh @@ -67,7 +67,7 @@ public: void printReach(void); void printReachWithSucc(void); - bool checkReach(const RctSys::Entities testState); + bool checkReach(const Entities testState); bool checkRSCTL(FormRSCTL *form); bool checkRSCTLfull(FormRSCTL *form); bool checkRSCTLbmc(FormRSCTL *form); diff --git a/rs.cc b/rs.cc index d3dde71..0458ca4 100644 --- a/rs.cc +++ b/rs.cc @@ -8,6 +8,11 @@ #include "rs.hh" +RctSys::RctSys(void) +{ + ctx_aut = nullptr; +} + bool RctSys::hasEntity(std::string name) { if (entities_names.find(name) == entities_names.end()) @@ -40,7 +45,7 @@ std::string RctSys::getEntityName(Entity entityID) } } -RctSys::Entity RctSys::getEntityID(std::string name) +Entity RctSys::getEntityID(std::string name) { if (!hasEntity(name)) { @@ -166,52 +171,21 @@ void RctSys::printSystem(void) showInitialStates(); showActionEntities(); showReactions(); -} - -bool CtxAut::hasState(std::string name) -{ - if (states_names.find(name) == states_names.end()) - return false; - else - return true; -} - -CtxAut::State CtxAut::getStateID(std::string name) -{ - if (!hasState(name)) - { - FERROR("No such state: " << name); - } - return states_names[name]; -} - -void CtxAut::addState(std::string name) -{ - if (!hasState(name)) - { - State new_state_id = states_ids.size(); - - VERB_L2("Adding state: " << name << " index=" << new_state_id); - - states_ids.push_back(name); - states_names[name] = new_state_id; - } -} - -void CtxAut::pushContextEntity(RctSys::Entity entity_id) -{ - tmpEntities.insert(entity_id); -} - -void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) -{ - VERB_L3("Saving transition"); - Transition new_transition; - - new_transition.src_state = getStateID(srcStateName); - new_transition.ctx = tmpEntities; - tmpEntities.clear(); - new_transition.dst_state = getStateID(dstStateName); + if (ctx_aut != nullptr) + { + ctx_aut->printAutomaton(); + } } +void RctSys::ctxAutEnable(void) +{ + assert(ctx_aut == nullptr); + ctx_aut = new CtxAut; +} + +void RctSys::ctxAutAddState(std::string stateName) +{ + assert(ctx_aut != nullptr); + +} diff --git a/rs.hh b/rs.hh index 97fc22b..2474811 100644 --- a/rs.hh +++ b/rs.hh @@ -15,6 +15,8 @@ #include #include #include +#include "types.hh" +#include "ctx_aut.hh" #include "macro.hh" #include "options.hh" #include "memtime.hh" @@ -26,38 +28,9 @@ class RctSys { friend class SymRS; friend class SymRSstate; - public: - typedef unsigned int Entity; - typedef std::set Entities; - struct Reaction { - Entities rctt; - Entities inhib; - Entities prod; - }; - typedef std::vector Reactions; - typedef std::vector EntitiesByIds; - typedef std::map EntitiesByName; - typedef std::set EntitiesSets; - private: - Reactions reactions; - EntitiesSets initStates; - - Entities actionEntities; - - EntitiesByIds entities_ids; - EntitiesByName entities_names; - - Entities tmpReactants; - Entities tmpInhibitors; - Entities tmpProducts; - - Entities tmpState; - - Entity getEntityID(std::string entityName); - - Options *opts; public: + RctSys(void); void setOptions(Options *opts) { this->opts = opts; @@ -93,40 +66,31 @@ class RctSys void showInitialStates(void); void showActionEntities(void); void printSystem(void); -}; -// Context Automaton -class CtxAut -{ - public: - typedef unsigned int State; - typedef std::vector StatesById; - typedef std::map StatesByName; - struct Transition { - State src_state; - RctSys::Entities ctx; - State dst_state; - }; - - bool hasState(std::string name); - void addState(std::string stateName); - State getStateID(std::string name); - void addTransition(std::string srcStateName, std::string dstStateName); - void pushContextEntity(RctSys::Entity entity_id); - void setOptions(Options *opts) { this->opts = opts; } + void ctxAutEnable(void); + void ctxAutAddState(std::string stateName); private: - Options *opts; - StatesById states_ids; - StatesByName states_names; - RctSys::Entities tmpEntities; -}; + Reactions reactions; + EntitiesSets initStates; + + Entities actionEntities; + + CtxAut *ctx_aut; + + EntitiesByIds entities_ids; + EntitiesByName entities_names; + + Entities tmpReactants; + Entities tmpInhibitors; + Entities tmpProducts; + + Entities tmpState; + + Options *opts; + + Entity getEntityID(std::string entityName); -class RctSysWithCtxAut : public RctSys -{ - // friend class CtxAut; - - CtxAut ctx_aut; }; #endif diff --git a/rsin_driver.cc b/rsin_driver.cc index ac76c39..7366265 100644 --- a/rsin_driver.cc +++ b/rsin_driver.cc @@ -16,8 +16,8 @@ rsin_driver::rsin_driver(RctSys *rs) void rsin_driver::initialise(void) { - this->rs = nullptr; - this->rsctlform = nullptr; + rs = nullptr; + rsctlform = nullptr; opts = nullptr; use_ctx_aut = false; use_concentrations = false; @@ -79,14 +79,11 @@ void rsin_driver::ensureReactionSystemReady(void) void rsin_driver::setupReactionSystem(void) { assert(rs == nullptr); - if (use_ctx_aut) - { - rs = new RctSysWithCtxAut; - } - else - { - rs = new RctSys; - } + rs = new RctSys; + + if (use_ctx_aut) VERB("Using RS with CA") + else VERB("Using ordinary RS") + rs->setOptions(opts); } @@ -96,3 +93,4 @@ RctSys *rsin_driver::getReactionSystem(void) assert(rs != nullptr); return rs; } + diff --git a/rsin_driver.hh b/rsin_driver.hh index 7d8eec5..630755d 100644 --- a/rsin_driver.hh +++ b/rsin_driver.hh @@ -25,13 +25,10 @@ public: virtual ~rsin_driver(); //std::map variables; - RctSys *rs; FormRSCTL *rsctlform; Options *opts; - // - // options in configuration file - // + // options in configuration file: bool use_ctx_aut; bool use_concentrations; @@ -49,19 +46,22 @@ public: FormRSCTL *getFormRSCTL(void); void ensureOptionsAllowed(void); - void useContextAutomaton(void) { ensureOptionsAllowed(); use_ctx_aut = true; }; + void useContextAutomaton(void) { ensureOptionsAllowed(); use_ctx_aut = true; getReactionSystem()->ctxAutEnable(); }; 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: + RctSys *rs; + void initialise(void); }; diff --git a/rsin_parser.yy b/rsin_parser.yy index 6fa3950..cd7fca8 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -91,7 +91,12 @@ options: ; option: - | USE_CTX_AUT { } + | USE_CTX_AUT { + driver.useContextAutomaton(); + } + | USE_CONCENTRATIONS { + driver.useConcentrations(); + } ; /* @@ -190,6 +195,8 @@ ctxaut: ; autstate: IDENTIFIER { + driver.getReactionSystem()->ctxAutAddState(*$1); + free($1); } ; diff --git a/symrs.cc b/symrs.cc index 4af9b45..7fac236 100644 --- a/symrs.cc +++ b/symrs.cc @@ -8,7 +8,7 @@ #include "symrs.hh" -BDD SymRS::encEntity_raw(RctSys::Entity entity, bool succ) const +BDD SymRS::encEntity_raw(Entity entity, bool succ) const { BDD r; @@ -20,7 +20,7 @@ BDD SymRS::encEntity_raw(RctSys::Entity entity, bool succ) const return r; } -BDD SymRS::encEntitiesConj_raw(const RctSys::Entities &entities, bool succ) +BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ) { BDD r = BDD_TRUE; @@ -33,7 +33,7 @@ BDD SymRS::encEntitiesConj_raw(const RctSys::Entities &entities, bool succ) return r; } -BDD SymRS::encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ) +BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ) { BDD r = BDD_FALSE; @@ -46,7 +46,7 @@ BDD SymRS::encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ) return r; } -BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities) +BDD SymRS::encStateActEntitiesConj(const Entities &entities) { BDD r = BDD_TRUE; @@ -62,7 +62,7 @@ BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities) return r; } -BDD SymRS::encStateActEntitiesDisj(const RctSys::Entities &entities) +BDD SymRS::encStateActEntitiesDisj(const Entities &entities) { BDD r = BDD_FALSE; @@ -182,7 +182,7 @@ void SymRS::encodeTransitions(void) cond.rctt = rs->reactions[i].rctt; cond.inhib = rs->reactions[i].inhib; - for (RctSys::Entities::iterator p = rs->reactions[i].prod.begin(); + for (Entities::iterator p = rs->reactions[i].prod.begin(); p != rs->reactions[i].prod.end(); ++p) { dr[*p].push_back(cond); @@ -289,7 +289,7 @@ void SymRS::encodeTransitions(void) VERB("Reactions ready"); } -BDD SymRS::getEncState(const RctSys::Entities &entities) +BDD SymRS::getEncState(const Entities &entities) { assert(0); //BDD state = compState(encEntitiesConj(rs->initState)); diff --git a/symrs.hh b/symrs.hh index f20dc76..3898896 100644 --- a/symrs.hh +++ b/symrs.hh @@ -14,6 +14,7 @@ #include #include #include "cudd.hh" +#include "types.hh" #include "macro.hh" #include "bdd_macro.hh" #include "rs.hh" @@ -36,11 +37,11 @@ class SymRS Options *opts; struct ReactionCond { - RctSys::Entities rctt; - RctSys::Entities inhib; + Entities rctt; + Entities inhib; }; typedef vector ReactionConds; - typedef map DecompReactions; + typedef map DecompReactions; typedef std::vector StateEntityToAction; StateEntityToAction stateToAct; @@ -62,33 +63,33 @@ class SymRS unsigned int totalStateVars; unsigned int totalActions; - BDD encEntity_raw(RctSys::Entity entity, bool succ) const; - BDD encEntity(RctSys::Entity entity) const { + BDD encEntity_raw(Entity entity, bool succ) const; + BDD encEntity(Entity entity) const { return encEntity_raw(entity, false); } - BDD encActEntity(RctSys::Entity entity) const { + BDD encActEntity(Entity entity) const { assert(entity < pv_act->size()); return (*pv_act)[entity]; } - BDD encEntitySucc(RctSys::Entity entity) const { + BDD encEntitySucc(Entity entity) const { return encEntity_raw(entity, true); } - BDD encEntitiesConj_raw(const RctSys::Entities &entities, bool succ); - BDD encEntitiesConj(const RctSys::Entities &entities) { + BDD encEntitiesConj_raw(const Entities &entities, bool succ); + BDD encEntitiesConj(const Entities &entities) { return encEntitiesConj_raw(entities, false); } - BDD encEntitiesConjSucc(const RctSys::Entities &entities) { + BDD encEntitiesConjSucc(const Entities &entities) { return encEntitiesConj_raw(entities, true); } - BDD encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ); - BDD encEntitiesDisj(const RctSys::Entities &entities) { + BDD encEntitiesDisj_raw(const Entities &entities, bool succ); + BDD encEntitiesDisj(const Entities &entities) { return encEntitiesDisj_raw(entities, false); } - BDD encEntitiesDisjSucc(const RctSys::Entities &entities) { + BDD encEntitiesDisjSucc(const Entities &entities) { return encEntitiesDisj_raw(entities, true); } - BDD encStateActEntitiesConj(const RctSys::Entities &entities); - BDD encStateActEntitiesDisj(const RctSys::Entities &entities); + BDD encStateActEntitiesConj(const Entities &entities); + BDD encStateActEntitiesDisj(const Entities &entities); /** * @brief Complements an encoding of a given state by negating all the variables that are not set to true @@ -134,7 +135,7 @@ public: BDD *getEncPVact_E(void) { return pv_act_E; } vector *getEncPartTrans(void) { return partTrans; } BDD *getEncMonoTrans(void) { return monoTrans; } - BDD getEncState(const RctSys::Entities &entities); + BDD getEncState(const Entities &entities); BDD *getEncInitStates(void) { return initStates; } Cudd *getCuddMgr(void) { return cuddMgr; } unsigned int getTotalStateVars(void) { return totalStateVars; }