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

Entities used per process (in reactions)

Browse Source
This commit is contained in:
Artur Meski
2018-03-30 17:51:29 +01:00
parent bac84bfe9a
commit e3ed26e4a1
3 changed files with 190 additions and 138 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
macro.hh
View File

@@ -39,4 +39,7 @@ if (opts->verbose >= (n)) { \
std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl; \
}
#define SET_ADD(set1, set2) (set1).insert((set2).begin(), (set2).end())
#endif

102
symrs.cc
View File

@@ -28,6 +28,77 @@ SymRS::SymRS(RctSys *rs, Options *opts)
encode();
}
void SymRS::encode(void)
{
VERB("Encoding...");
if (opts->measure) {
opts->enc_time = cpuTime();
opts->enc_mem = memUsed();
}
mapStateToAct();
mapProcEntities();
initBDDvars();
if (usingContextAutomaton()) {
encodeCtxAutTrans();
}
else {
VERB_LN(3, "Not using context automata, not encoding TR for CA")
}
encodeTransitions();
encodeInitStates();
if (opts->measure) {
opts->enc_time = cpuTime() - opts->enc_time;
opts->enc_mem = memUsed() - opts->enc_mem;
}
VERB("Encoding done");
}
void SymRS::mapProcEntities(void)
{
// Reactions
for (const auto &proc_rcts : rs->proc_reactions) {
Process proc_id = proc_rcts.first;
for (const auto &rct : proc_rcts.second) {
// collect entities that can be produced
// locally by the process with proc_id
SET_ADD(usedEntities[proc_id], rct.prod);
}
}
// Context automaton
// for ()
printUsedEntitiesPerProc();
}
void SymRS::printUsedEntitiesPerProc(void)
{
for (const auto &proc_entities : usedEntities) {
std::string proc_name = rs->getProcessName(proc_entities.first);
cout << proc_name << ": ";
for (const auto &ent : proc_entities.second) {
cout << rs->getEntityName(ent) << " ";
}
cout << endl;
}
}
BDD SymRS::encEntity_raw(Entity entity, bool succ) const
{
BDD r;
@@ -455,37 +526,6 @@ void SymRS::mapStateToAct(void)
}
}
void SymRS::encode(void)
{
VERB("Encoding...");
if (opts->measure) {
opts->enc_time = cpuTime();
opts->enc_mem = memUsed();
}
mapStateToAct();
initBDDvars();
if (usingContextAutomaton()) {
encodeCtxAutTrans();
}
else {
VERB_LN(3, "Not using context automata, not encoding TR for CA")
}
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
{
int id = getMappedStateToActID(rs->getEntityID(name));

223
symrs.hh
View File

@@ -32,113 +32,6 @@ class SymRS
friend class ModelChecker;
friend class FormRSCTL;
RctSys *rs;
Cudd *cuddMgr;
Options *opts;
// Mapping: entity ID -> action/context entity ID
StateEntityToAction stateToAct;
BDD *initStates;
vector<BDD> *pv;
vector<BDD> *pv_succ;
BDD *pv_E;
BDD *pv_succ_E;
vector<BDD> *pv_rs;
vector<BDD> *pv_rs_succ;
BDD *pv_rs_E;
BDD *pv_rs_succ_E;
vector<BDD> *partTrans;
BDD *monoTrans;
// Context automaton
vector<BDD> *pv_ca;
vector<BDD> *pv_ca_succ;
BDD *pv_ca_E;
BDD *pv_ca_succ_E;
BDD *tr_ca;
vector<BDD> *pv_act;
BDD *pv_act_E;
unsigned int totalStateVars;
unsigned int totalReactions;
unsigned int totalRctSysStateVars;
unsigned int totalActions;
unsigned int totalCtxAutStateVars;
BDD encEntity_raw(Entity entity, bool succ) const;
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 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 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 encEntitiesDisjSucc(const Entities &entities)
{
return encEntitiesDisj_raw(entities, true);
}
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
*
* @return Returns the encoded state
*/
BDD compState(const BDD &state) const;
BDD compContext(const BDD &context) const;
std::string decodedRctSysStateToStr(const BDD &state);
void printDecodedRctSysStates(const BDD &states);
BDD encNoContext(void);
void initBDDvars(void);
void encodeTransitions(void);
void encodeTransitions_old(void);
void encodeInitStates(void);
void encodeInitStatesForCtxAut(void);
void encodeInitStatesNoCtxAut(void);
void mapStateToAct(void);
void encode(void);
int getMappedStateToActID(int stateID) const
{
assert(stateID < static_cast<int>(totalRctSysStateVars));
return stateToAct[stateID];
}
size_t getCtxAutStateEncodingSize(void);
public:
SymRS(RctSys *rs, Options *opts);
@@ -300,6 +193,122 @@ class SymRS
{
return tr_ca;
}
private:
RctSys *rs;
Cudd *cuddMgr;
Options *opts;
// Mapping: entity ID -> action/context entity ID
StateEntityToAction stateToAct;
BDD *initStates;
vector<BDD> *pv;
vector<BDD> *pv_succ;
BDD *pv_E;
BDD *pv_succ_E;
vector<BDD> *pv_rs;
vector<BDD> *pv_rs_succ;
BDD *pv_rs_E;
BDD *pv_rs_succ_E;
vector<BDD> *partTrans;
BDD *monoTrans;
// Context automaton
vector<BDD> *pv_ca;
vector<BDD> *pv_ca_succ;
BDD *pv_ca_E;
BDD *pv_ca_succ_E;
BDD *tr_ca;
vector<BDD> *pv_act;
BDD *pv_act_E;
unsigned int totalStateVars;
unsigned int totalReactions;
unsigned int totalRctSysStateVars;
unsigned int totalActions;
unsigned int totalCtxAutStateVars;
EntitiesForProc usedEntities;
BDD encEntity_raw(Entity entity, bool succ) const;
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 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 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 encEntitiesDisjSucc(const Entities &entities)
{
return encEntitiesDisj_raw(entities, true);
}
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
*
* @return Returns the encoded state
*/
BDD compState(const BDD &state) const;
BDD compContext(const BDD &context) const;
std::string decodedRctSysStateToStr(const BDD &state);
void printDecodedRctSysStates(const BDD &states);
BDD encNoContext(void);
void initBDDvars(void);
void encodeTransitions(void);
void encodeTransitions_old(void);
void encodeInitStates(void);
void encodeInitStatesForCtxAut(void);
void encodeInitStatesNoCtxAut(void);
void mapStateToAct(void);
void mapProcEntities(void);
void encode(void);
void printUsedEntitiesPerProc(void);
int getMappedStateToActID(int stateID) const
{
assert(stateID < static_cast<int>(totalRctSysStateVars));
return stateToAct[stateID];
}
size_t getCtxAutStateEncodingSize(void);
};
#endif