From d34e3954c47011eb34eb33478a246ebb2355a121 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 15 Apr 2018 13:20:07 +0100
Subject: [PATCH] First working version of rsCTL verification.

---
 formrsctl.cc |  6 +++---
 formrsctl.hh |  4 ++--
 mc.cc        |  2 ++
 symrs.cc     | 17 +++--------------
 symrs.hh     |  2 +-
 5 files changed, 11 insertions(+), 20 deletions(-)

diff --git a/formrsctl.cc b/formrsctl.cc
index 570544b..f85693a 100644
--- a/formrsctl.cc
+++ b/formrsctl.cc
@@ -12,7 +12,7 @@
 std::string BoolContexts::toStr(void) const
 {
   if (oper == BCTX_PV) {
-    return name;
+    return proc_name + "." + entity_name;
   }
   else if (oper == BCTX_TF) {
     if (tf) {
@@ -44,7 +44,7 @@ std::string BoolContexts::toStr(void) const
 BDD BoolContexts::getBDD(const SymRS *srs) const
 {
   if (oper == BCTX_PV) {
-    return srs->encActStrEntity(name);
+    return srs->encActStrEntity(proc_name, entity_name);
   }
   else if (oper == BCTX_TF) {
     if (tf) {
@@ -76,7 +76,7 @@ BDD BoolContexts::getBDD(const SymRS *srs) const
 std::string FormRSCTL::toStr(void) const
 {
   if (oper == RSCTL_PV) {
-    return proc_name + ":" + entity_name;
+    return proc_name + "." + entity_name;
   }
   else if (oper == RSCTL_TF) {
     if (tf) {
diff --git a/formrsctl.hh b/formrsctl.hh
index 60a9db8..8f64c97 100644
--- a/formrsctl.hh
+++ b/formrsctl.hh
@@ -73,7 +73,7 @@ class BoolContexts
 {
     Oper oper;
     BoolContexts *arg[2];
-    std::string name;
+    std::string entity_name;
     std::string proc_name;
     bool tf;
 
@@ -82,7 +82,7 @@ class BoolContexts
     BoolContexts(std::string procName, std::string varName)
     {
       oper = BCTX_PV;
-      name = varName;
+      entity_name = varName;
       proc_name = procName;
       arg[0] = nullptr;
       arg[1] = nullptr;
diff --git a/mc.cc b/mc.cc
index eda6a2e..315cdc8 100644
--- a/mc.cc
+++ b/mc.cc
@@ -107,6 +107,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
 
   q = q.ExistAbstract(*pv_succ_E);
   q = q.ExistAbstract(*pv_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
   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_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
   return q;
 }
 
diff --git a/symrs.cc b/symrs.cc
index 32889d6..1dcaa55 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -723,21 +723,10 @@ void SymRS::encodeInitStatesForCtxAut(void)
   *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
-  /*
-  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;
+  auto enc_entity = encCtxEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name));
+  return enc_entity;
 }
 
 size_t SymRS::getCtxAutStateEncodingSize(void)
diff --git a/symrs.hh b/symrs.hh
index 600e975..cf7be42 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -87,7 +87,7 @@ class SymRS
     {
       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
     {
       return BDD_TRUE;