Make Progressive as option

rs.cc

@@ -9,6 +9,7 @@ RctSys::RctSys(void)
   : current_process_defined(false)
 {
   ctx_aut = nullptr;
+  gen_ctxaut_progressive_closure = false;
 }
 
 bool RctSys::hasEntity(std::string name)
@@ -306,6 +307,11 @@ void RctSys::ctxAutEnable(void)
   ctx_aut = new CtxAut(opts, this);
 }
 
+void RctSys::ctxAutEnableProgressiveClosure(void)
+{
+  gen_ctxaut_progressive_closure = true;
+}
+
 void RctSys::ctxAutAddState(std::string stateName)
 {
   assert(ctx_aut != nullptr);
@@ -355,4 +361,9 @@ void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
   ctx_aut->saveCurrentContextSet(processID);
 }
 
+void RctSys::ctxAutFinalise(void)
+{
+  ctx_aut->makeProgressive();
+}
+
 /** EOF **/

rs.hh

@@ -85,12 +85,14 @@ class RctSys
     void printSystem(void);
 
     void ctxAutEnable(void);
+    void ctxAutEnableProgressiveClosure(void);
     void ctxAutAddState(std::string stateName);
     void ctxAutSetInitState(std::string stateName);
     void ctxAutAddTransition(std::string srcStateName, std::string dstStateName);
     void ctxAutAddTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
     void ctxAutPushNamedContextEntity(std::string entity_name);
     void ctxAutSaveCurrentContextSet(std::string processName);
+    void ctxAutFinalise(void);
 
     bool initStatesDefined(void)
     {
@@ -116,6 +118,8 @@ class RctSys
 
     CtxAut *ctx_aut;
 
+    bool gen_ctxaut_progressive_closure;
+
     EntitiesById entities_ids;
     EntitiesByName entities_names;
 

rsin_driver.cc

@@ -22,6 +22,7 @@ void rsin_driver::initialise(void)
   opts = nullptr;
   use_ctx_aut = false;
   use_concentrations = false;
+  use_progressive = false;
 }
 
 rsin_driver::~rsin_driver ()
@@ -106,3 +107,17 @@ void rsin_driver::useContextAutomaton(void)
   getReactionSystem()->ctxAutEnable();
 }
 
+void rsin_driver::makeProgressive(void)
+{
+  use_progressive = true;
+  if (use_ctx_aut)
+  {
+    getReactionSystem()->ctxAutEnableProgressiveClosure();
+  }
+  else
+  {
+    FERROR("Context automaton not enabled");
+  }
+}
+
+// EOF

rsin_driver.hh

@@ -35,6 +35,7 @@ class rsin_driver
     // options in configuration file:
     bool use_ctx_aut;
     bool use_concentrations;
+    bool use_progressive;
 
     // Handling the scanner
     void scan_begin();
@@ -60,7 +61,7 @@ class rsin_driver
       ensureOptionsAllowed();
       use_concentrations = true;
     };
-
+    void makeProgressive(void);
     void ensureReactionSystemReady(void);
     void setupReactionSystem(void);
 
@@ -78,4 +79,3 @@ class rsin_driver
 };
 
 #endif
-

rsin_parser.ll

@@ -41,6 +41,7 @@ blank [ \t]
 "options"				        return token::OPTIONS;
 "use-context-automaton"	return token::USE_CTX_AUT;
 "use-concentrations"	  return token::USE_CONCENTRATIONS;
+"make-progressive"      return token::MAKE_PROGRESSIVE;
 "reactions"             return token::REACTIONS;
 "initial-contexts"      return token::INITIALCONTEXTS;
 "context-entities"      return token::CONTEXTENTITIES;
@@ -128,4 +129,3 @@ rsin_driver::scan_end()
 {
   fclose(yyin);
 }
-

rsin_parser.yy

@@ -46,7 +46,7 @@ class rsin_driver;
 #include "rsin_driver.hh"
 }
 
-%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
+%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS MAKE_PROGRESSIVE
 %token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLKFORM
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
 %token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
@@ -79,15 +79,18 @@ class rsin_driver;
 
 system:
 	| OPTIONS LCB options RCB system
-    | REACTIONS LCB reactionsets RCB system
-    | INITIALCONTEXTS LCB initstates RCB system
-    | CONTEXTENTITIES LCB actionentities RCB system
+  | REACTIONS LCB reactionsets RCB system
+  | INITIALCONTEXTS LCB initstates RCB system
+  | CONTEXTENTITIES LCB actionentities RCB system
 	| CONTEXTAUTOMATON LCB ctxaut RCB system
-    | RSCTLKFORM LCB IDENTIFIER COL rsctlk_form RCB system {
-        driver.addFormRSCTLK(*$3, $5);
-        free($3);
-    }
-    ;
+  {
+    driver.getReactionSystem()->ctxAutFinalise();
+  }
+  | RSCTLKFORM LCB IDENTIFIER COL rsctlk_form RCB system {
+    driver.addFormRSCTLK(*$3, $5);
+    free($3);
+  }
+  ;
 
 options:
 	| options option SEMICOL
@@ -100,6 +103,9 @@ option:
 	| USE_CONCENTRATIONS {
 		driver.useConcentrations();
 	}
+  | MAKE_PROGRESSIVE {
+    driver.makeProgressive();
+  }
 	;
 
 /*
@@ -443,4 +449,3 @@ yy::rsin_parser::error(const yy::rsin_parser::location_type &l, const std::strin
 {
     driver.error(l, m);
 }
-

symrs.cc

@@ -34,12 +34,8 @@ 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();
 }