diff --git a/ctx_aut.cc b/ctx_aut.cc index 57ad359..a77e21c 100644 --- a/ctx_aut.cc +++ b/ctx_aut.cc @@ -102,7 +102,7 @@ void CtxAut::showTransitions(void) { 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 64228f2..a2e2f6f 100644 --- a/ctx_aut.hh +++ b/ctx_aut.hh @@ -27,6 +27,8 @@ class RctSys; class CtxAut { + friend class SymRS; + public: CtxAut(Options *opts, RctSys *parent_rctsys); bool hasState(std::string name); diff --git a/macro.hh b/macro.hh index 4a78a70..dc44207 100644 --- a/macro.hh +++ b/macro.hh @@ -33,4 +33,10 @@ if (opts->verbose > 2) { \ 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; \ +} + #endif diff --git a/symrs.cc b/symrs.cc index 98313f4..6a9f502 100644 --- a/symrs.cc +++ b/symrs.cc @@ -5,6 +5,25 @@ #include "symrs.hh" + +SymRS::SymRS(RctSys *rs, Options *opts) +{ + this->rs = rs; + this->opts = opts; + totalStateVars = rs->getEntitiesSize(); + totalReactions = rs->getReactionsSize(); + totalActions = rs->getActionsSize(); + totalCtxAutStateVars = getCtxAutStateEncodingSize(); + + partTrans = nullptr; + monoTrans = nullptr; + + pv_ca = nullptr; + pv_ca_succ = nullptr; + + encode(); +} + BDD SymRS::encEntity_raw(Entity entity, bool succ) const { BDD r; @@ -21,10 +40,10 @@ BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ) { BDD r = BDD_TRUE; - for (auto entity = entities.begin(); entity != entities.end(); ++entity) + for (const auto &entity : entities) { - if (succ) r *= encEntitySucc(*entity); - else r *= encEntity(*entity); + if (succ) r *= encEntitySucc(entity); + else r *= encEntity(entity); } return r; @@ -34,10 +53,10 @@ BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ) { BDD r = BDD_FALSE; - for (auto entity = entities.begin(); entity != entities.end(); ++entity) + for (const auto &entity : entities) { - if (succ) r += encEntitySucc(*entity); - else r += encEntity(*entity); + if (succ) r += encEntitySucc(entity); + else r += encEntity(entity); } return r; @@ -47,13 +66,13 @@ BDD SymRS::encStateActEntitiesConj(const Entities &entities) { BDD r = BDD_TRUE; - for (auto entity = entities.begin(); entity != entities.end(); ++entity) + for (const auto &entity : entities) { - BDD state_act = encEntity(*entity); + 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) + if ((actEntity = getMappedStateToActID(entity)) >= 0) state_act += encActEntity(actEntity); r *= state_act; @@ -66,13 +85,13 @@ BDD SymRS::encStateActEntitiesDisj(const Entities &entities) { BDD r = BDD_FALSE; - for (auto entity = entities.begin(); entity != entities.end(); ++entity) + for (const auto &entity : entities) { - BDD state_act = encEntity(*entity); + 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) + if ((actEntity = getMappedStateToActID(entity)) >= 0) state_act += encActEntity(actEntity); r += state_act; @@ -81,6 +100,19 @@ BDD SymRS::encStateActEntitiesDisj(const Entities &entities) return r; } +BDD SymRS::encActEntitiesConj(const Entities &entities) +{ + BDD r = BDD_TRUE; + + for (const auto &entity : entities) + { + Entity actEntity = getMappedStateToActID(entity); + r *= encActEntity(actEntity); + } + + return r; +} + BDD SymRS::compState(const BDD &state) const { BDD s = state; @@ -413,7 +445,7 @@ size_t SymRS::getCtxAutStateEncodingSize(void) } BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const -{ +{ // select appropriate BDD vector vector *enc_vec; if (succ) @@ -421,7 +453,9 @@ BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const else enc_vec = pv_ca; - BDD r; + assert(enc_vec != nullptr); + + BDD r = BDD_TRUE; State val = state_id; for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) @@ -429,9 +463,13 @@ BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const if (val != 0) { if (val % 2 == 1) - r *= (*enc_vec)[i]; + { + r *= (*enc_vec)[i]; + } else - r *= !(*enc_vec)[i]; + { + r *= !(*enc_vec)[i]; + } val /= 2; } else @@ -443,22 +481,31 @@ BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const BDD *SymRS::getEncCtxAutInitState(void) { - return new BDD(BDD_TRUE); -} - -vector *SymRS::getEncCtxAutPV(void) -{ - return new vector(); -} - -vector *SymRS::getEncCtxAutPVsucc(void) -{ - return new vector(); + VERB_LN(2, "Encoding context automaton's initial state"); + + State state = rs->ctx_aut->getInitState(); + + BDD *r = new BDD(encCtxAutState(state)); + + return r; } BDD *SymRS::getEncCtxAutTrans(void) { - return new BDD(BDD_TRUE); + VERB_LN(2, "Encoding context automaton's transition relation"); + + BDD *r = new BDD(BDD_FALSE); + + for (auto &t : rs->ctx_aut->transitions) + { + BDD enc_src = encCtxAutState(t.src_state); + BDD enc_dst = encCtxAutStateSucc(t.dst_state); + BDD enc_ctx = encActEntitiesConj(t.ctx); + + *r += enc_src * enc_ctx * enc_dst; + } + + return r; } /** EOF **/ diff --git a/symrs.hh b/symrs.hh index 9f65b4c..a7e6e57 100644 --- a/symrs.hh +++ b/symrs.hh @@ -94,6 +94,8 @@ class SymRS BDD encStateActEntitiesConj(const Entities &entities); BDD encStateActEntitiesDisj(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 * @@ -120,20 +122,8 @@ class SymRS size_t getCtxAutStateEncodingSize(void); public: - SymRS(RctSys *rs, Options *opts) - { - this->rs = rs; - this->opts = opts; - totalStateVars = rs->getEntitiesSize(); - totalReactions = rs->getReactionsSize(); - totalActions = rs->getActionsSize(); - totalCtxAutStateVars = getCtxAutStateEncodingSize(); - - partTrans = nullptr; - monoTrans = nullptr; - - encode(); - } + SymRS(RctSys *rs, Options *opts); + vector *getEncPV(void) { return pv; } vector *getEncPVsucc(void) { return pv_succ; } BDD *getEncPV_E(void) { return pv_E; } @@ -193,14 +183,14 @@ public: * * @return Returns a vector of BDDs */ - vector *getEncCtxAutPV(void); + 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); + vector *getEncCtxAutPVsucc(void) { return pv_ca_succ; } /** * @brief Encodes the monolithic transition relation