From 206996a7008b3d5b3b7da5c59cfd4308a41cc3b5 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sat, 22 Sep 2018 22:55:00 +0100
Subject: [PATCH] Building of stateconstr.o; prelim. methods for ctx and state
 BDD enc.

---
 Makefile       |  8 +++----
 formrsctlk.cc  | 65 --------------------------------------------------
 stateconstr.cc | 13 ++++++++--
 stateconstr.hh |  8 +++++--
 4 files changed, 21 insertions(+), 73 deletions(-)

diff --git a/Makefile b/Makefile
index 8317c63..0e28206 100644
--- a/Makefile
+++ b/Makefile
@@ -4,13 +4,13 @@ CUDD_INCLUDE=cudd/lib/libcudd.a
 INCLUDES=-Icudd/include
 CPPFLAGS_SILENT = $(INCLUDES)
 CPPFLAGS = -Wall $(CPPFLAGS_SILENT) #-Werror
-#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG 
+#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG
 CXXFLAGS_SILENT = -O3 -g
 CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
 #CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
-LDLIBS = $(CUDD_INCLUDE) 
+LDLIBS = $(CUDD_INCLUDE)
 
-OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o 
+OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o stateconstr.o
 
 all: reactics
 
@@ -44,7 +44,7 @@ rsin_parser.lex.cc: rsin_parser.ll
 	mv lex.yy.c rsin_parser.lex.cc
 
 style:
-	astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh	
+	astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh
 
 commit: style
 	git commit -a
diff --git a/formrsctlk.cc b/formrsctlk.cc
index 6dc82fa..f2f3acc 100644
--- a/formrsctlk.cc
+++ b/formrsctlk.cc
@@ -8,71 +8,6 @@
 
 #include "formrsctlk.hh"
 
-
-std::string StateConstr::toStr(void) const
-{
-  if (oper == STC_PV) {
-    return proc_name + "." + entity_name;
-  }
-  else if (oper == STC_TF) {
-    if (tf) {
-      return "true";
-    }
-    else {
-      return "false";
-    }
-  }
-  else if (oper == STC_AND) {
-    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
-  }
-  else if (oper == STC_OR) {
-    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
-  }
-  else if (oper == STC_XOR) {
-    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
-  }
-  else if (oper == STC_NOT) {
-    return "~" + arg[0]->toStr();
-  }
-
-  else {
-    return "??";
-    assert(0);
-  }
-}
-
-BDD StateConstr::getBDD(const SymRS *srs) const
-{
-  if (oper == STC_PV) {
-    return srs->encActStrEntity(proc_name, entity_name);
-  }
-  else if (oper == STC_TF) {
-    if (tf) {
-      return srs->getBDDtrue();
-    }
-    else {
-      return srs->getBDDfalse();
-    }
-  }
-  else if (oper == STC_AND) {
-    return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
-  }
-  else if (oper == STC_OR) {
-    return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
-  }
-  else if (oper == STC_XOR) {
-    return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
-  }
-  else if (oper == STC_NOT) {
-    return !arg[0]->getBDD(srs);
-  }
-  else {
-    assert(0);
-    FERROR("Undefined operator used in Boolean context definition. This should not happen.");
-    return srs->getBDDfalse();
-  }
-}
-
 std::string FormRSCTLK::toStr(void) const
 {
   if (oper == RSCTLK_PV) {
diff --git a/stateconstr.cc b/stateconstr.cc
index b1e47e4..9290ac6 100644
--- a/stateconstr.cc
+++ b/stateconstr.cc
@@ -7,6 +7,10 @@
 */
 
 #include "stateconstr.hh"
+#include "types.hh"
+#include "cudd.hh"
+#include "bdd_macro.hh"
+#include "symrs.hh"
 
 std::string StateConstr::toStr(void) const
 {
@@ -40,7 +44,13 @@ std::string StateConstr::toStr(void) const
   }
 }
 
-BDD StateConstr::getBDD(const SymRS *srs) const
+BDD StateConstr::getBDDforState(const SymRS *srs) const
+{
+  assert(0);
+  // return BDD_FALSE;
+}
+
+BDD StateConstr::getBDDforContext(const SymRS *srs) const
 {
   if (oper == STC_PV) {
     return srs->encActStrEntity(proc_name, entity_name);
@@ -71,4 +81,3 @@ BDD StateConstr::getBDD(const SymRS *srs) const
     return srs->getBDDfalse();
   }
 }
-
diff --git a/stateconstr.hh b/stateconstr.hh
index 8fbbc59..9b60f2d 100644
--- a/stateconstr.hh
+++ b/stateconstr.hh
@@ -11,7 +11,7 @@
 
 #include "types.hh"
 
-/* For Boolean contexts: */
+/* For state constraints: */
 #define STC_PV   80
 #define STC_AND  81
 #define STC_OR   82
@@ -87,7 +87,11 @@ class StateConstr
 
     std::string toStr(void) const;
 
-    BDD getBDD(const SymRS *srs) const;
+    BDD getBDD(const SymRS *srs) const {
+      return getBDDforContext(srs);
+    }
+    BDD getBDDforContext(const SymRS *srs) const;
+    BDD getBDDforState(const SymRS *srs) const;
 
     Oper getOper(void) const
     {