From 96b02781360637ee26c1e1119655c81af1cde510 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur@Arturs-MacBook-Pro.local>
Date: Mon, 8 Oct 2018 21:01:39 +0100
Subject: [PATCH] Progressive eca construction

---
 ctx_aut.cc     | 37 +++++++++++++++++++++++++++++++++++++
 ctx_aut.hh     |  1 +
 stateconstr.cc | 22 ++++++++++++++++++++++
 stateconstr.hh |  3 +++
 symrs.cc       |  6 ++++++
 5 files changed, 69 insertions(+)

diff --git a/ctx_aut.cc b/ctx_aut.cc
index d095f9f..b581690 100644
--- a/ctx_aut.cc
+++ b/ctx_aut.cc
@@ -127,4 +127,41 @@ void CtxAut::showTransitions(void)
   }
 }
 
+void CtxAut::makeProgressive(void)
+{
+  std::string special_loc = "T";
+  while (hasState(special_loc))
+  {
+    special_loc += "T";
+  }
+  addState(special_loc);
+
+  std::map<State, StateConstr *> constrs;
+  for (State s = 0; s < states_ids.size(); ++s)
+  {
+    if (constrs.count(s) == 0) {
+      constrs[s] = new StateConstr(false);
+    }
+  }
+
+  for (const auto &t : transitions) {
+    State curr_st = t.src_state;
+    if (t.state_constr != nullptr)
+    {
+      constrs[curr_st] = new StateConstr(
+      STC_OR, constrs[curr_st], t.state_constr);
+    }
+  }
+
+  for (const auto &s : states_ids)
+  {
+      StateConstr *state_constr = nullptr;
+      if (!constrs[getStateID(s)]->isFalse()) {
+        state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
+      }
+      addTransition(s, special_loc, state_constr);
+  }
+
+}
+
 /** EOF **/
diff --git a/ctx_aut.hh b/ctx_aut.hh
index 66bb489..c413632 100644
--- a/ctx_aut.hh
+++ b/ctx_aut.hh
@@ -40,6 +40,7 @@ class CtxAut
     void showStates(void);
     void addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
     void showTransitions(void);
+    void makeProgressive(void);
     void pushContextEntity(Entity entity_id);
     void saveCurrentContextSet(Process proc_id);
     void setOptions(Options *opts)
diff --git a/stateconstr.cc b/stateconstr.cc
index a0d1170..6aef1b8 100644
--- a/stateconstr.cc
+++ b/stateconstr.cc
@@ -88,3 +88,25 @@ BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
     return srs->getBDDfalse();
   }
 }
+
+bool StateConstr::isFalse(void) const
+{
+  if (oper == STC_TF && tf == false)
+    return true;
+
+  if (oper == STC_NOT && arg[0]->oper == STC_TF && arg[0]->tf == true)
+    return true;
+    
+  return false;
+}
+
+bool StateConstr::isTrue(void) const
+{
+  if (oper == STC_TF && tf == true)
+    return true;
+
+  if (oper == STC_NOT && arg[0]->oper == STC_TF && arg[0]->tf == false)
+    return true;
+
+  return false;
+}
diff --git a/stateconstr.hh b/stateconstr.hh
index 482f94c..21b42ae 100644
--- a/stateconstr.hh
+++ b/stateconstr.hh
@@ -107,6 +107,9 @@ class StateConstr
       assert(arg[1] != nullptr);
       return arg[1];
     }
+
+    bool isFalse(void) const;
+    bool isTrue(void) const;
 };
 
 #endif
diff --git a/symrs.cc b/symrs.cc
index a17e661..d05808c 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -34,6 +34,12 @@ SymRS::SymRS(RctSys *rs, Options *opts)
   pv_ca_succ = nullptr;
   tr_ca = nullptr;
 
+  // TODO: this should be triggered by the parser and it should depend
+  //       on an option in the input file
+  rs->ctx_aut->makeProgressive();
+
+  rs->printSystem();
+
   encode();
 }