From 469ca7e46ba406741fcb0d18784b4bc2ea395fc4 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur@Arturs-MacBook-Pro.local>
Date: Sun, 7 Oct 2018 21:45:28 +0100
Subject: [PATCH] Added encoding of the DRS state constraints to the context
 automaton

---
 formrsctlk.cc  |  2 +-
 stateconstr.cc | 23 +++++++++++++++--------
 stateconstr.hh |  4 +---
 symrs.cc       |  7 ++++---
 4 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/formrsctlk.cc b/formrsctlk.cc
index f2f3acc..6921548 100644
--- a/formrsctlk.cc
+++ b/formrsctlk.cc
@@ -234,7 +234,7 @@ void FormRSCTLK::encodeActions(const SymRS *srs)
     //   }
     // }
     if (boolCtx != nullptr) {
-      *actions_bdd = boolCtx->getBDD(srs);
+      *actions_bdd = boolCtx->getBDDforContext(srs);
     }
     else {
       assert(0);
diff --git a/stateconstr.cc b/stateconstr.cc
index 9290ac6..a0d1170 100644
--- a/stateconstr.cc
+++ b/stateconstr.cc
@@ -46,14 +46,21 @@ std::string StateConstr::toStr(void) const
 
 BDD StateConstr::getBDDforState(const SymRS *srs) const
 {
-  assert(0);
-  // return BDD_FALSE;
+  return getBDD(srs, false);
 }
 
 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) {
-    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) {
     if (tf) {
@@ -64,20 +71,20 @@ BDD StateConstr::getBDDforContext(const SymRS *srs) const
     }
   }
   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) {
-    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) {
-    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) {
-    return !arg[0]->getBDD(srs);
+    return !arg[0]->getBDD(srs, encode_context);
   }
   else {
     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();
   }
 }
diff --git a/stateconstr.hh b/stateconstr.hh
index 9b60f2d..482f94c 100644
--- a/stateconstr.hh
+++ b/stateconstr.hh
@@ -87,9 +87,7 @@ class StateConstr
 
     std::string toStr(void) const;
 
-    BDD getBDD(const SymRS *srs) const {
-      return getBDDforContext(srs);
-    }
+    BDD getBDD(const SymRS *srs, bool encode_context) const;
     BDD getBDDforContext(const SymRS *srs) const;
     BDD getBDDforState(const SymRS *srs) const;
 
diff --git a/symrs.cc b/symrs.cc
index b6cafbf..2f2c9aa 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -5,6 +5,7 @@
 
 #include "symrs.hh"
 #include "rs.hh"
+#include "stateconstr.hh"
 #include "bdd_macro.hh"
 
 SymRS::SymRS(RctSys *rs, Options *opts)
@@ -822,7 +823,7 @@ void SymRS::encodeTransitions(void)
   if (usingContextAutomaton()) {
     VERB("Augmenting transition relation encoding with the transition relation for context automaton");
 
-    if (opts->part_tr_rel) {  
+    if (opts->part_tr_rel) {
       auto last_index = numberOfProc;
       (*partTrans)[last_index] = *tr_ca;
     }
@@ -946,8 +947,8 @@ void SymRS::encodeCtxAutTrans(void)
     BDD enc_src = encCtxAutState(t.src_state);
     BDD enc_dst = encCtxAutStateSucc(t.dst_state);
     BDD enc_ctx = compContext(encContext(t.ctx));
-
-    BDD new_trans = enc_src * enc_ctx * enc_dst;
+    BDD enc_drs_state = t.state_constr->getBDDforState(this);
+    BDD new_trans = enc_src * enc_drs_state * enc_ctx * enc_dst;
 
     *tr_ca += new_trans;
   }