RS with context automaton (we embed CA with RS)

Makefile

@@ -10,7 +10,7 @@ CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
 #CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
 LDLIBS = $(CUDD_INCLUDE) 
 
-OBJ = rs.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o 
+OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o 
 
 all: main
 

mc.cc

@@ -117,7 +117,7 @@ void ModelChecker::printReachWithSucc(void)
     cleanup();
 }
 
-bool ModelChecker::checkReach(const RctSys::Entities testState)
+bool ModelChecker::checkReach(const Entities testState)
 {
     if (opts->measure)
         opts->ver_time = cpuTime();

mc.hh

@@ -67,7 +67,7 @@ public:
 
     void printReach(void);
     void printReachWithSucc(void);
-    bool checkReach(const RctSys::Entities testState);
+    bool checkReach(const Entities testState);
     bool checkRSCTL(FormRSCTL *form);
     bool checkRSCTLfull(FormRSCTL *form);
     bool checkRSCTLbmc(FormRSCTL *form);

rs.cc

@@ -8,6 +8,11 @@
 
 #include "rs.hh"
 
+RctSys::RctSys(void)
+{
+	ctx_aut = nullptr;
+}
+
 bool RctSys::hasEntity(std::string name)
 {
     if (entities_names.find(name) == entities_names.end())
@@ -40,7 +45,7 @@ std::string RctSys::getEntityName(Entity entityID)
     }
 }
 
-RctSys::Entity RctSys::getEntityID(std::string name)
+Entity RctSys::getEntityID(std::string name)
 {
     if (!hasEntity(name))
     {
@@ -166,52 +171,21 @@ void RctSys::printSystem(void)
     showInitialStates();
     showActionEntities();
     showReactions();
-}
 	
-bool CtxAut::hasState(std::string name)
+	if (ctx_aut != nullptr)
-{
-    if (states_names.find(name) == states_names.end())
-        return false;
-    else
-        return true;
-}
-
-CtxAut::State CtxAut::getStateID(std::string name)
-{
-    if (!hasState(name))
 	{
-        FERROR("No such state: " << name);
+		ctx_aut->printAutomaton();
-    }
-    return states_names[name];
-}
-
-void CtxAut::addState(std::string name)
-{
-    if (!hasState(name))
-    {
-        State new_state_id = states_ids.size();
-
-        VERB_L2("Adding state: " << name << " index=" << new_state_id);
-
-        states_ids.push_back(name);
-        states_names[name] = new_state_id;
 	}
 }
 
-void CtxAut::pushContextEntity(RctSys::Entity entity_id) 
+void RctSys::ctxAutEnable(void)
 {
-	tmpEntities.insert(entity_id);
+	assert(ctx_aut == nullptr);
+	ctx_aut = new CtxAut;
 }
 
-void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) 
+void RctSys::ctxAutAddState(std::string stateName)
 {
-    VERB_L3("Saving transition");
+	assert(ctx_aut != nullptr);
 	
-	Transition new_transition;
-	
-	new_transition.src_state = getStateID(srcStateName);
-	new_transition.ctx = tmpEntities; 
-	tmpEntities.clear();
-	new_transition.dst_state = getStateID(dstStateName);
 }
-

rs.hh

@@ -15,6 +15,8 @@
 #include <vector>
 #include <string>
 #include <cstdlib>
+#include "types.hh"
+#include "ctx_aut.hh"
 #include "macro.hh"
 #include "options.hh"
 #include "memtime.hh"
@@ -26,38 +28,9 @@ class RctSys
 {
 	    friend class SymRS;
 	    friend class SymRSstate;
-	public:
-	    typedef unsigned int Entity;
-	    typedef std::set<Entity> Entities;
-	    struct Reaction {
-	        Entities rctt;
-	        Entities inhib;
-	        Entities prod;
-	    };
-	    typedef std::vector<Reaction> Reactions;
-	    typedef std::vector<std::string> EntitiesByIds;
-	    typedef std::map<std::string, Entity> EntitiesByName;
-	    typedef std::set<Entities> EntitiesSets;
-	private:
-	    Reactions reactions;
-	    EntitiesSets initStates;
-
-	    Entities actionEntities;
-
-	    EntitiesByIds entities_ids;
-	    EntitiesByName entities_names;
-
-	    Entities tmpReactants;
-	    Entities tmpInhibitors;
-	    Entities tmpProducts;
-
-	    Entities tmpState;
-
-	    Entity getEntityID(std::string entityName);
-
-	    Options *opts;
 
 	public:
+		RctSys(void);
 	    void setOptions(Options *opts)
 	    {
 	        this->opts = opts;
@@ -93,40 +66,31 @@ class RctSys
 	    void showInitialStates(void);
 	    void showActionEntities(void);
 	    void printSystem(void);
-};
 
-// Context Automaton
+		void ctxAutEnable(void);		
-class CtxAut
+		void ctxAutAddState(std::string stateName);
-{
-	public:
-	    typedef unsigned int State;
-	    typedef std::vector<std::string> StatesById;
-	    typedef std::map<std::string, State> StatesByName;
-		struct Transition {
-			State src_state;
-			RctSys::Entities ctx;
-			State dst_state;
-		};
-		
-		bool hasState(std::string name);
-		void addState(std::string stateName);
-		State getStateID(std::string name);
-		void addTransition(std::string srcStateName, std::string dstStateName);
-		void pushContextEntity(RctSys::Entity entity_id);	
-	    void setOptions(Options *opts) { this->opts = opts; }
 		
 	private:
+	    Reactions reactions;
+	    EntitiesSets initStates;
+
+	    Entities actionEntities;
+
+		CtxAut *ctx_aut;
+
+	    EntitiesByIds entities_ids;
+	    EntitiesByName entities_names;
+
+	    Entities tmpReactants;
+	    Entities tmpInhibitors;
+	    Entities tmpProducts;
+
+	    Entities tmpState;
+
 	    Options *opts;
-		StatesById states_ids;
-		StatesByName states_names;
-		RctSys::Entities tmpEntities;	
-};
 
-class RctSysWithCtxAut : public RctSys
+	    Entity getEntityID(std::string entityName);
-{
-	// friend class CtxAut;
 
-	CtxAut ctx_aut;
 };
 
 #endif

rsin_driver.cc

@@ -16,8 +16,8 @@ rsin_driver::rsin_driver(RctSys *rs)
 
 void rsin_driver::initialise(void)
 {
-    this->rs = nullptr;
+    rs = nullptr;
-    this->rsctlform = nullptr;
+    rsctlform = nullptr;
 	opts = nullptr;
 	use_ctx_aut = false;
 	use_concentrations = false;
@@ -79,14 +79,11 @@ void rsin_driver::ensureReactionSystemReady(void)
 void rsin_driver::setupReactionSystem(void)
 {
 	assert(rs == nullptr);
-	if (use_ctx_aut)
-	{
-		rs = new RctSysWithCtxAut;
-	}
-	else
-	{
 	rs = new RctSys;
-	}
+	
+	if (use_ctx_aut) VERB("Using RS with CA")
+	else VERB("Using ordinary RS")
+
 	rs->setOptions(opts);
 }
 
@@ -96,3 +93,4 @@ RctSys *rsin_driver::getReactionSystem(void)
 	assert(rs != nullptr);
 	return rs;
 }
+

rsin_driver.hh

@@ -25,13 +25,10 @@ public:
     virtual ~rsin_driver();
 
     //std::map<std::string, int> variables;
-    RctSys *rs;
     FormRSCTL *rsctlform;
     Options *opts;
 	
-	//
+	// options in configuration file:
-	// options in configuration file
-	//
 	bool use_ctx_aut;
 	bool use_concentrations;
 
@@ -49,19 +46,22 @@ public:
     FormRSCTL *getFormRSCTL(void);
 
 	void ensureOptionsAllowed(void);
-	void useContextAutomaton(void)		{ ensureOptionsAllowed(); use_ctx_aut = true; };
+	void useContextAutomaton(void)		{ ensureOptionsAllowed(); use_ctx_aut = true; getReactionSystem()->ctxAutEnable(); };
 	void useConcentrations(void)		{ ensureOptionsAllowed(); use_concentrations = true; };
 	
 	void ensureReactionSystemReady(void);
 	void setupReactionSystem(void);
 	
 	RctSys *getReactionSystem(void);
+	CtxAut *getCtxAut(void);
 
     // Error handling.
     void error(const yy::location &l, const std::string &m);
     void error(const std::string &m);
 	
 private:
+    RctSys *rs;
+
 	void initialise(void);
 };
 

rsin_parser.yy

@@ -91,7 +91,12 @@ options:
 	;
 
 option:
-	| USE_CTX_AUT { } 
+	| USE_CTX_AUT { 
+		driver.useContextAutomaton(); 
+	}
+	| USE_CONCENTRATIONS {
+		driver.useConcentrations();
+	}
 	;
 
 /* 
@@ -190,6 +195,8 @@ ctxaut:
 	;
 
 autstate: IDENTIFIER {
+		driver.getReactionSystem()->ctxAutAddState(*$1);
+		free($1);
 	}
 	;
 

symrs.cc

@@ -8,7 +8,7 @@
 
 #include "symrs.hh"
 
-BDD SymRS::encEntity_raw(RctSys::Entity entity, bool succ) const
+BDD SymRS::encEntity_raw(Entity entity, bool succ) const
 {
     BDD r;
 
@@ -20,7 +20,7 @@ BDD SymRS::encEntity_raw(RctSys::Entity entity, bool succ) const
     return r;
 }
 
-BDD SymRS::encEntitiesConj_raw(const RctSys::Entities &entities, bool succ)
+BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ)
 {
     BDD r = BDD_TRUE;
 
@@ -33,7 +33,7 @@ BDD SymRS::encEntitiesConj_raw(const RctSys::Entities &entities, bool succ)
     return r;
 }
 
-BDD SymRS::encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ)
+BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ)
 {
     BDD r = BDD_FALSE;
 
@@ -46,7 +46,7 @@ BDD SymRS::encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ)
     return r;
 }
 
-BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities)
+BDD SymRS::encStateActEntitiesConj(const Entities &entities)
 {
     BDD r = BDD_TRUE;
 
@@ -62,7 +62,7 @@ BDD SymRS::encStateActEntitiesConj(const RctSys::Entities &entities)
     return r;
 }
 
-BDD SymRS::encStateActEntitiesDisj(const RctSys::Entities &entities)
+BDD SymRS::encStateActEntitiesDisj(const Entities &entities)
 {
     BDD r = BDD_FALSE;
 
@@ -182,7 +182,7 @@ void SymRS::encodeTransitions(void)
         cond.rctt = rs->reactions[i].rctt;
         cond.inhib = rs->reactions[i].inhib;
     
-        for (RctSys::Entities::iterator p = rs->reactions[i].prod.begin();
+        for (Entities::iterator p = rs->reactions[i].prod.begin();
                 p != rs->reactions[i].prod.end(); ++p)
         {
             dr[*p].push_back(cond);
@@ -289,7 +289,7 @@ void SymRS::encodeTransitions(void)
     VERB("Reactions ready");
 }
 
-BDD SymRS::getEncState(const RctSys::Entities &entities)
+BDD SymRS::getEncState(const Entities &entities)
 {
     assert(0);
     //BDD state = compState(encEntitiesConj(rs->initState));

symrs.hh

@@ -14,6 +14,7 @@
 #include <map>
 #include <cassert>
 #include "cudd.hh"
+#include "types.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
 #include "rs.hh"
@@ -36,11 +37,11 @@ class SymRS
     Options *opts;
 
     struct ReactionCond {
-        RctSys::Entities rctt;
+        Entities rctt;
-        RctSys::Entities inhib;
+        Entities inhib;
     };
     typedef vector<ReactionCond> ReactionConds;
-    typedef map<RctSys::Entity,ReactionConds> DecompReactions;
+    typedef map<Entity,ReactionConds> DecompReactions;
     typedef std::vector<int> StateEntityToAction; 
 
     StateEntityToAction stateToAct;
@@ -62,33 +63,33 @@ class SymRS
     unsigned int totalStateVars;
     unsigned int totalActions;
 
-    BDD encEntity_raw(RctSys::Entity entity, bool succ) const;
+    BDD encEntity_raw(Entity entity, bool succ) const;
-    BDD encEntity(RctSys::Entity entity) const {
+    BDD encEntity(Entity entity) const {
         return encEntity_raw(entity, false);
     }
-    BDD encActEntity(RctSys::Entity entity) const {
+    BDD encActEntity(Entity entity) const {
 		assert(entity < pv_act->size());
         return (*pv_act)[entity];
     }
-    BDD encEntitySucc(RctSys::Entity entity) const {
+    BDD encEntitySucc(Entity entity) const {
         return encEntity_raw(entity, true); 
     }
-    BDD encEntitiesConj_raw(const RctSys::Entities &entities, bool succ);
+    BDD encEntitiesConj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesConj(const RctSys::Entities &entities) {
+    BDD encEntitiesConj(const Entities &entities) {
         return encEntitiesConj_raw(entities, false);
     }
-    BDD encEntitiesConjSucc(const RctSys::Entities &entities) {
+    BDD encEntitiesConjSucc(const Entities &entities) {
         return encEntitiesConj_raw(entities, true);
     }
-    BDD encEntitiesDisj_raw(const RctSys::Entities &entities, bool succ);
+    BDD encEntitiesDisj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesDisj(const RctSys::Entities &entities) {
+    BDD encEntitiesDisj(const Entities &entities) {
         return encEntitiesDisj_raw(entities, false);
     }
-    BDD encEntitiesDisjSucc(const RctSys::Entities &entities) {
+    BDD encEntitiesDisjSucc(const Entities &entities) {
         return encEntitiesDisj_raw(entities, true);
     }
-    BDD encStateActEntitiesConj(const RctSys::Entities &entities);
+    BDD encStateActEntitiesConj(const Entities &entities);
-    BDD encStateActEntitiesDisj(const RctSys::Entities &entities);
+    BDD encStateActEntitiesDisj(const Entities &entities);
 
     /**
      * @brief Complements an encoding of a given state by negating all the variables that are not set to true
@@ -134,7 +135,7 @@ public:
     BDD *getEncPVact_E(void) { return pv_act_E; }
     vector<BDD> *getEncPartTrans(void) { return partTrans; }
     BDD *getEncMonoTrans(void) { return monoTrans; }
-    BDD getEncState(const RctSys::Entities &entities);
+    BDD getEncState(const Entities &entities);
     BDD *getEncInitStates(void) { return initStates; }
     Cudd *getCuddMgr(void) { return cuddMgr; }
     unsigned int getTotalStateVars(void) { return totalStateVars; }