Progressive eca construction

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 **/

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)

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;
+}

stateconstr.hh

@@ -107,6 +107,9 @@ class StateConstr
       assert(arg[1] != nullptr);
       return arg[1];
     }
+
+    bool isFalse(void) const;
+    bool isTrue(void) const;
 };
 
 #endif

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();
 }