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

First working version of rsCTL verification.

Browse Source
This commit is contained in:
Artur Meski
2018-04-15 13:20:07 +01:00
parent c4c3af0300
commit d34e3954c4
5 changed files with 11 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
formrsctl.cc
View File

@@ -12,7 +12,7 @@
std::string BoolContexts::toStr(void) const std::string BoolContexts::toStr(void) const
{ {
if (oper == BCTX_PV) { if (oper == BCTX_PV) {
return name; return proc_name + "." + entity_name;
} }
else if (oper == BCTX_TF) { else if (oper == BCTX_TF) {
if (tf) { if (tf) {
@@ -44,7 +44,7 @@ std::string BoolContexts::toStr(void) const
BDD BoolContexts::getBDD(const SymRS *srs) const BDD BoolContexts::getBDD(const SymRS *srs) const
{ {
if (oper == BCTX_PV) { if (oper == BCTX_PV) {
return srs->encActStrEntity(name); return srs->encActStrEntity(proc_name, entity_name);
} }
else if (oper == BCTX_TF) { else if (oper == BCTX_TF) {
if (tf) { if (tf) {
@@ -76,7 +76,7 @@ BDD BoolContexts::getBDD(const SymRS *srs) const
std::string FormRSCTL::toStr(void) const std::string FormRSCTL::toStr(void) const
{ {
if (oper == RSCTL_PV) { if (oper == RSCTL_PV) {
return proc_name + ":" + entity_name; return proc_name + "." + entity_name;
} }
else if (oper == RSCTL_TF) { else if (oper == RSCTL_TF) {
if (tf) { if (tf) {

4
formrsctl.hh
View File

@@ -73,7 +73,7 @@ class BoolContexts
{ {
Oper oper; Oper oper;
BoolContexts *arg[2]; BoolContexts *arg[2];
std::string name; std::string entity_name;
std::string proc_name; std::string proc_name;
bool tf; bool tf;
@@ -82,7 +82,7 @@ class BoolContexts
BoolContexts(std::string procName, std::string varName) BoolContexts(std::string procName, std::string varName)
{ {
oper = BCTX_PV; oper = BCTX_PV;
name = varName; entity_name = varName;
proc_name = procName; proc_name = procName;
arg[0] = nullptr; arg[0] = nullptr;
arg[1] = nullptr; arg[1] = nullptr;

2
mc.cc
View File

@@ -107,6 +107,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
q = q.ExistAbstract(*pv_succ_E); q = q.ExistAbstract(*pv_succ_E);
q = q.ExistAbstract(*pv_ctx_E); q = q.ExistAbstract(*pv_ctx_E);
q = q.ExistAbstract(*pv_proc_enab_E);
return q; return q;
} }
@@ -127,6 +128,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
q = q.ExistAbstract(*pv_succ_E); q = q.ExistAbstract(*pv_succ_E);
q = q.ExistAbstract(*pv_ctx_E); q = q.ExistAbstract(*pv_ctx_E);
q = q.ExistAbstract(*pv_proc_enab_E);
return q; return q;
} }

17
symrs.cc
View File

@@ -723,21 +723,10 @@ void SymRS::encodeInitStatesForCtxAut(void)
*initStates *= getEncCtxAutInitState(); *initStates *= getEncCtxAutInitState();
} }
BDD SymRS::encActStrEntity(std::string name) const BDD SymRS::encActStrEntity(std::string proc_name, std::string entity_name) const
{ {
assert(0); // TODO for rsCTL auto enc_entity = encCtxEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name));
/* return enc_entity;
int id = getMappedStateToActID(rs->getEntityID(name));
if (id < 0) {
FERROR("Entity \"" << name << "\" not defined as context entity");
return BDD_FALSE;
}
else {
return encActEntity(getMappedStateToActID(rs->getEntityID(name)));
}
*/
return BDD_FALSE;
} }
size_t SymRS::getCtxAutStateEncodingSize(void) size_t SymRS::getCtxAutStateEncodingSize(void)

2
symrs.hh
View File

@@ -87,7 +87,7 @@ class SymRS
{ {
return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name)); return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name));
} }
BDD encActStrEntity(std::string name) const; BDD encActStrEntity(std::string proc_name, std::string entity_name) const;
BDD getBDDtrue(void) const BDD getBDDtrue(void) const
{ {
return BDD_TRUE; return BDD_TRUE;