artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

atom -> entity

Browse Source
This commit is contained in:
Artur Meski
2018-02-17 17:09:17 +00:00
parent ae01b78563
commit 6dbdd586d6
9 changed files with 202 additions and 189 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
formrsctl.cc
View File

@@ -48,7 +48,7 @@ BDD BoolContexts::getBDD(const SymRS *srs) const
{ {
if (oper == BCTX_PV) if (oper == BCTX_PV)
{ {
return srs->encActStrAtom(name); return srs->encActStrEntity(name);
} }
else if (oper == BCTX_TF) 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)) if (RSCTL_COND_1ARG(oper))
{ {
arg[0]->encodeAtoms(srs); arg[0]->encodeEntities(srs);
} }
else if (RSCTL_COND_2ARG(oper)) else if (RSCTL_COND_2ARG(oper))
{ {
arg[0]->encodeAtoms(srs); arg[0]->encodeEntities(srs);
arg[1]->encodeAtoms(srs); arg[1]->encodeEntities(srs);
} }
else if (oper == RSCTL_PV) 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(); BDD single_action = srs->getBDDtrue();
for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) 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); single_action = srs->compContext(single_action);
*actions_bdd += single_action; *actions_bdd += single_action;

2
formrsctl.hh
View File

@@ -321,7 +321,7 @@ public:
assert(oper == RSCTL_TF); assert(oper == RSCTL_TF);
return tf; return tf;
} }
void encodeAtoms(const SymRS *srs); void encodeEntities(const SymRS *srs);
void encodeActions(const SymRS *srs); void encodeActions(const SymRS *srs);
void forgetActionsBDD(void) { void forgetActionsBDD(void) {
if (actions_bdd != NULL) delete actions_bdd; if (actions_bdd != NULL) delete actions_bdd;

14
mc.cc
View File

@@ -117,7 +117,7 @@ void ModelChecker::printReachWithSucc(void)
cleanup(); cleanup();
} }
bool ModelChecker::checkReach(const RctSys::Atoms testState) bool ModelChecker::checkReach(const RctSys::Entities testState)
{ {
if (opts->measure) if (opts->measure)
opts->ver_time = cpuTime(); opts->ver_time = cpuTime();
@@ -370,9 +370,9 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
VERB("Model checking for RSCTL formula: " << form->toStr()); VERB("Model checking for RSCTL formula: " << form->toStr());
VERB("Processing the formula: encoding atoms"); VERB("Processing the formula: encoding entities");
form->encodeAtoms(srs); form->encodeEntities(srs);
VERB("Atoms encoded"); VERB("Entities encoded");
VERB("Processing the formula: encoding actions/contexts"); VERB("Processing the formula: encoding actions/contexts");
form->encodeActions(srs); form->encodeActions(srs);
@@ -448,9 +448,9 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
VERB("Bounded model checking for RSCTL formula: " << form->toStr()); VERB("Bounded model checking for RSCTL formula: " << form->toStr());
VERB("Processing the formula: encoding atoms"); VERB("Processing the formula: encoding entities");
form->encodeAtoms(srs); form->encodeEntities(srs);
VERB("Atoms encoded"); VERB("Entities encoded");
VERB("Processing the formula: encoding actions/contexts"); VERB("Processing the formula: encoding actions/contexts");
form->encodeActions(srs); form->encodeActions(srs);

2
mc.hh
View File

@@ -67,7 +67,7 @@ public:
void printReach(void); void printReach(void);
void printReachWithSucc(void); void printReachWithSucc(void);
bool checkReach(const RctSys::Atoms testState); bool checkReach(const RctSys::Entities testState);
bool checkRSCTL(FormRSCTL *form); bool checkRSCTL(FormRSCTL *form);
bool checkRSCTLfull(FormRSCTL *form); bool checkRSCTLfull(FormRSCTL *form);
bool checkRSCTLbmc(FormRSCTL *form); bool checkRSCTLbmc(FormRSCTL *form);

98
rs.cc
View File

@@ -8,64 +8,64 @@
#include "rs.hh" #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; return false;
else else
return true; 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); entities_ids.push_back(name);
atoms_names[name] = new_atom_id; entities_names[name] = new_entity_id;
} }
} }
std::string RctSys::getAtomName(Atom atomID) std::string RctSys::getEntityName(Entity entityID)
{ {
if (atomID < atoms_ids.size()) if (entityID < entities_ids.size())
return atoms_ids[atomID]; return entities_ids[entityID];
else else
{ {
FERROR("No such atom ID: " << atomID); FERROR("No such entity ID: " << entityID);
return "??"; 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)) if (!hasEntity(entityName))
addAtom(atomName); addEntity(entityName);
tmpReactants.insert(getAtomID(atomName)); tmpReactants.insert(getEntityID(entityName));
} }
void RctSys::pushInhibitor(std::string atomName) void RctSys::pushInhibitor(std::string entityName)
{ {
if (!hasAtom(atomName)) if (!hasEntity(entityName))
addAtom(atomName); addEntity(entityName);
tmpInhibitors.insert(getAtomID(atomName)); tmpInhibitors.insert(getEntityID(entityName));
} }
void RctSys::pushProduct(std::string atomName) void RctSys::pushProduct(std::string entityName)
{ {
if (!hasAtom(atomName)) if (!hasEntity(entityName))
addAtom(atomName); addEntity(entityName);
tmpProducts.insert(getAtomID(atomName)); tmpProducts.insert(getEntityID(entityName));
} }
void RctSys::commitReaction(void) void RctSys::commitReaction(void)
@@ -85,12 +85,12 @@ void RctSys::commitReaction(void)
tmpProducts.clear(); tmpProducts.clear();
} }
std::string RctSys::atomsToStr(const Atoms &atoms) std::string RctSys::entitiesToStr(const Entities &entities)
{ {
std::string s = " "; 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; return s;
} }
@@ -100,19 +100,19 @@ void RctSys::showReactions(void)
cout << "# Reactions:" << endl; cout << "# Reactions:" << endl;
for (auto r = reactions.begin(); r != reactions.end(); ++r) for (auto r = reactions.begin(); r != reactions.end(); ++r)
{ {
cout << " * (R={" << atomsToStr(r->rctt) << "}," cout << " * (R={" << entitiesToStr(r->rctt) << "},"
<< "I={" << atomsToStr(r->inhib) << "}," << "I={" << entitiesToStr(r->inhib) << "},"
<< "P={" << atomsToStr(r->prod) << "})" << endl; << "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) 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)) if (!hasEntity(entityName))
addAtom(atomName); addEntity(entityName);
actionAtoms.insert(getAtomID(atomName)); 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; return true;
else else
return false; return false;
} }
void RctSys::showActionAtoms(void) void RctSys::showActionEntities(void)
{ {
cout << "# Context entities:"; 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; cout << endl;
} }
@@ -155,7 +155,7 @@ void RctSys::showInitialStates(void)
cout << " *"; cout << " *";
for (auto a = s->begin(); a != s->end(); ++a) for (auto a = s->begin(); a != s->end(); ++a)
{ {
cout << " " << getAtomName(*a); cout << " " << getEntityName(*a);
} }
cout << endl; cout << endl;
} }
@@ -164,7 +164,7 @@ void RctSys::showInitialStates(void)
void RctSys::printSystem(void) void RctSys::printSystem(void)
{ {
showInitialStates(); showInitialStates();
showActionAtoms(); showActionEntities();
showReactions(); showReactions();
} }

79
rs.hh
View File

@@ -26,34 +26,35 @@ class RctSys
{ {
friend class SymRS; friend class SymRS;
friend class SymRSstate; friend class SymRSstate;
friend class CtxAut;
public: public:
typedef unsigned int Atom; typedef unsigned int Entity;
typedef std::set<Atom> Atoms; typedef std::set<Entity> Entities;
struct Reaction { struct Reaction {
Atoms rctt; Entities rctt;
Atoms inhib; Entities inhib;
Atoms prod; Entities prod;
}; };
typedef std::vector<Reaction> Reactions; typedef std::vector<Reaction> Reactions;
typedef std::vector<std::string> AtomsByIds; typedef std::vector<std::string> EntitiesByIds;
typedef std::map<std::string, Atom> AtomsByName; typedef std::map<std::string, Entity> EntitiesByName;
typedef std::set<Atoms> AtomsSets; typedef std::set<Entities> EntitiesSets;
private: private:
Reactions reactions; Reactions reactions;
AtomsSets initStates; EntitiesSets initStates;
Atoms actionAtoms; Entities actionEntities;
AtomsByIds atoms_ids; EntitiesByIds entities_ids;
AtomsByName atoms_names; EntitiesByName entities_names;
Atoms tmpReactants; Entities tmpReactants;
Atoms tmpInhibitors; Entities tmpInhibitors;
Atoms tmpProducts; Entities tmpProducts;
Atoms tmpState; Entities tmpState;
Atom getAtomID(std::string atomName); Entity getEntityID(std::string entityName);
Options *opts; Options *opts;
@@ -62,38 +63,50 @@ public:
{ {
this->opts = opts; this->opts = opts;
} }
bool hasAtom(std::string atomName); bool hasEntity(std::string entityName);
void addAtom(std::string atomName); void addEntity(std::string entityName);
std::string getAtomName(Atom atomID); std::string getEntityName(Entity entityID);
void pushReactant(std::string atomName); void pushReactant(std::string entityName);
void pushInhibitor(std::string atomName); void pushInhibitor(std::string entityName);
void pushProduct(std::string atomName); void pushProduct(std::string entityName);
void commitReaction(void); void commitReaction(void);
std::string atomToStr(const Atom atom) { std::string entityToStr(const Entity entity) {
return atoms_ids[atom]; return entities_ids[entity];
} }
std::string atomsToStr(const Atoms &atoms); std::string entitiesToStr(const Entities &entities);
void showReactions(void); void showReactions(void);
void pushStateAtom(std::string atomName); void pushStateEntity(std::string entityName);
void commitInitState(void); void commitInitState(void);
void addActionAtom(std::string atomName); void addActionEntity(std::string entityName);
bool isActionAtom(Atom atom); bool isActionEntity(Entity entity);
void resetInitStates(void) { void resetInitStates(void) {
initStates.clear(); initStates.clear();
} }
unsigned int getAtomsSize(void) { unsigned int getEntitiesSize(void) {
return atoms_ids.size(); return entities_ids.size();
} }
unsigned int getReactionsSize(void) { unsigned int getReactionsSize(void) {
return reactions.size(); return reactions.size();
} }
unsigned int getActionsSize(void) { unsigned int getActionsSize(void) {
return actionAtoms.size(); return actionEntities.size();
} }
void showInitialStates(void); void showInitialStates(void);
void showActionAtoms(void); void showActionEntities(void);
void printSystem(void); void printSystem(void);
}; };
// Context Automaton
class CtxAut
{
typedef unsigned int State;
typedef std::set<State> States;
struct Transition {
State src_state;
State dst_state;
};
};
#endif #endif

20
rsin_parser.yy
View File

@@ -76,7 +76,7 @@ class rsin_driver;
system: system:
| REACTIONS LCB reactions RCB system | REACTIONS LCB reactions RCB system
| INITIALCONTEXTS LCB initstates RCB system | INITIALCONTEXTS LCB initstates RCB system
| CONTEXTENTITIES LCB actionatoms RCB system | CONTEXTENTITIES LCB actionentities RCB system
| RSCTLFORM LCB rsctl_form RCB system { | RSCTLFORM LCB rsctl_form RCB system {
driver.addFormRSCTL($3); driver.addFormRSCTL($3);
} }
@@ -140,23 +140,23 @@ initstates:
; ;
initstate: initstate:
| atom | entity
| initstate COMMA atom | initstate COMMA entity
; ;
atom: IDENTIFIER { entity: IDENTIFIER {
driver.rs->pushStateAtom(*$1); driver.rs->pushStateEntity(*$1);
free($1); free($1);
} }
; ;
actionatoms: actionentities:
| actatom | actentity
| actionatoms COMMA actatom | actionentities COMMA actentity
; ;
actatom: IDENTIFIER { actentity: IDENTIFIER {
driver.rs->addActionAtom(*$1); driver.rs->addActionEntity(*$1);
free($1); free($1);
} }
; ;

102
symrs.cc
View File

@@ -8,70 +8,70 @@
#include "symrs.hh" #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; BDD r;
if (succ) if (succ)
r = (*pv_succ)[atom]; r = (*pv_succ)[entity];
else else
r = (*pv)[atom]; r = (*pv)[entity];
return r; 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; 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); if (succ) r *= encEntitySucc(*entity);
else r *= encAtom(*atom); else r *= encEntity(*entity);
} }
return r; 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; 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); if (succ) r += encEntitySucc(*entity);
else r += encAtom(*atom); else r += encEntity(*entity);
} }
return r; return r;
} }
BDD SymRS::encStateActAtomsConj(const RctSys::Atoms &atoms) BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities)
{ {
BDD r = BDD_TRUE; 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); BDD state_act = encEntity(*entity);
int actAtom; int actEntity;
if ((actAtom = getMappedStateToActID(*atom)) >= 0) if ((actEntity = getMappedStateToActID(*entity)) >= 0)
state_act += encActAtom(actAtom); state_act += encActEntity(actEntity);
r *= state_act; r *= state_act;
} }
return r; return r;
} }
BDD SymRS::encStateActAtomsDisj(const RctSys::Atoms &atoms) BDD SymRS::encStateActEntitiesDisj(const RctSys::Entities &entities)
{ {
BDD r = BDD_FALSE; 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); BDD state_act = encEntity(*entity);
int actAtom; int actEntity;
if ((actAtom = getMappedStateToActID(*atom)) >= 0) if ((actEntity = getMappedStateToActID(*entity)) >= 0)
state_act += encActAtom(actAtom); state_act += encActEntity(actEntity);
r += state_act; r += state_act;
} }
@@ -109,9 +109,9 @@ std::string SymRS::decodedStateToStr(const BDD &state)
std::string s = "{ "; std::string s = "{ ";
for (unsigned int i = 0; i < totalStateVars; ++i) 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 += "}"; s += "}";
@@ -137,7 +137,7 @@ void SymRS::initBDDvars(void)
{ {
cuddMgr = new Cudd(0,0); cuddMgr = new Cudd(0,0);
//RctSys::Atoms aa = rs->actionAtoms; //RctSys::Entities aa = rs->actionEntities;
VERB("Preparing BDD variables"); VERB("Preparing BDD variables");
pv = new vector<BDD>(totalStateVars); pv = new vector<BDD>(totalStateVars);
@@ -157,7 +157,7 @@ void SymRS::initBDDvars(void)
*pv_E *= (*pv)[i]; *pv_E *= (*pv)[i];
*pv_succ_E *= (*pv_succ)[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); // (*pv_noact)[j++] = cuddMgr->bddVar(i*2);
} }
@@ -182,7 +182,7 @@ void SymRS::encodeTransitions(void)
cond.rctt = rs->reactions[i].rctt; cond.rctt = rs->reactions[i].rctt;
cond.inhib = rs->reactions[i].inhib; 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) p != rs->reactions[i].prod.end(); ++p)
{ {
dr[*p].push_back(cond); dr[*p].push_back(cond);
@@ -212,10 +212,10 @@ void SymRS::encodeTransitions(void)
{ {
// nie ma reakcji produkujacej p: // nie ma reakcji produkujacej p:
if (opts->part_tr_rel) if (opts->part_tr_rel)
(*partTrans)[p] = !encAtomSucc(p); (*partTrans)[p] = !encEntitySucc(p);
else else
{ {
*monoTrans *= !encAtomSucc(p); *monoTrans *= !encEntitySucc(p);
} }
} }
else else
@@ -228,17 +228,17 @@ void SymRS::encodeTransitions(void)
for (unsigned int j = 0; j < di->second.size(); ++j) 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) if (opts->part_tr_rel)
{ {
(*partTrans)[p] = conditions * encAtomSucc(p); (*partTrans)[p] = conditions * encEntitySucc(p);
(*partTrans)[p] += !conditions * !encAtomSucc(p); (*partTrans)[p] += !conditions * !encEntitySucc(p);
} }
else else
{ {
*monoTrans *= (conditions * encAtomSucc(p)) + (!conditions * !encAtomSucc(p)); *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc(p));
} }
} }
if (opts->reorder_trans) if (opts->reorder_trans)
@@ -252,14 +252,14 @@ void SymRS::encodeTransitions(void)
/* /*
for (unsigned int p = 0; p < totalStateVars; ++p) // we iterate through products 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; DecompReactions::iterator di;
if ((di = dr.find(p)) == dr.end()) if ((di = dr.find(p)) == dr.end())
{ {
(*partTrans)[p] = cuddMgr->bddOne(); (*partTrans)[p] = cuddMgr->bddOne();
if (ai == rs->actionAtoms.end()) if (ai == rs->actionEntities.end())
(*partTrans)[p] *= !encAtomSucc(p); (*partTrans)[p] *= !encEntitySucc(p);
} }
else else
{ {
@@ -267,20 +267,20 @@ void SymRS::encodeTransitions(void)
for (unsigned int j = 0; j < di->second.size(); ++j) 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 // not an action entity
(*partTrans)[p] += !conditions * !encAtomSucc(p); (*partTrans)[p] += !conditions * !encEntitySucc(p);
} }
else else
{ {
// action entity // 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"); VERB("Reactions ready");
} }
BDD SymRS::getEncState(const RctSys::Atoms &atoms) BDD SymRS::getEncState(const RctSys::Entities &entities)
{ {
assert(0); assert(0);
//BDD state = compState(encAtomsConj(rs->initState)); //BDD state = compState(encEntitiesConj(rs->initState));
//for (RctSys::Atoms::iterator at = rs->actionAtoms.begin(); at != rs->actionAtoms.end(); ++at) //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; return BDD_FALSE;
} }
@@ -328,7 +328,7 @@ void SymRS::encodeInitStates(void)
++state) ++state)
{ {
VERB("Encoding a single inital state"); VERB("Encoding a single inital state");
BDD newInitState = compState(encAtomsConj(*state)); BDD newInitState = compState(encEntitiesConj(*state));
BDD q = BDD_TRUE; BDD q = BDD_TRUE;
if (opts->part_tr_rel) if (opts->part_tr_rel)
{ {
@@ -357,7 +357,7 @@ void SymRS::mapStateToAct(void)
unsigned int j = 0; unsigned int j = 0;
for (unsigned int i = 0; i < totalStateVars; ++i) for (unsigned int i = 0; i < totalStateVars; ++i)
{ {
if (rs->isActionAtom(i)) { if (rs->isActionEntity(i)) {
stateToAct.push_back(j++); stateToAct.push_back(j++);
} }
else else
@@ -399,13 +399,13 @@ void SymRS::encode(void)
VERB("Encoding done"); VERB("Encoding done");
} }
BDD SymRS::encActStrAtom(std::string name) const { BDD SymRS::encActStrEntity(std::string name) const {
int id = getMappedStateToActID(rs->getAtomID(name)); int id = getMappedStateToActID(rs->getEntityID(name));
if (id < 0) if (id < 0)
{ {
FERROR("Entity \"" << name << "\" not defined as context entity"); FERROR("Entity \"" << name << "\" not defined as context entity");
return BDD_FALSE; return BDD_FALSE;
} else { } else {
return encActAtom(getMappedStateToActID(rs->getAtomID(name))); return encActEntity(getMappedStateToActID(rs->getEntityID(name)));
} }
} }

60
symrs.hh
View File

@@ -36,14 +36,14 @@ class SymRS
Options *opts; Options *opts;
struct ReactionCond { struct ReactionCond {
RctSys::Atoms rctt; RctSys::Entities rctt;
RctSys::Atoms inhib; RctSys::Entities inhib;
}; };
typedef vector<ReactionCond> ReactionConds; typedef vector<ReactionCond> ReactionConds;
typedef map<RctSys::Atom,ReactionConds> DecompReactions; typedef map<RctSys::Entity,ReactionConds> DecompReactions;
typedef std::vector<int> StateAtomToAction; typedef std::vector<int> StateEntityToAction;
StateAtomToAction stateToAct; StateEntityToAction stateToAct;
BDD *initStates; BDD *initStates;
vector<BDD> *pv; vector<BDD> *pv;
@@ -62,33 +62,33 @@ class SymRS
unsigned int totalStateVars; unsigned int totalStateVars;
unsigned int totalActions; unsigned int totalActions;
BDD encAtom_raw(RctSys::Atom atom, bool succ) const; BDD encEntity_raw(RctSys::Entity entity, bool succ) const;
BDD encAtom(RctSys::Atom atom) const { BDD encEntity(RctSys::Entity entity) const {
return encAtom_raw(atom, false); return encEntity_raw(entity, false);
} }
BDD encActAtom(RctSys::Atom atom) const { BDD encActEntity(RctSys::Entity entity) const {
assert(atom < pv_act->size()); assert(entity < pv_act->size());
return (*pv_act)[atom]; return (*pv_act)[entity];
} }
BDD encAtomSucc(RctSys::Atom atom) const { BDD encEntitySucc(RctSys::Entity entity) const {
return encAtom_raw(atom, true); return encEntity_raw(entity, true);
} }
BDD encAtomsConj_raw(const RctSys::Atoms &atoms, bool succ); BDD encEntitiesConj_raw(const RctSys::Entities &entities, bool succ);
BDD encAtomsConj(const RctSys::Atoms &atoms) { BDD encEntitiesConj(const RctSys::Entities &entities) {
return encAtomsConj_raw(atoms, false); return encEntitiesConj_raw(entities, false);
} }
BDD encAtomsConjSucc(const RctSys::Atoms &atoms) { BDD encEntitiesConjSucc(const RctSys::Entities &entities) {
return encAtomsConj_raw(atoms, true); return encEntitiesConj_raw(entities, true);
} }
BDD encAtomsDisj_raw(const RctSys::Atoms &atoms, bool succ); BDD encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ);
BDD encAtomsDisj(const RctSys::Atoms &atoms) { BDD encEntitiesDisj(const RctSys::Entities &entities) {
return encAtomsDisj_raw(atoms, false); return encEntitiesDisj_raw(entities, false);
} }
BDD encAtomsDisjSucc(const RctSys::Atoms &atoms) { BDD encEntitiesDisjSucc(const RctSys::Entities &entities) {
return encAtomsDisj_raw(atoms, true); return encEntitiesDisj_raw(entities, true);
} }
BDD encStateActAtomsConj(const RctSys::Atoms &atoms); BDD encStateActEntitiesConj(const RctSys::Entities &entities);
BDD encStateActAtomsDisj(const RctSys::Atoms &atoms); 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 * @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->rs = rs;
this->opts = opts; this->opts = opts;
totalStateVars = rs->getAtomsSize(); totalStateVars = rs->getEntitiesSize();
totalReactions = rs->getReactionsSize(); totalReactions = rs->getReactionsSize();
totalActions = rs->getActionsSize(); totalActions = rs->getActionsSize();
@@ -134,14 +134,14 @@ public:
BDD *getEncPVact_E(void) { return pv_act_E; } BDD *getEncPVact_E(void) { return pv_act_E; }
vector<BDD> *getEncPartTrans(void) { return partTrans; } vector<BDD> *getEncPartTrans(void) { return partTrans; }
BDD *getEncMonoTrans(void) { return monoTrans; } BDD *getEncMonoTrans(void) { return monoTrans; }
BDD getEncState(const RctSys::Atoms &atoms); BDD getEncState(const RctSys::Entities &entities);
BDD *getEncInitStates(void) { return initStates; } BDD *getEncInitStates(void) { return initStates; }
Cudd *getCuddMgr(void) { return cuddMgr; } Cudd *getCuddMgr(void) { return cuddMgr; }
unsigned int getTotalStateVars(void) { return totalStateVars; } unsigned int getTotalStateVars(void) { return totalStateVars; }
BDD encAtom(std::string name) const { BDD encEntity(std::string name) const {
return encAtom(rs->getAtomID(name)); 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 getBDDtrue(void) const { return BDD_TRUE; }
BDD getBDDfalse(void) const { return BDD_FALSE; } BDD getBDDfalse(void) const { return BDD_FALSE; }
}; };