Context encoding and complementation

rs.hh

@@ -105,7 +105,7 @@ class RctSys
     }
 
   private:
-    // Reactions reactions; // TODO: to be removed later
+
     ReactionsForProc proc_reactions;
 
     EntitiesSets initStates;

symrs.cc

@@ -470,16 +470,24 @@ BDD SymRS::encEntityCondition(Process proc_id, Entity entity_id)
   return r;
 }
 
-BDD SymRS::encActEntitiesConj(const Entities &entities)
+BDD SymRS::encContext(const EntitiesForProc &proc_entities)
 {
-  assert(0);
   BDD r = BDD_TRUE;
-  /*
+
+  for (const auto &pe : proc_entities) {
+    auto proc_id = pe.first;
+    auto entities = pe.second;
+
     for (const auto &entity : entities) {
-    Entity actEntity = getMappedStateToActID(entity);
+      r *= encCtxEntity(proc_id, entity);
-    r *= encActEntity(actEntity);
     }
-  */
+
+    // This check is not really requires. Just to be sure...
+    if (entities.size() > 0) {
+      r *= encProcEnabled(proc_id);
+    }
+  }
+
   return r;
 }
 
@@ -499,12 +507,17 @@ BDD SymRS::compState(const BDD &state) const
 
 BDD SymRS::compContext(const BDD &context) const
 {
-  assert(0);
   BDD c = context;
 
-  for (unsigned int i = 0; i < totalActions; ++i) {
+  for (const auto &var : *pv_ctx) {
-    if (!(*pv_act)[i] * context != cuddMgr->bddZero()) {
+    if (!var * context != cuddMgr->bddZero()) {
-      c *= !(*pv_act)[i];
+      c *= !var;
+    }
+  }
+
+  for (const auto &var : *pv_proc_enab) {
+    if (!var * context != cuddMgr->bddZero()) {
+      c *= !var;
     }
   }
 
@@ -797,10 +810,11 @@ void SymRS::encodeCtxAutTrans(void)
             << " -> " << rs->ctx_aut->getStateName(t.dst_state));
     BDD enc_src = encCtxAutState(t.src_state);
     BDD enc_dst = encCtxAutStateSucc(t.dst_state);
-    // assert(0); // enc_ctx
+    BDD enc_ctx = compContext(encContext(t.ctx));
-    BDD enc_ctx = BDD_FALSE; //compContext(encActEntitiesConj(t.ctx));
 
-    *tr_ca += enc_src * enc_ctx * enc_dst;
+    BDD new_trans = enc_src * enc_ctx * enc_dst;
+
+    *tr_ca += new_trans;
   }
 }
 

symrs.hh

@@ -236,7 +236,7 @@ class SymRS
     BDD *pv_ca_succ_E;
     BDD *tr_ca;
 
-    BDDvec *pv_ctx;
+    BDDvec *pv_ctx;               /*!< Flat */
     BDD *pv_ctx_E;
     vector<BDDvec> *pv_proc_ctx;
     BDDvec *pv_proc_ctx_E;
@@ -249,7 +249,7 @@ class SymRS
     unsigned int numberOfProc;         /*!< The number of DRS processes */
     unsigned int totalStateVars;
     unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */
-    unsigned int totalCtxEntities;     /*!< Total number of different process-context entities used */
+    unsigned int totalCtxEntities;     /*!< Total number of different (process,context) entities used */
     unsigned int totalActions;
     unsigned int totalCtxAutStateVars;
 
@@ -309,7 +309,7 @@ class SymRS
 
     BDD encEntityCondition(Process proc_id, Entity entity_id);
 
-    BDD encActEntitiesConj(const Entities &entities);
+    BDD encContext(const EntitiesForProc &proc_entities);
 
     /**
      * @brief Complements an encoding of a given state by negating all the variables that are not set to true