Working DRS with one process

mc.cc

@@ -16,7 +16,15 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
   pv_succ = srs->getEncPVsucc();
   pv_E = srs->getEncPV_E();
   pv_succ_E = srs->getEncPVsucc_E();
-  pv_act_E = srs->getEncPVact_E();
+  pv_ctx_E = srs->getEncPVctx_E();
+  pv_proc_enab_E = srs->getEncPVproc_enab_E();
+
+  assert(pv != nullptr);
+  assert(pv_succ != nullptr);
+  assert(pv_E != nullptr);
+  assert(pv_succ_E != nullptr);
+  assert(pv_ctx_E != nullptr);
+  assert(pv_proc_enab_E != nullptr);
 
   //
   // Transition relations
@@ -69,10 +77,12 @@ inline BDD ModelChecker::getSucc(const BDD &states)
   }
   else {
     q *= states * *trm;
+    BDD_PRINT(q);
   }
 
   q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
-  q = q.ExistAbstract(*pv_act_E);
+  q = q.ExistAbstract(*pv_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
 
   return q;
 }
@@ -93,7 +103,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
   }
 
   q = q.ExistAbstract(*pv_succ_E);
-  q = q.ExistAbstract(*pv_act_E);
+  q = q.ExistAbstract(*pv_ctx_E);
   return q;
 }
 
@@ -113,7 +123,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
   }
 
   q = q.ExistAbstract(*pv_succ_E);
-  q = q.ExistAbstract(*pv_act_E);
+  q = q.ExistAbstract(*pv_ctx_E);
   return q;
 }
 
@@ -147,9 +157,7 @@ void ModelChecker::printReach(void)
   }
 
   dropCtxAutStatePart(*reach);
-
   srs->printDecodedRctSysStates(*reach);
-
   cleanup();
 
   if (opts->measure) {

mc.hh

@@ -25,7 +25,7 @@ class ModelChecker
     vector<BDD> *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
-    BDD *pv_act_E;
+    BDD *pv_ctx_E;
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;
@@ -37,6 +37,8 @@ class ModelChecker
     BDD *pv_ca_E;
     BDD *pv_ca_succ_E;
 
+    BDD *pv_proc_enab_E;
+
     unsigned int trp_size;
     unsigned int totalStateVars;
 

symrs.cc

@@ -215,27 +215,18 @@ void SymRS::initBDDvars(void)
   VERB_LN(2, "Variables for process enabledness/activity");
 
   pv_proc_enab = new BDDvec(numberOfProc);
+  pv_proc_enab_E = new BDD(BDD_TRUE);
 
   for (unsigned int i = 0; i < numberOfProc; ++i) {
-    (*pv_proc_enab)[i] = cuddMgr->bddVar(bdd_var_idx++);
+    auto bdd_var = cuddMgr->bddVar(bdd_var_idx++);
+    (*pv_proc_enab)[i] = bdd_var;
+    *pv_proc_enab_E *= bdd_var;
   }
 
   // ----------------------------------------------------------
   //                   Context Entities
   // ----------------------------------------------------------
 
-  // // 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];
-  // }
-
   VERB_LN(2, "Variables for context entities");
 
   pv_ctx = new BDDvec(totalCtxEntities);
@@ -526,26 +517,33 @@ BDD SymRS::compContext(const BDD &context) const
 
 std::string SymRS::decodedRctSysStateToStr(const BDD &state)
 {
-  assert(0);
   std::string s = "{ ";
-  /*
-  for (unsigned int i = 0; i < totalRctSysStateVars; ++i) {
-    if (!(encEntity(i) * state).IsZero()) {
-      s += rs->entityToStr(i) + " ";
+
+  for (const auto &proc_entities : usedProducts) {
+
+    auto proc_id = proc_entities.first;
+    auto entities = proc_entities.second;
+    s += rs->getProcessName(proc_id) + "={ ";
+
+    for (const auto &entity : entities) {
+      if (!(encEntity(proc_id, entity) * state).IsZero()) {
+        s += rs->entityToStr(entity) + " ";
+      }
     }
+
+    s += "} ";
   }
-  */
+
   s += "}";
   return s;
 }
 
 void SymRS::printDecodedRctSysStates(const BDD &states)
 {
-  assert(0);
   BDD unproc = states;
 
   while (!unproc.IsZero()) {
-    BDD t = unproc.PickOneMinterm(*pv_rs);
+    BDD t = unproc.PickOneMinterm(*pv_drs_flat);
     cout << decodedRctSysStateToStr(t) << endl;
 
     if (opts->verbose > 9) {
@@ -663,7 +661,9 @@ void SymRS::encodeTransitions(void)
     auto products = proc_products.second;
 
     for (const auto &prod : products) {
-      *monoTrans = encEntityProduction(proc_id, prod);
+      *monoTrans *= encEntityProduction(proc_id, prod);
+      cout << rs->getProcessName(proc_id) << " " << rs->getEntityName(prod) << endl;
+      BDD_PRINT(encEntityProduction(proc_id, prod));
     }
   }
 
@@ -682,12 +682,6 @@ void SymRS::encodeTransitions(void)
   }
 }
 
-BDD SymRS::encNoContext(void)
-{
-  assert(0);
-  return BDD_FALSE;
-}
-
 void SymRS::encodeInitStates(void)
 {
   if (usingContextAutomaton()) {

symrs.hh

@@ -51,9 +51,13 @@ class SymRS
     {
       return pv_succ_E;
     }
-    BDD *getEncPVact_E(void)
+    BDD *getEncPVctx_E(void)
     {
-      return pv_act_E;
+      return pv_ctx_E;
+    }
+    BDD *getEncPVproc_enab_E(void)
+    {
+      return pv_proc_enab_E;
     }
     BDDvec *getEncPartTrans(void)
     {
@@ -206,12 +210,7 @@ class SymRS
     BDD *pv_succ_E;
 
     BDDvec *pv_proc_enab;         /*!< Variables indicating if a process is enabled */
-
-    BDDvec *pv_rs; // remove
-    BDDvec *pv_rs_succ; // remove
-
-    BDD *pv_rs_E; // remove
-    BDD *pv_rs_succ_E; // remove
+    BDD *pv_proc_enab_E;
 
     vector<BDDvec> *pv_drs;       /*!< PVs for the product part of state
                                        (per DRS process) */
@@ -323,8 +322,6 @@ class SymRS
     std::string decodedRctSysStateToStr(const BDD &state);
     void printDecodedRctSysStates(const BDD &states);
 
-    BDD encNoContext(void);
-
     DecompReactions getProductionConditions(Process proc_id);
 
     void initBDDvars(void);