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

Added encoding of the DRS state constraints to the context automaton

Browse Source
This commit is contained in:
Artur Meski
2018-10-07 21:45:28 +01:00
parent ac97db8ead
commit 469ca7e46b
4 changed files with 21 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
formrsctlk.cc
View File

@@ -234,7 +234,7 @@ void FormRSCTLK::encodeActions(const SymRS *srs)
// } // }
// } // }
if (boolCtx != nullptr) { if (boolCtx != nullptr) {
*actions_bdd = boolCtx->getBDD(srs); *actions_bdd = boolCtx->getBDDforContext(srs);
} }
else { else {
assert(0); assert(0);

23
stateconstr.cc
View File

@@ -46,14 +46,21 @@ std::string StateConstr::toStr(void) const
BDD StateConstr::getBDDforState(const SymRS *srs) const BDD StateConstr::getBDDforState(const SymRS *srs) const
{ {
assert(0); return getBDD(srs, false);
// return BDD_FALSE;
} }
BDD StateConstr::getBDDforContext(const SymRS *srs) const BDD StateConstr::getBDDforContext(const SymRS *srs) const
{
return getBDD(srs, true);
}
BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
{ {
if (oper == STC_PV) { if (oper == STC_PV) {
return srs->encActStrEntity(proc_name, entity_name); if (encode_context)
return srs->encActStrEntity(proc_name, entity_name);
else
return srs->encEntity(proc_name, entity_name);
} }
else if (oper == STC_TF) { else if (oper == STC_TF) {
if (tf) { if (tf) {
@@ -64,20 +71,20 @@ BDD StateConstr::getBDDforContext(const SymRS *srs) const
} }
} }
else if (oper == STC_AND) { else if (oper == STC_AND) {
return arg[0]->getBDD(srs) * arg[1]->getBDD(srs); return arg[0]->getBDD(srs, encode_context) * arg[1]->getBDD(srs, encode_context);
} }
else if (oper == STC_OR) { else if (oper == STC_OR) {
return arg[0]->getBDD(srs) + arg[1]->getBDD(srs); return arg[0]->getBDD(srs, encode_context) + arg[1]->getBDD(srs, encode_context);
} }
else if (oper == STC_XOR) { else if (oper == STC_XOR) {
return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs); return arg[0]->getBDD(srs, encode_context) ^ arg[1]->getBDD(srs, encode_context);
} }
else if (oper == STC_NOT) { else if (oper == STC_NOT) {
return !arg[0]->getBDD(srs); return !arg[0]->getBDD(srs, encode_context);
} }
else { else {
assert(0); assert(0);
FERROR("Undefined operator used in Boolean context definition. This should not happen."); FERROR("Undefined operator used in Boolean state/context definition. This should not happen.");
return srs->getBDDfalse(); return srs->getBDDfalse();
} }
} }

4
stateconstr.hh
View File

@@ -87,9 +87,7 @@ class StateConstr
std::string toStr(void) const; std::string toStr(void) const;
BDD getBDD(const SymRS *srs) const { BDD getBDD(const SymRS *srs, bool encode_context) const;
return getBDDforContext(srs);
}
BDD getBDDforContext(const SymRS *srs) const; BDD getBDDforContext(const SymRS *srs) const;
BDD getBDDforState(const SymRS *srs) const; BDD getBDDforState(const SymRS *srs) const;

5
symrs.cc
View File

@@ -5,6 +5,7 @@
#include "symrs.hh" #include "symrs.hh"
#include "rs.hh" #include "rs.hh"
#include "stateconstr.hh"
#include "bdd_macro.hh" #include "bdd_macro.hh"
SymRS::SymRS(RctSys *rs, Options *opts) SymRS::SymRS(RctSys *rs, Options *opts)
@@ -946,8 +947,8 @@ void SymRS::encodeCtxAutTrans(void)
BDD enc_src = encCtxAutState(t.src_state); BDD enc_src = encCtxAutState(t.src_state);
BDD enc_dst = encCtxAutStateSucc(t.dst_state); BDD enc_dst = encCtxAutStateSucc(t.dst_state);
BDD enc_ctx = compContext(encContext(t.ctx)); BDD enc_ctx = compContext(encContext(t.ctx));
BDD enc_drs_state = t.state_constr->getBDDforState(this);
BDD new_trans = enc_src * enc_ctx * enc_dst; BDD new_trans = enc_src * enc_drs_state * enc_ctx * enc_dst;
*tr_ca += new_trans; *tr_ca += new_trans;
} }