Context automaton state encoding

ctx_aut.cc

@@ -57,6 +57,12 @@ void CtxAut::setInitState(std::string name)
 	init_state_defined = true;
 }
 
+State CtxAut::getInitState(void)
+{
+	assert(init_state_defined);
+	return init_state_id;
+}
+
 void CtxAut::printAutomaton(void)
 {
 	showStates();

ctx_aut.hh

@@ -32,6 +32,7 @@ class CtxAut
 		bool hasState(std::string name);
 		void addState(std::string stateName);
 		void setInitState(std::string stateName);
+		State getInitState(void);
 		State getStateID(std::string name);
 		std::string getStateName(State state_id);
 		void printAutomaton(void);

mc.cc

@@ -21,7 +21,10 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
     //
 	// Transition relations
 	//
-	// If we use trp, then trm is going to be nullptr (same for trm)
+	//	trp -- partitioned TR
+	//	trm -- monolithic TR
+	//
+	// If we use trp, then trm is nullptr (same for trm)
 	//
 	trp = srs->getEncPartTrans();
     if (trp == nullptr) 
@@ -32,10 +35,10 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
     
 	if (srs->usingContextAutomaton())
 	{
-		ca_init_state = srs->getEncCA_InitState();
+		ca_init_state = srs->getEncCtxAutInitState();
-		pv_ca = srs->getEncCA_PV();
+		pv_ca = srs->getEncCtxAutPV();
-		pv_ca_succ = srs->getEncCA_PVsucc();
+		pv_ca_succ = srs->getEncCtxAutPVsucc();
-		ca_tr = srs->getEncCA_Trans();
+		ca_tr = srs->getEncCtxAutTrans();
 	}
 	
 	// Initialise the set of reachable states

rs.cc

@@ -130,7 +130,6 @@ void RctSys::commitInitState(void)
     tmpState.clear();
 }
 
-
 void RctSys::addActionEntity(std::string entityName)
 {
     if (!hasEntity(entityName))
@@ -138,6 +137,12 @@ void RctSys::addActionEntity(std::string entityName)
     actionEntities.insert(getEntityID(entityName));
 }
 
+void RctSys::addActionEntity(Entity entity)
+{
+	if (!isActionEntity(entity))
+	    actionEntities.insert(entity);
+}
+
 bool RctSys::isActionEntity(Entity entity)
 {
     if (actionEntities.count(entity) > 0)
@@ -211,7 +216,17 @@ void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateN
 void RctSys::ctxAutPushNamedContextEntity(std::string entityName)
 {
 	assert(ctx_aut != nullptr);
+	
 	Entity entity_id = getEntityID(entityName);
+
+	//
+	// We mark the entity as an action entity
+	//
+	// 	This step is required to ensure the minimal number of
+	//  BDD variables used in the encoding of the context sets
+	//
+	addActionEntity(entity_id);
+	
 	ctx_aut->pushContextEntity(entity_id);
 }
 

rs.hh

@@ -52,6 +52,7 @@ class RctSys
 	    void pushStateEntity(std::string entityName);
 	    void commitInitState(void);
 	    void addActionEntity(std::string entityName);
+	    void addActionEntity(Entity entity);
 	    bool isActionEntity(Entity entity);
 	    void resetInitStates(void) {
 	        initStates.clear();

symrs.cc

@@ -51,8 +51,11 @@ BDD SymRS::encStateActEntitiesConj(const Entities &entities)
     {
         BDD state_act = encEntity(*entity);
         int actEntity;
+		
+		// if entity is also an aciton entity, we include it in the encoding
         if ((actEntity = getMappedStateToActID(*entity)) >= 0)
             state_act += encActEntity(actEntity);
+        
 		r *= state_act;
     }
 
@@ -67,8 +70,11 @@ BDD SymRS::encStateActEntitiesDisj(const Entities &entities)
     {
         BDD state_act = encEntity(*entity);
         int actEntity;
+
+		// if entity is also an aciton entity, we include it in the encoding
         if ((actEntity = getMappedStateToActID(*entity)) >= 0)
             state_act += encActEntity(actEntity);
+		
         r += state_act;
     }
 
@@ -132,40 +138,61 @@ void SymRS::printDecodedStates(const BDD &states)
 
 void SymRS::initBDDvars(void)
 {
+	VERB("Initialising CUDD");
+	
     cuddMgr = new Cudd(0,0);
 
-    //RctSys::Entities aa = rs->actionEntities;
-
     VERB("Preparing BDD variables");
+	
     pv = new vector<BDD>(totalStateVars);
     pv_succ = new vector<BDD>(totalStateVars);
     pv_act = new vector<BDD>(totalActions);
-    pv_E = new BDD(cuddMgr->bddOne());
+    pv_E = new BDD(BDD_TRUE);
-    pv_succ_E = new BDD(cuddMgr->bddOne());
+    pv_succ_E = new BDD(BDD_TRUE);
-    pv_act_E = new BDD(cuddMgr->bddOne());
+    pv_act_E = new BDD(BDD_TRUE);
 
-    //unsigned int j = 0;
     for (unsigned int i = 0; i < totalStateVars; ++i)
     {
         (*pv)[i] = cuddMgr->bddVar(i*2);
         (*pv_succ)[i] = cuddMgr->bddVar((i*2)+1);
-        //(*pv_act)[i] = cuddMgr->bddVar(totalStateVars*2+i);
 
         *pv_E *= (*pv)[i];
         *pv_succ_E *= (*pv_succ)[i];
-        
-        //if (rs->actionEntities.find(i) == rs->actionEntities.end())
-        //    (*pv_noact)[j++] = cuddMgr->bddVar(i*2);
     }
 
     unsigned int offset = totalStateVars * 2;
+	
     for (unsigned int i = 0; i < totalActions; ++i)
     {
         (*pv_act)[i] = cuddMgr->bddVar(offset+i);
         *pv_act_E *= (*pv_act)[i];
     }
 
-    VERB("Variables ready");
+	offset += totalActions;
+
+	VERB("Context automaton variables");
+
+	pv_ca = new vector<BDD>(totalCtxAutStateVars);
+	pv_ca_succ = new vector<BDD>(totalCtxAutStateVars);
+	pv_ca_E = new BDD(BDD_TRUE);
+	pv_ca_succ_E = new BDD(BDD_TRUE);
+	
+	//
+	// BDD variables for encoding local states of context automaton
+	//
+	unsigned int base_index = offset;
+	for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
+	{
+		(*pv_ca)[i] = cuddMgr->bddVar(base_index);
+		(*pv_ca_succ)[i] = cuddMgr->bddVar(base_index+1);
+		
+		*pv_ca_E *= (*pv_ca)[i];
+		*pv_ca_succ_E *= (*pv_ca_succ)[i];
+	
+		base_index += 2;
+	}
+
+    VERB("All BDD variables ready");
 }
 
 void SymRS::encodeTransitions(void)
@@ -246,43 +273,6 @@ void SymRS::encodeTransitions(void)
 
     }
 
-    /*
-    for (unsigned int p = 0; p < totalStateVars; ++p) // we iterate through products
-    {
-        RctSys::Entities::iterator ai = rs->actionEntities.find(p);
-        DecompReactions::iterator di;
-
-        if ((di = dr.find(p)) == dr.end())
-        {
-            (*partTrans)[p] = cuddMgr->bddOne();
-            if (ai == rs->actionEntities.end()) 
-                (*partTrans)[p] *= !encEntitySucc(p);
-        }
-        else
-        {
-            BDD conditions = cuddMgr->bddZero();
-
-            for (unsigned int j = 0; j < di->second.size(); ++j)
-            {
-                conditions += encEntitiesConj(di->second[j].rctt) * !encEntitiesDisj(di->second[j].inhib);
-            }
-
-            (*partTrans)[p] = conditions * encEntitySucc(p);
-
-            if (ai == rs->actionEntities.end())
-            {
-                // not an action entity
-                (*partTrans)[p] += !conditions * !encEntitySucc(p);
-            }
-            else
-            {
-                // action entity
-                (*partTrans)[p] += cuddMgr->bddOne(); //(encEntitySucc(p) + !encEntitySucc(p));
-            }
-        }
-    }
-    */
-
     VERB("Reactions ready");
 }
 
@@ -362,11 +352,12 @@ void SymRS::mapStateToAct(void)
             stateToAct.push_back(-1);
         }
     }
-    if (opts->verbose > 9)
+	const unsigned int verbosity_level = 9;
+    if (opts->verbose > verbosity_level)
     {
         for (unsigned int i = 0; i < stateToAct.size(); ++i)
         {
-            cout << "ii VERBOSE(9): stateToAct[" << i << "] = " << stateToAct[i] << endl;
+            cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << stateToAct[i] << endl;
         }
     }
 }
@@ -408,22 +399,64 @@ BDD SymRS::encActStrEntity(std::string name) const
 	}
 }
 
-BDD *SymRS::getEncCA_InitState(void)
+size_t SymRS::getCtxAutStateEncodingSize(void)
+{
+    size_t bitCount = 0;
+    size_t bitCountMaxVal = 1;
+    size_t numStates = rs->ctx_aut->statesCount();
+    while (bitCountMaxVal <= numStates)
+    {
+        bitCount++;
+        bitCountMaxVal *= 2;
+    }
+    return bitCount;
+}
+
+BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const
+{
+	// select appropriate BDD vector
+	vector<BDD> *enc_vec;
+    if (succ)
+        enc_vec = pv_ca_succ;
+    else
+        enc_vec = pv_ca;
+
+    BDD r;
+	State val = state_id;
+
+	for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
+	{
+		if (val != 0)
+		{
+			if (val % 2 == 1)
+				r *= (*enc_vec)[i];
+			else
+				r *= !(*enc_vec)[i];
+			val /= 2;
+		}
+		else
+			r *= !(*enc_vec)[i];
+	}
+
+    return r;
+}
+
+BDD *SymRS::getEncCtxAutInitState(void)
 {
 	return new BDD(BDD_TRUE);
 }
 
-vector<BDD> *SymRS::getEncCA_PV(void)
+vector<BDD> *SymRS::getEncCtxAutPV(void)
 {
 	return new vector<BDD>();
 }
 
-vector<BDD> *SymRS::getEncCA_PVsucc(void)
+vector<BDD> *SymRS::getEncCtxAutPVsucc(void)
 {
 	return new vector<BDD>();
 }
 
-BDD *SymRS::getEncCA_Trans(void)
+BDD *SymRS::getEncCtxAutTrans(void)
 {
 	return new BDD(BDD_TRUE);
 }

symrs.hh

@@ -36,24 +36,35 @@ class SymRS
     Cudd *cuddMgr;
     Options *opts;
 
+	// Mapping: entity ID -> action/context entity ID
     StateEntityToAction stateToAct;
 
     BDD *initStates;
+	
     vector<BDD> *pv;
     vector<BDD> *pv_act;
     vector<BDD> *pv_succ;
+	
+	// BDDs for quantification
     BDD *pv_E;
     BDD *pv_act_E;
     BDD *pv_succ_E;
 
-    vector<BDD> *pv_noact;
     vector<BDD> *partTrans;
 
     BDD *monoTrans;
 
+	// Context automaton
+	vector<BDD> *pv_ca;
+	vector<BDD> *pv_ca_succ;
+	BDD *pv_ca_E;
+	BDD *pv_ca_succ_E;
+
     unsigned int totalReactions;
     unsigned int totalStateVars;
     unsigned int totalActions;
+	unsigned int totalCtxAutStateVars;
+	
 
     BDD encEntity_raw(Entity entity, bool succ) const;
     BDD encEntity(Entity entity) const {
@@ -106,6 +117,8 @@ class SymRS
 
     int getMappedStateToActID(int stateID) const { assert(stateID < static_cast<int>(totalStateVars)); return stateToAct[stateID]; }
 
+	size_t getCtxAutStateEncodingSize(void);
+	
 public:
     SymRS(RctSys *rs, Options *opts)
     {
@@ -114,6 +127,7 @@ public:
         totalStateVars = rs->getEntitiesSize();
         totalReactions = rs->getReactionsSize();
         totalActions = rs->getActionsSize();
+		totalCtxAutStateVars = getCtxAutStateEncodingSize();
 
         partTrans = nullptr;
         monoTrans = nullptr;
@@ -140,11 +154,13 @@ public:
 	
 	bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; }
 	
-	BDD *getEncCA_InitState(void);
+	BDD encCtxAutState_raw(State state_id, bool succ) const;
-	vector<BDD> *getEncCA_PV(void);
+	BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); }
-	vector<BDD> *getEncCA_PVsucc(void);
+	BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); }
-	BDD *getEncCA_Trans(void);
+	BDD *getEncCtxAutInitState(void);
-	
+	vector<BDD> *getEncCtxAutPV(void);
+	vector<BDD> *getEncCtxAutPVsucc(void);
+	BDD *getEncCtxAutTrans(void);
 };
 
 #endif