Prog

ctx_aut.cc

@@ -139,15 +139,22 @@ void CtxAut::makeProgressive(void)
     special_loc += "T";
   }
   addState(special_loc);
+  State special_loc_id = getLastStateID();
 
   std::map<State, StateConstr *> constrs;
   for (State s = 0; s < states_ids.size(); ++s)
   {
+    if (s == special_loc_id) {
+      continue;
+    }
+
     if (constrs.count(s) == 0) {
-      constrs[s] = new StateConstr(false);
+      constrs[s] = new StateConstr(true);
     }
   }
 
+  constrs[special_loc_id] = new StateConstr(true);
+
   for (const auto &t : transitions) {
     State curr_st = t.src_state;
     if (t.state_constr != nullptr)
@@ -160,12 +167,14 @@ void CtxAut::makeProgressive(void)
   for (const auto &s : states_ids)
   {
       StateConstr *state_constr = nullptr;
-      if (!constrs[getStateID(s)]->isFalse()) {
+      if (!constrs[getStateID(s)]->isTrue()) {
         state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
-      }
         addTransition(s, special_loc, state_constr);
       }
 
+  }
+  addTransition(special_loc, special_loc, nullptr);
+
   made_progressive = true;
 
 }

ctx_aut.hh

@@ -35,6 +35,7 @@ class CtxAut
     void setInitState(std::string stateName);
     State getInitState(void);
     State getStateID(std::string name);
+    State getLastStateID(void) { return states_ids.size(); }
     std::string getStateName(State state_id);
     void printAutomaton(void);
     void showStates(void);

rs.cc

@@ -363,7 +363,8 @@ void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
 
 void RctSys::ctxAutFinalise(void)
 {
-  // EMPTY
+  if (gen_ctxaut_progressive_closure)
+    ctx_aut->makeProgressive();
 }
 
 /** EOF **/

stateconstr.cc

@@ -94,7 +94,7 @@ 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)
+  if (oper == STC_NOT && arg[0]->isTrue())
     return true;
 
   return false;
@@ -105,7 +105,7 @@ 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)
+  if (oper == STC_NOT && arg[0]->isFalse())
     return true;
 
   return false;