diff --git a/formrsctl.cc b/formrsctl.cc index 002f100..7ca391e 100644 --- a/formrsctl.cc +++ b/formrsctl.cc @@ -48,7 +48,7 @@ BDD BoolContexts::getBDD(const SymRS *srs) const { if (oper == BCTX_PV) { - return srs->encActStrAtom(name); + return srs->encActStrEntity(name); } else if (oper == BCTX_TF) { @@ -195,20 +195,20 @@ bool FormRSCTL::hasOper(Oper op) const } } -void FormRSCTL::encodeAtoms(const SymRS *srs) +void FormRSCTL::encodeEntities(const SymRS *srs) { if (RSCTL_COND_1ARG(oper)) { - arg[0]->encodeAtoms(srs); + arg[0]->encodeEntities(srs); } else if (RSCTL_COND_2ARG(oper)) { - arg[0]->encodeAtoms(srs); - arg[1]->encodeAtoms(srs); + arg[0]->encodeEntities(srs); + arg[1]->encodeEntities(srs); } else if (oper == RSCTL_PV) { - bdd = new BDD(srs->encAtom(name)); + bdd = new BDD(srs->encEntity(name)); } } @@ -296,7 +296,7 @@ void FormRSCTL::encodeActions(const SymRS *srs) BDD single_action = srs->getBDDtrue(); for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) { - single_action *= srs->encActStrAtom(*ent); + single_action *= srs->encActStrEntity(*ent); } single_action = srs->compContext(single_action); *actions_bdd += single_action; diff --git a/formrsctl.hh b/formrsctl.hh index 236a924..fbbd92d 100644 --- a/formrsctl.hh +++ b/formrsctl.hh @@ -321,7 +321,7 @@ public: assert(oper == RSCTL_TF); return tf; } - void encodeAtoms(const SymRS *srs); + void encodeEntities(const SymRS *srs); void encodeActions(const SymRS *srs); void forgetActionsBDD(void) { if (actions_bdd != NULL) delete actions_bdd; diff --git a/mc.cc b/mc.cc index 5505f2a..e3670a3 100644 --- a/mc.cc +++ b/mc.cc @@ -117,7 +117,7 @@ void ModelChecker::printReachWithSucc(void) cleanup(); } -bool ModelChecker::checkReach(const RctSys::Atoms testState) +bool ModelChecker::checkReach(const RctSys::Entities testState) { if (opts->measure) opts->ver_time = cpuTime(); @@ -370,9 +370,9 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form) VERB("Model checking for RSCTL formula: " << form->toStr()); - VERB("Processing the formula: encoding atoms"); - form->encodeAtoms(srs); - VERB("Atoms encoded"); + VERB("Processing the formula: encoding entities"); + form->encodeEntities(srs); + VERB("Entities encoded"); VERB("Processing the formula: encoding actions/contexts"); form->encodeActions(srs); @@ -448,9 +448,9 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form) VERB("Bounded model checking for RSCTL formula: " << form->toStr()); - VERB("Processing the formula: encoding atoms"); - form->encodeAtoms(srs); - VERB("Atoms encoded"); + VERB("Processing the formula: encoding entities"); + form->encodeEntities(srs); + VERB("Entities encoded"); VERB("Processing the formula: encoding actions/contexts"); form->encodeActions(srs); diff --git a/mc.hh b/mc.hh index 7707b1d..20ff756 100644 --- a/mc.hh +++ b/mc.hh @@ -67,7 +67,7 @@ public: void printReach(void); void printReachWithSucc(void); - bool checkReach(const RctSys::Atoms testState); + bool checkReach(const RctSys::Entities testState); bool checkRSCTL(FormRSCTL *form); bool checkRSCTLfull(FormRSCTL *form); bool checkRSCTLbmc(FormRSCTL *form); diff --git a/rs.cc b/rs.cc index 970df3e..4bf94f2 100644 --- a/rs.cc +++ b/rs.cc @@ -8,64 +8,64 @@ #include "rs.hh" -bool RctSys::hasAtom(std::string name) +bool RctSys::hasEntity(std::string name) { - if (atoms_names.find(name) == atoms_names.end()) + if (entities_names.find(name) == entities_names.end()) return false; else return true; } -void RctSys::addAtom(std::string name) +void RctSys::addEntity(std::string name) { - if (!hasAtom(name)) + if (!hasEntity(name)) { - Atom new_atom_id = atoms_ids.size(); + Entity new_entity_id = entities_ids.size(); - VERB_L2("Adding atom: " << name << " index=" << new_atom_id); + VERB_L2("Adding entity: " << name << " index=" << new_entity_id); - atoms_ids.push_back(name); - atoms_names[name] = new_atom_id; + entities_ids.push_back(name); + entities_names[name] = new_entity_id; } } -std::string RctSys::getAtomName(Atom atomID) +std::string RctSys::getEntityName(Entity entityID) { - if (atomID < atoms_ids.size()) - return atoms_ids[atomID]; + if (entityID < entities_ids.size()) + return entities_ids[entityID]; else { - FERROR("No such atom ID: " << atomID); + FERROR("No such entity ID: " << entityID); return "??"; } } -RctSys::Atom RctSys::getAtomID(std::string name) +RctSys::Entity RctSys::getEntityID(std::string name) { - if (!hasAtom(name)) + if (!hasEntity(name)) { - FERROR("No such atom: " << name); + FERROR("No such entity: " << name); } - return atoms_names[name]; + return entities_names[name]; } -void RctSys::pushReactant(std::string atomName) +void RctSys::pushReactant(std::string entityName) { - if (!hasAtom(atomName)) - addAtom(atomName); - tmpReactants.insert(getAtomID(atomName)); + if (!hasEntity(entityName)) + addEntity(entityName); + tmpReactants.insert(getEntityID(entityName)); } -void RctSys::pushInhibitor(std::string atomName) +void RctSys::pushInhibitor(std::string entityName) { - if (!hasAtom(atomName)) - addAtom(atomName); - tmpInhibitors.insert(getAtomID(atomName)); + if (!hasEntity(entityName)) + addEntity(entityName); + tmpInhibitors.insert(getEntityID(entityName)); } -void RctSys::pushProduct(std::string atomName) +void RctSys::pushProduct(std::string entityName) { - if (!hasAtom(atomName)) - addAtom(atomName); - tmpProducts.insert(getAtomID(atomName)); + if (!hasEntity(entityName)) + addEntity(entityName); + tmpProducts.insert(getEntityID(entityName)); } void RctSys::commitReaction(void) @@ -85,12 +85,12 @@ void RctSys::commitReaction(void) tmpProducts.clear(); } -std::string RctSys::atomsToStr(const Atoms &atoms) +std::string RctSys::entitiesToStr(const Entities &entities) { std::string s = " "; - for (auto a = atoms.begin(); a != atoms.end(); ++a) + for (auto a = entities.begin(); a != entities.end(); ++a) { - s += atomToStr(*a) + " "; + s += entityToStr(*a) + " "; } return s; } @@ -100,19 +100,19 @@ void RctSys::showReactions(void) cout << "# Reactions:" << endl; for (auto r = reactions.begin(); r != reactions.end(); ++r) { - cout << " * (R={" << atomsToStr(r->rctt) << "}," - << "I={" << atomsToStr(r->inhib) << "}," - << "P={" << atomsToStr(r->prod) << "})" << endl; + cout << " * (R={" << entitiesToStr(r->rctt) << "}," + << "I={" << entitiesToStr(r->inhib) << "}," + << "P={" << entitiesToStr(r->prod) << "})" << endl; } } -void RctSys::pushStateAtom(std::string atomName) +void RctSys::pushStateEntity(std::string entityName) { - if (!hasAtom(atomName)) + if (!hasEntity(entityName)) { - FERROR("No such entity: " << atomName); + FERROR("No such entity: " << entityName); } - tmpState.insert(getAtomID(atomName)); + tmpState.insert(getEntityID(entityName)); } void RctSys::commitInitState(void) @@ -122,27 +122,27 @@ void RctSys::commitInitState(void) } -void RctSys::addActionAtom(std::string atomName) +void RctSys::addActionEntity(std::string entityName) { - if (!hasAtom(atomName)) - addAtom(atomName); - actionAtoms.insert(getAtomID(atomName)); + if (!hasEntity(entityName)) + addEntity(entityName); + actionEntities.insert(getEntityID(entityName)); } -bool RctSys::isActionAtom(Atom atom) +bool RctSys::isActionEntity(Entity entity) { - if (actionAtoms.count(atom) > 0) + if (actionEntities.count(entity) > 0) return true; else return false; } -void RctSys::showActionAtoms(void) +void RctSys::showActionEntities(void) { cout << "# Context entities:"; - for (auto a = actionAtoms.begin(); a != actionAtoms.end(); ++a) + for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a) { - cout << " " << getAtomName(*a); + cout << " " << getEntityName(*a); } cout << endl; } @@ -155,7 +155,7 @@ void RctSys::showInitialStates(void) cout << " *"; for (auto a = s->begin(); a != s->end(); ++a) { - cout << " " << getAtomName(*a); + cout << " " << getEntityName(*a); } cout << endl; } @@ -164,7 +164,7 @@ void RctSys::showInitialStates(void) void RctSys::printSystem(void) { showInitialStates(); - showActionAtoms(); + showActionEntities(); showReactions(); } diff --git a/rs.hh b/rs.hh index eee2aa8..f7aaf69 100644 --- a/rs.hh +++ b/rs.hh @@ -26,34 +26,35 @@ class RctSys { friend class SymRS; friend class SymRSstate; + friend class CtxAut; public: - typedef unsigned int Atom; - typedef std::set Atoms; + typedef unsigned int Entity; + typedef std::set Entities; struct Reaction { - Atoms rctt; - Atoms inhib; - Atoms prod; + Entities rctt; + Entities inhib; + Entities prod; }; typedef std::vector Reactions; - typedef std::vector AtomsByIds; - typedef std::map AtomsByName; - typedef std::set AtomsSets; + typedef std::vector EntitiesByIds; + typedef std::map EntitiesByName; + typedef std::set EntitiesSets; private: Reactions reactions; - AtomsSets initStates; + EntitiesSets initStates; - Atoms actionAtoms; + Entities actionEntities; - AtomsByIds atoms_ids; - AtomsByName atoms_names; + EntitiesByIds entities_ids; + EntitiesByName entities_names; - Atoms tmpReactants; - Atoms tmpInhibitors; - Atoms tmpProducts; + Entities tmpReactants; + Entities tmpInhibitors; + Entities tmpProducts; - Atoms tmpState; + Entities tmpState; - Atom getAtomID(std::string atomName); + Entity getEntityID(std::string entityName); Options *opts; @@ -62,38 +63,50 @@ public: { this->opts = opts; } - bool hasAtom(std::string atomName); - void addAtom(std::string atomName); - std::string getAtomName(Atom atomID); - void pushReactant(std::string atomName); - void pushInhibitor(std::string atomName); - void pushProduct(std::string atomName); + bool hasEntity(std::string entityName); + void addEntity(std::string entityName); + std::string getEntityName(Entity entityID); + void pushReactant(std::string entityName); + void pushInhibitor(std::string entityName); + void pushProduct(std::string entityName); void commitReaction(void); - std::string atomToStr(const Atom atom) { - return atoms_ids[atom]; + std::string entityToStr(const Entity entity) { + return entities_ids[entity]; } - std::string atomsToStr(const Atoms &atoms); + std::string entitiesToStr(const Entities &entities); void showReactions(void); - void pushStateAtom(std::string atomName); + void pushStateEntity(std::string entityName); void commitInitState(void); - void addActionAtom(std::string atomName); - bool isActionAtom(Atom atom); + void addActionEntity(std::string entityName); + bool isActionEntity(Entity entity); void resetInitStates(void) { initStates.clear(); } - unsigned int getAtomsSize(void) { - return atoms_ids.size(); + unsigned int getEntitiesSize(void) { + return entities_ids.size(); } unsigned int getReactionsSize(void) { return reactions.size(); } unsigned int getActionsSize(void) { - return actionAtoms.size(); + return actionEntities.size(); } void showInitialStates(void); - void showActionAtoms(void); + void showActionEntities(void); void printSystem(void); }; +// Context Automaton +class CtxAut +{ + typedef unsigned int State; + typedef std::set States; + struct Transition { + State src_state; + State dst_state; + }; +}; + + #endif diff --git a/rsin_parser.yy b/rsin_parser.yy index 0d2e63c..da0e527 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -76,7 +76,7 @@ class rsin_driver; system: | REACTIONS LCB reactions RCB system | INITIALCONTEXTS LCB initstates RCB system - | CONTEXTENTITIES LCB actionatoms RCB system + | CONTEXTENTITIES LCB actionentities RCB system | RSCTLFORM LCB rsctl_form RCB system { driver.addFormRSCTL($3); } @@ -140,23 +140,23 @@ initstates: ; initstate: - | atom - | initstate COMMA atom + | entity + | initstate COMMA entity ; -atom: IDENTIFIER { - driver.rs->pushStateAtom(*$1); +entity: IDENTIFIER { + driver.rs->pushStateEntity(*$1); free($1); } ; -actionatoms: - | actatom - | actionatoms COMMA actatom +actionentities: + | actentity + | actionentities COMMA actentity ; -actatom: IDENTIFIER { - driver.rs->addActionAtom(*$1); +actentity: IDENTIFIER { + driver.rs->addActionEntity(*$1); free($1); } ; diff --git a/symrs.cc b/symrs.cc index 7401ef5..e2eca69 100644 --- a/symrs.cc +++ b/symrs.cc @@ -8,70 +8,70 @@ #include "symrs.hh" -BDD SymRS::encAtom_raw(RctSys::Atom atom, bool succ) const +BDD SymRS::encEntity_raw(RctSys::Entity entity, bool succ) const { BDD r; if (succ) - r = (*pv_succ)[atom]; + r = (*pv_succ)[entity]; else - r = (*pv)[atom]; + r = (*pv)[entity]; return r; } -BDD SymRS::encAtomsConj_raw(const RctSys::Atoms &atoms, bool succ) +BDD SymRS::encEntitiesConj_raw(const RctSys::Entities &entities, bool succ) { BDD r = BDD_TRUE; - for (auto atom = atoms.begin(); atom != atoms.end(); ++atom) + for (auto entity = entities.begin(); entity != entities.end(); ++entity) { - if (succ) r *= encAtomSucc(*atom); - else r *= encAtom(*atom); + if (succ) r *= encEntitySucc(*entity); + else r *= encEntity(*entity); } return r; } -BDD SymRS::encAtomsDisj_raw(const RctSys::Atoms &atoms, bool succ) +BDD SymRS::encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ) { BDD r = BDD_FALSE; - for (auto atom = atoms.begin(); atom != atoms.end(); ++atom) + for (auto entity = entities.begin(); entity != entities.end(); ++entity) { - if (succ) r += encAtomSucc(*atom); - else r += encAtom(*atom); + if (succ) r += encEntitySucc(*entity); + else r += encEntity(*entity); } return r; } -BDD SymRS::encStateActAtomsConj(const RctSys::Atoms &atoms) +BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities) { BDD r = BDD_TRUE; - for (auto atom = atoms.begin(); atom != atoms.end(); ++atom) + for (auto entity = entities.begin(); entity != entities.end(); ++entity) { - BDD state_act = encAtom(*atom); - int actAtom; - if ((actAtom = getMappedStateToActID(*atom)) >= 0) - state_act += encActAtom(actAtom); + BDD state_act = encEntity(*entity); + int actEntity; + if ((actEntity = getMappedStateToActID(*entity)) >= 0) + state_act += encActEntity(actEntity); r *= state_act; } return r; } -BDD SymRS::encStateActAtomsDisj(const RctSys::Atoms &atoms) +BDD SymRS::encStateActEntitiesDisj(const RctSys::Entities &entities) { BDD r = BDD_FALSE; - for (auto atom = atoms.begin(); atom != atoms.end(); ++atom) + for (auto entity = entities.begin(); entity != entities.end(); ++entity) { - BDD state_act = encAtom(*atom); - int actAtom; - if ((actAtom = getMappedStateToActID(*atom)) >= 0) - state_act += encActAtom(actAtom); + BDD state_act = encEntity(*entity); + int actEntity; + if ((actEntity = getMappedStateToActID(*entity)) >= 0) + state_act += encActEntity(actEntity); r += state_act; } @@ -109,9 +109,9 @@ std::string SymRS::decodedStateToStr(const BDD &state) std::string s = "{ "; for (unsigned int i = 0; i < totalStateVars; ++i) { - if (!(encAtom(i) * state).IsZero()) + if (!(encEntity(i) * state).IsZero()) { - s += rs->atomToStr(i) + " "; + s += rs->entityToStr(i) + " "; } } s += "}"; @@ -137,7 +137,7 @@ void SymRS::initBDDvars(void) { cuddMgr = new Cudd(0,0); - //RctSys::Atoms aa = rs->actionAtoms; + //RctSys::Entities aa = rs->actionEntities; VERB("Preparing BDD variables"); pv = new vector(totalStateVars); @@ -157,7 +157,7 @@ void SymRS::initBDDvars(void) *pv_E *= (*pv)[i]; *pv_succ_E *= (*pv_succ)[i]; - //if (rs->actionAtoms.find(i) == rs->actionAtoms.end()) + //if (rs->actionEntities.find(i) == rs->actionEntities.end()) // (*pv_noact)[j++] = cuddMgr->bddVar(i*2); } @@ -182,7 +182,7 @@ void SymRS::encodeTransitions(void) cond.rctt = rs->reactions[i].rctt; cond.inhib = rs->reactions[i].inhib; - for (RctSys::Atoms::iterator p = rs->reactions[i].prod.begin(); + for (RctSys::Entities::iterator p = rs->reactions[i].prod.begin(); p != rs->reactions[i].prod.end(); ++p) { dr[*p].push_back(cond); @@ -212,10 +212,10 @@ void SymRS::encodeTransitions(void) { // nie ma reakcji produkujacej p: if (opts->part_tr_rel) - (*partTrans)[p] = !encAtomSucc(p); + (*partTrans)[p] = !encEntitySucc(p); else { - *monoTrans *= !encAtomSucc(p); + *monoTrans *= !encEntitySucc(p); } } else @@ -228,17 +228,17 @@ void SymRS::encodeTransitions(void) for (unsigned int j = 0; j < di->second.size(); ++j) { - conditions += encStateActAtomsConj(di->second[j].rctt) * !encStateActAtomsDisj(di->second[j].inhib); + conditions += encStateActEntitiesConj(di->second[j].rctt) * !encStateActEntitiesDisj(di->second[j].inhib); } if (opts->part_tr_rel) { - (*partTrans)[p] = conditions * encAtomSucc(p); - (*partTrans)[p] += !conditions * !encAtomSucc(p); + (*partTrans)[p] = conditions * encEntitySucc(p); + (*partTrans)[p] += !conditions * !encEntitySucc(p); } else { - *monoTrans *= (conditions * encAtomSucc(p)) + (!conditions * !encAtomSucc(p)); + *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc(p)); } } if (opts->reorder_trans) @@ -252,14 +252,14 @@ void SymRS::encodeTransitions(void) /* for (unsigned int p = 0; p < totalStateVars; ++p) // we iterate through products { - RctSys::Atoms::iterator ai = rs->actionAtoms.find(p); + RctSys::Entities::iterator ai = rs->actionEntities.find(p); DecompReactions::iterator di; if ((di = dr.find(p)) == dr.end()) { (*partTrans)[p] = cuddMgr->bddOne(); - if (ai == rs->actionAtoms.end()) - (*partTrans)[p] *= !encAtomSucc(p); + if (ai == rs->actionEntities.end()) + (*partTrans)[p] *= !encEntitySucc(p); } else { @@ -267,20 +267,20 @@ void SymRS::encodeTransitions(void) for (unsigned int j = 0; j < di->second.size(); ++j) { - conditions += encAtomsConj(di->second[j].rctt) * !encAtomsDisj(di->second[j].inhib); + conditions += encEntitiesConj(di->second[j].rctt) * !encEntitiesDisj(di->second[j].inhib); } - (*partTrans)[p] = conditions * encAtomSucc(p); + (*partTrans)[p] = conditions * encEntitySucc(p); - if (ai == rs->actionAtoms.end()) + if (ai == rs->actionEntities.end()) { // not an action entity - (*partTrans)[p] += !conditions * !encAtomSucc(p); + (*partTrans)[p] += !conditions * !encEntitySucc(p); } else { // action entity - (*partTrans)[p] += cuddMgr->bddOne(); //(encAtomSucc(p) + !encAtomSucc(p)); + (*partTrans)[p] += cuddMgr->bddOne(); //(encEntitySucc(p) + !encEntitySucc(p)); } } } @@ -289,13 +289,13 @@ void SymRS::encodeTransitions(void) VERB("Reactions ready"); } -BDD SymRS::getEncState(const RctSys::Atoms &atoms) +BDD SymRS::getEncState(const RctSys::Entities &entities) { assert(0); - //BDD state = compState(encAtomsConj(rs->initState)); - //for (RctSys::Atoms::iterator at = rs->actionAtoms.begin(); at != rs->actionAtoms.end(); ++at) + //BDD state = compState(encEntitiesConj(rs->initState)); + //for (RctSys::Entities::iterator at = rs->actionEntities.begin(); at != rs->actionEntities.end(); ++at) //{ - // state = state.ExistAbstract(encAtom(*at)); + // state = state.ExistAbstract(encEntity(*at)); //} return BDD_FALSE; } @@ -328,7 +328,7 @@ void SymRS::encodeInitStates(void) ++state) { VERB("Encoding a single inital state"); - BDD newInitState = compState(encAtomsConj(*state)); + BDD newInitState = compState(encEntitiesConj(*state)); BDD q = BDD_TRUE; if (opts->part_tr_rel) { @@ -357,7 +357,7 @@ void SymRS::mapStateToAct(void) unsigned int j = 0; for (unsigned int i = 0; i < totalStateVars; ++i) { - if (rs->isActionAtom(i)) { + if (rs->isActionEntity(i)) { stateToAct.push_back(j++); } else @@ -399,13 +399,13 @@ void SymRS::encode(void) VERB("Encoding done"); } -BDD SymRS::encActStrAtom(std::string name) const { - int id = getMappedStateToActID(rs->getAtomID(name)); +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 encActAtom(getMappedStateToActID(rs->getAtomID(name))); + return encActEntity(getMappedStateToActID(rs->getEntityID(name))); } } diff --git a/symrs.hh b/symrs.hh index 42c3dde..2b2cc66 100644 --- a/symrs.hh +++ b/symrs.hh @@ -36,14 +36,14 @@ class SymRS Options *opts; struct ReactionCond { - RctSys::Atoms rctt; - RctSys::Atoms inhib; + RctSys::Entities rctt; + RctSys::Entities inhib; }; typedef vector ReactionConds; - typedef map DecompReactions; - typedef std::vector StateAtomToAction; + typedef map DecompReactions; + typedef std::vector StateEntityToAction; - StateAtomToAction stateToAct; + StateEntityToAction stateToAct; BDD *initStates; vector *pv; @@ -62,33 +62,33 @@ class SymRS unsigned int totalStateVars; unsigned int totalActions; - BDD encAtom_raw(RctSys::Atom atom, bool succ) const; - BDD encAtom(RctSys::Atom atom) const { - return encAtom_raw(atom, false); + BDD encEntity_raw(RctSys::Entity entity, bool succ) const; + BDD encEntity(RctSys::Entity entity) const { + return encEntity_raw(entity, false); } - BDD encActAtom(RctSys::Atom atom) const { - assert(atom < pv_act->size()); - return (*pv_act)[atom]; + BDD encActEntity(RctSys::Entity entity) const { + assert(entity < pv_act->size()); + return (*pv_act)[entity]; } - BDD encAtomSucc(RctSys::Atom atom) const { - return encAtom_raw(atom, true); + BDD encEntitySucc(RctSys::Entity entity) const { + return encEntity_raw(entity, true); } - BDD encAtomsConj_raw(const RctSys::Atoms &atoms, bool succ); - BDD encAtomsConj(const RctSys::Atoms &atoms) { - return encAtomsConj_raw(atoms, false); + BDD encEntitiesConj_raw(const RctSys::Entities &entities, bool succ); + BDD encEntitiesConj(const RctSys::Entities &entities) { + return encEntitiesConj_raw(entities, false); } - BDD encAtomsConjSucc(const RctSys::Atoms &atoms) { - return encAtomsConj_raw(atoms, true); + BDD encEntitiesConjSucc(const RctSys::Entities &entities) { + return encEntitiesConj_raw(entities, true); } - BDD encAtomsDisj_raw(const RctSys::Atoms &atoms, bool succ); - BDD encAtomsDisj(const RctSys::Atoms &atoms) { - return encAtomsDisj_raw(atoms, false); + BDD encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ); + BDD encEntitiesDisj(const RctSys::Entities &entities) { + return encEntitiesDisj_raw(entities, false); } - BDD encAtomsDisjSucc(const RctSys::Atoms &atoms) { - return encAtomsDisj_raw(atoms, true); + BDD encEntitiesDisjSucc(const RctSys::Entities &entities) { + return encEntitiesDisj_raw(entities, true); } - BDD encStateActAtomsConj(const RctSys::Atoms &atoms); - BDD encStateActAtomsDisj(const RctSys::Atoms &atoms); + BDD encStateActEntitiesConj(const RctSys::Entities &entities); + BDD encStateActEntitiesDisj(const RctSys::Entities &entities); /** * @brief Complements an encoding of a given state by negating all the variables that are not set to true @@ -118,7 +118,7 @@ public: { this->rs = rs; this->opts = opts; - totalStateVars = rs->getAtomsSize(); + totalStateVars = rs->getEntitiesSize(); totalReactions = rs->getReactionsSize(); totalActions = rs->getActionsSize(); @@ -134,14 +134,14 @@ public: BDD *getEncPVact_E(void) { return pv_act_E; } vector *getEncPartTrans(void) { return partTrans; } BDD *getEncMonoTrans(void) { return monoTrans; } - BDD getEncState(const RctSys::Atoms &atoms); + BDD getEncState(const RctSys::Entities &entities); BDD *getEncInitStates(void) { return initStates; } Cudd *getCuddMgr(void) { return cuddMgr; } unsigned int getTotalStateVars(void) { return totalStateVars; } - BDD encAtom(std::string name) const { - return encAtom(rs->getAtomID(name)); + BDD encEntity(std::string name) const { + return encEntity(rs->getEntityID(name)); } - BDD encActStrAtom(std::string name) const; + BDD encActStrEntity(std::string name) const; BDD getBDDtrue(void) const { return BDD_TRUE; } BDD getBDDfalse(void) const { return BDD_FALSE; } };