Initialisation of BDD variables

Makefile

@@ -44,7 +44,7 @@ rsin_parser.lex.cc: rsin_parser.ll
 	mv lex.yy.c rsin_parser.lex.cc
 
 style:
-	astyle --max-code-length=78 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh	
+	astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh	
 
 commit: style
 	git commit -a

rs.hh

@@ -103,6 +103,11 @@ class RctSys
       return ctx_aut != nullptr;
     }
 
+    size_t getNumberOfProcesses(void)
+    {
+      return processes_ids.size();
+    }
+
   private:
     Reactions reactions; // TODO: to be removed later
     ReactionsForProc proc_reactions;

symrs.cc

@@ -10,13 +10,19 @@ SymRS::SymRS(RctSys *rs, Options *opts)
 {
   this->rs = rs;
   this->opts = opts;
-  totalRctSysStateVars = rs->getEntitiesSize();
+
+  mapProcEntities();
+
+  // TODO: remove
+  totalActions = 0;
+
+  totalRctSysStateVars = getTotalProductVariables();
   totalReactions = rs->getReactionsSize();
-  totalActions = rs->getActionsSize();
+  totalCtxEntities = getTotalCtxEntitiesVariables();
 
   totalCtxAutStateVars = getCtxAutStateEncodingSize();
-
   totalStateVars = totalRctSysStateVars + totalCtxAutStateVars;
+  numberOfProc = rs->getNumberOfProcesses();
 
   partTrans = nullptr;
   monoTrans = nullptr;
@@ -39,8 +45,6 @@ void SymRS::encode(void)
 
   mapStateToAct();
 
-  mapProcEntities();
-
   initBDDvars();
 
   if (usingContextAutomaton()) {
@@ -78,6 +82,188 @@ LocalIndicesForProcEntities SymRS::buildLocalEntitiesMap(
   return ent_map;
 }
 
+void SymRS::initBDDvars(void)
+{
+  VERB("Initialising CUDD");
+
+  cuddMgr = new Cudd(0, 0);
+
+  VERB("Preparing BDD variables");
+
+  // used for bddVar
+  unsigned int bdd_var_idx = 0;
+
+  // used for pv, pv_succ
+  unsigned int global_state_idx = 0;
+
+  // ----------------------------------------------------------
+  //                        Global state
+  // ----------------------------------------------------------
+  //
+  //  Variables for reaction system with CA (if used)
+  //
+
+  pv = new BDDvec(totalStateVars);
+  pv_succ = new BDDvec(totalStateVars);
+  pv_E = new BDD(BDD_TRUE);
+  pv_succ_E = new BDD(BDD_TRUE);
+
+  // ----------------------------------------------------------
+  //                       Distributed RS
+  // ----------------------------------------------------------
+
+  // // Reaction system (no actions, no CA)
+  // pv_rs = new BDDvec(totalRctSysStateVars);
+  // pv_rs_succ = new BDDvec(totalRctSysStateVars);
+  // pv_rs_E = new BDD(BDD_TRUE);
+  // pv_rs_succ_E = new BDD(BDD_TRUE);
+
+  pv_drs = new vector<BDDvec>(numberOfProc);
+  pv_drs_succ = new vector<BDDvec>(numberOfProc);
+
+  pv_drs_flat = new BDDvec(totalRctSysStateVars);
+  pv_drs_flat_succ = new BDDvec(totalRctSysStateVars);
+
+  pv_drs_flat_E = new BDD(BDD_TRUE);
+  pv_drs_flat_succ_E = new BDD(BDD_TRUE);
+
+  VERB_LN(3, "DRS processing");
+
+  unsigned int drs_flat_index = 0;
+
+  for (const auto &proc_ent : usedProducts) {
+
+    auto proc_id = proc_ent.first;
+    auto entities_count = proc_ent.second.size();
+
+    //
+    // The order of entities and their correspondence to the
+    // correct entities in pv (global) does not matter here.
+    //
+    // The correspondence is established in the methods
+    // returning BDD variables (encoding) of the individual
+    // enties.
+    //
+    // We only need to make sure we have the correct number of
+    // variables that are going to be used in the encoding.
+    //
+    // For efficiency, we do not introduce BDD variables for
+    // entites that are never produced in a given local component.
+    // Instead, we only select those that are. We apply the same
+    // strategy to product entities and context entities.
+    //
+
+    // First, we need to adjust the sizes of all the nested vectors
+    (*pv_drs)[proc_id].resize(entities_count);
+    (*pv_drs_succ)[proc_id].resize(entities_count);
+
+    for (unsigned int i = 0; i < entities_count; ++i) {
+
+      assert(drs_flat_index < totalRctSysStateVars);
+      assert(global_state_idx < totalStateVars);
+      assert(proc_id < numberOfProc);
+      assert(i < rs->getEntitiesSize());
+
+      // Variables for each individual process/component
+      (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
+      (*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
+
+      // The DRS part of the system (flattened): these vars do not include CA
+      (*pv_drs_flat)[drs_flat_index] = (*pv_drs)[proc_id][i];
+      (*pv_drs_flat_succ)[drs_flat_index] = (*pv_drs_succ)[proc_id][i];
+      ++drs_flat_index;
+
+      // Variables used for the global states
+      (*pv)[global_state_idx] = (*pv_drs)[proc_id][i];
+      (*pv_succ)[global_state_idx] = (*pv_drs_succ)[proc_id][i];
+      ++global_state_idx;
+    }
+  }
+
+  // ----------------------------------------------------------
+  //                      Context Automaton
+  // ----------------------------------------------------------
+
+  if (usingContextAutomaton()) {
+    VERB("Context automaton variables");
+
+    pv_ca = new BDDvec(totalCtxAutStateVars);
+    pv_ca_succ = new BDDvec(totalCtxAutStateVars);
+    pv_ca_E = new BDD(BDD_TRUE);
+    pv_ca_succ_E = new BDD(BDD_TRUE);
+
+    for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) {
+      (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++);
+      (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
+      *pv_ca_E *= (*pv_ca)[i];
+      *pv_ca_succ_E *= (*pv_ca_succ)[i];
+
+      (*pv)[global_state_idx] = (*pv_ca)[i];
+      (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i];
+      ++global_state_idx;
+    }
+  }
+
+  // ----------------------------------------------------------
+  //                Enabledness of processes
+  // ----------------------------------------------------------
+  //
+  //  These variables indicate which process is
+  //  allowed to perform action
+  //
+  pv_proc_enab = new BDDvec(numberOfProc);
+
+  for (unsigned int i = 0; i < numberOfProc; ++i) {
+    (*pv_proc_enab)[i] = cuddMgr->bddVar(bdd_var_idx++);
+  }
+
+  // Actions/Contexts
+  pv_act = new BDDvec(totalActions);
+  pv_act_E = new BDD(BDD_TRUE);
+
+  // TODO
+  // Actions need also per-process PV and flattened PV
+
+  for (unsigned int i = 0; i < totalActions; ++i) {
+    (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++);
+    *pv_act_E *= (*pv_act)[i];
+  }
+
+  // Quantification BDDs
+
+  *pv_E = *pv_rs_E;
+  *pv_succ_E = *pv_rs_succ_E;
+
+  if (usingContextAutomaton()) {
+    *pv_E *= *pv_ca_E;
+    *pv_succ_E *= *pv_ca_succ_E;
+  }
+
+  VERB("All BDD variables ready");
+}
+
+size_t SymRS::getTotalProductVariables(void)
+{
+  size_t total = 0;
+
+  for (const auto &it : usedProducts) {
+    total += it.second.size();
+  }
+
+  return total;
+}
+
+size_t SymRS::getTotalCtxEntitiesVariables(void)
+{
+  size_t total = 0;
+
+  for (const auto &it : usedCtxEntities) {
+    total += it.second.size();
+  }
+
+  return total;
+}
+
 void SymRS::mapProcEntities(void)
 {
   //
@@ -256,7 +442,7 @@ void SymRS::printDecodedRctSysStates(const BDD &states)
     cout << decodedRctSysStateToStr(t) << endl;
 
     if (opts->verbose > 9) {
-      t.PrintMinterm();
+      BDD_PRINT(t);
       cout << endl;
     }
 
@@ -264,86 +450,6 @@ void SymRS::printDecodedRctSysStates(const BDD &states)
   }
 }
 
-void SymRS::initBDDvars(void)
-{
-  VERB("Initialising CUDD");
-
-  cuddMgr = new Cudd(0, 0);
-
-  VERB("Preparing BDD variables");
-
-  // used for bddVar
-  unsigned int bdd_var_idx = 0;
-
-  // used for pv, pv_succ
-  unsigned int global_state_idx = 0;
-
-  // Variables for reaction system with CA (if used)
-  pv = new vector<BDD>(totalStateVars);
-  pv_succ = new vector<BDD>(totalStateVars);
-  pv_E = new BDD(BDD_TRUE);
-  pv_succ_E = new BDD(BDD_TRUE);
-
-  // Reaction system (no actions, no CA)
-  pv_rs = new vector<BDD>(totalRctSysStateVars);
-  pv_rs_succ = new vector<BDD>(totalRctSysStateVars);
-  pv_rs_E = new BDD(BDD_TRUE);
-  pv_rs_succ_E = new BDD(BDD_TRUE);
-
-  for (unsigned int i = 0; i < totalRctSysStateVars; ++i) {
-    (*pv_rs)[i] = cuddMgr->bddVar(bdd_var_idx++);
-    (*pv_rs_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
-    *pv_rs_E *= (*pv_rs)[i];
-    *pv_rs_succ_E *= (*pv_rs_succ)[i];
-
-    (*pv)[global_state_idx] = (*pv_rs)[i];
-    (*pv_succ)[global_state_idx] = (*pv_rs_succ)[i];
-    ++global_state_idx;
-  }
-
-  // CA
-  if (usingContextAutomaton()) {
-    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);
-
-    for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) {
-      (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++);
-      (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
-      *pv_ca_E *= (*pv_ca)[i];
-      *pv_ca_succ_E *= (*pv_ca_succ)[i];
-
-      (*pv)[global_state_idx] = (*pv_ca)[i];
-      (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i];
-      ++global_state_idx;
-    }
-  }
-
-  // Actions/Contexts
-  pv_act = new vector<BDD>(totalActions);
-  pv_act_E = new BDD(BDD_TRUE);
-
-  for (unsigned int i = 0; i < totalActions; ++i) {
-    (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++);
-    *pv_act_E *= (*pv_act)[i];
-  }
-
-  // Quantification BDDs
-
-  *pv_E = *pv_rs_E;
-  *pv_succ_E = *pv_rs_succ_E;
-
-  if (usingContextAutomaton()) {
-    *pv_E *= *pv_ca_E;
-    *pv_succ_E *= *pv_ca_succ_E;
-  }
-
-  VERB("All BDD variables ready");
-}
-
 void SymRS::encodeTransitions(void)
 {
   DecompReactions dr;
@@ -365,7 +471,7 @@ void SymRS::encodeTransitions(void)
 
   if (opts->part_tr_rel) {
     VERB("Using partitioned transition relation encoding");
-    partTrans = new vector<BDD>(totalRctSysStateVars);
+    partTrans = new BDDvec(totalRctSysStateVars);
   }
   else {
     VERB("Using monolithic transition relation encoding");
@@ -575,7 +681,7 @@ size_t SymRS::getCtxAutStateEncodingSize(void)
 BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const
 {
   // select appropriate BDD vector
-  vector<BDD> *enc_vec;
+  BDDvec *enc_vec;
 
   if (succ) {
     enc_vec = pv_ca_succ;

symrs.hh

@@ -35,11 +35,11 @@ class SymRS
   public:
     SymRS(RctSys *rs, Options *opts);
 
-    vector<BDD> *getEncPV(void)
+    BDDvec *getEncPV(void)
     {
       return pv;
     }
-    vector<BDD> *getEncPVsucc(void)
+    BDDvec *getEncPVsucc(void)
     {
       return pv_succ;
     }
@@ -55,7 +55,7 @@ class SymRS
     {
       return pv_act_E;
     }
-    vector<BDD> *getEncPartTrans(void)
+    BDDvec *getEncPartTrans(void)
     {
       return partTrans;
     }
@@ -144,7 +144,7 @@ class SymRS
      *
      * @return Returns a vector of BDDs
      */
-    vector<BDD> *getEncCtxAutPV(void)
+    BDDvec *getEncCtxAutPV(void)
     {
       return pv_ca;
     }
@@ -154,7 +154,7 @@ class SymRS
      *
      * @return Returns a vector of BDDs
      */
-    vector<BDD> *getEncCtxAutPVsucc(void)
+    BDDvec *getEncCtxAutPVsucc(void)
     {
       return pv_ca_succ;
     }
@@ -200,48 +200,62 @@ class SymRS
     Cudd *cuddMgr;
     Options *opts;
 
-    // Mapping: entity ID -> action/context entity ID
+    StateEntityToAction
-    StateEntityToAction stateToAct;
+    stateToAct; /*!< Mapping: entity ID -> action/context entity ID */
 
-    BDD *initStates;
+    BDD *initStates;              /*!< BDD with initial states encoded */
 
-    vector<BDD> *pv;
+    BDDvec *pv;                   /*!< PVs for the global state (all the variables, flat) */
-    vector<BDD> *pv_succ;
+    BDDvec *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
 
-    vector<BDD> *pv_rs;
+    BDDvec *pv_proc_enab;         /*!< Variables indicating if a process is enabled */
-    vector<BDD> *pv_rs_succ;
+
+    BDDvec *pv_rs;
+    BDDvec *pv_rs_succ;
+
     BDD *pv_rs_E;
     BDD *pv_rs_succ_E;
 
-    vector<BDD> *partTrans;
+    vector<BDDvec> *pv_drs;       /*!< PVs for the product part of state
+                                       (per DRS process) */
+    vector<BDDvec> *pv_drs_succ;  /*!< PVs for the product (successor)
+                                       part of state (per DRS process) */
+
+    BDDvec *pv_drs_flat;          /*!< PVs for the DRS product part of state (flat) */
+    BDDvec *pv_drs_flat_succ;     /*!< PVs for the DRS product (successor) part of state (flat) */
+
+    BDDvec *partTrans;
 
     BDD *monoTrans;
 
     // Context automaton
-    vector<BDD> *pv_ca;
+    BDDvec *pv_ca;
-    vector<BDD> *pv_ca_succ;
+    BDDvec *pv_ca_succ;
     BDD *pv_ca_E;
     BDD *pv_ca_succ_E;
     BDD *tr_ca;
 
-    vector<BDD> *pv_act;
+    BDDvec *pv_act;
     BDD *pv_act_E;
 
+    unsigned int numberOfProc;         /*!< The number of DRS processes */
     unsigned int totalStateVars;
     unsigned int totalReactions;
-    unsigned int totalRctSysStateVars;
+    unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */
+    unsigned int totalCtxEntities;     /*!< Total number of different process-context entities used */
     unsigned int totalActions;
     unsigned int totalCtxAutStateVars;
 
-    EntitiesForProc usedProducts;
+    EntitiesForProc usedProducts;     /*!< Entities used in products (per process) */
-    EntitiesForProc usedCtxEntities;
+    EntitiesForProc usedCtxEntities;  /*!< Entities used in context sets (per process) */
 
-    // Local indices for each entity (per process):
+    LocalIndicesForProcEntities prod_ent_local_idx; /*!< Local indices for each entity (per process): product entities */
-    // separete for state/product entities and context
+    LocalIndicesForProcEntities ctx_ent_local_idx;  /*!< Local indices for each entity (per process): context entities */
-    LocalIndicesForProcEntities prod_ent_local_idx;
+
-    LocalIndicesForProcEntities ctx_ent_local_idx;
+    size_t getTotalProductVariables(void);
+    size_t getTotalCtxEntitiesVariables(void);
 
     BDD encEntity_raw(Entity entity, bool succ) const;
     BDD encEntity(Entity entity) const

types.hh

@@ -13,6 +13,9 @@
 #include <map>
 #include <vector>
 #include <string>
+#include "cudd.hh"
+
+typedef std::vector<BDD> BDDvec;
 
 typedef unsigned int Entity;
 typedef std::set<Entity> Entities;