Partitioned trnasition relation with reordering

drs_benchmark.sh

@@ -2,7 +2,7 @@
 
 TMPINPUT="tmp_$RANDOM$RANDOM.rs"
 
-CMD="./reactics -b -B"
+CMD="./reactics -z -b -B"
 
 for i in `seq 2 20`;do
 

mc.cc

@@ -73,8 +73,8 @@ inline BDD ModelChecker::getSucc(const BDD &states)
   VERB_L2("Computing successors");
 
   if (opts->part_tr_rel) {
-    for (unsigned int i = 0; i < trp_size; ++i) {
-      q *= states * (*trp)[i];
+    for (const auto &trans : *trp) {
+      q *= states * trans;
     }
   }
   else {
@@ -99,8 +99,8 @@ inline BDD ModelChecker::getPreE(const BDD &states)
   BDD x = states.SwapVariables(*pv, *pv_succ);
 
   if (opts->part_tr_rel) {
-    for (unsigned int i = 0; i < trp_size; ++i) {
-      q *= x * (*trp)[i];
+    for (const auto &trans : *trp) {
+      q *= x * trans;
     }
   }
   else {
@@ -110,6 +110,7 @@ inline BDD ModelChecker::getPreE(const BDD &states)
   q = q.ExistAbstract(*pv_succ_E);
   q = q.ExistAbstract(*pv_ctx_E);
   q = q.ExistAbstract(*pv_proc_enab_E);
+
   return q;
 }
 
@@ -120,9 +121,10 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
   BDD x = states.SwapVariables(*pv, *pv_succ);
 
   if (opts->part_tr_rel) {
-    for (unsigned int i = 0; i < trp_size; ++i) {
-      q *= x * (*trp)[i] * *contexts;
+    for (const auto &trans : *trp) {
+      q *= x * trans;
     }
+    q *= *contexts;
   }
   else {
     q *= x * *trm * *contexts;

symrs.cc

@@ -660,11 +660,7 @@ BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
 
   } // END FOR: cond
 
-  if (opts->reorder_trans) {
-    VERB_L2("Reordering START");
-    Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
-    VERB_L2("Reordering DONE");
-  }
+  reorder();
 
   return enab;
 }
@@ -762,15 +758,42 @@ void SymRS::encodeTransitions(void)
 
   if (opts->part_tr_rel) {
     VERB("Using partitioned transition relation encoding");
-    FERROR("Partitioned transition relation is currently not supported");
+
+    if (usingContextAutomaton()) {
+      partTrans = new BDDvec(numberOfProc+1);
     }
     else {
+      partTrans = new BDDvec(numberOfProc);
+    }
+
+  }
+  else {
+
     VERB("Using monolithic transition relation encoding");
     monoTrans = new BDD(BDD_TRUE);
+
   }
 
   VERB_LN(3, "Entity production encoding for all the processes and their products");
 
+  if (opts->part_tr_rel)
+  {
+
+    for (const auto &proc_products : usedProducts) {
+      auto proc_id = proc_products.first;
+      auto products = proc_products.second;
+
+      (*partTrans)[proc_id] = BDD_TRUE;
+
+      for (const auto &prod : products) {
+        (*partTrans)[proc_id] *= encEntityProduction(proc_id, prod);
+      }
+    }
+
+
+  }
+  else {
+
     for (const auto &proc_products : usedProducts) {
       auto proc_id = proc_products.first;
       auto products = proc_products.second;
@@ -780,13 +803,16 @@ void SymRS::encodeTransitions(void)
       }
     }
 
+  }
+
   VERB("Reactions ready");
 
   if (usingContextAutomaton()) {
     VERB("Augmenting transition relation encoding with the transition relation for context automaton");
 
     if (opts->part_tr_rel) {  
-      FERROR("Partitioned transition relation is currently not supported");
+      auto last_index = numberOfProc;
+      (*partTrans)[last_index] = *tr_ca;
     }
     else {
       assert(tr_ca != nullptr);
@@ -915,4 +941,14 @@ void SymRS::encodeCtxAutTrans(void)
   }
 }
 
+
+void SymRS::reorder(void)
+{
+  if (opts->reorder_trans) {
+    VERB_L2("Reordering START");
+    Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+    VERB_L2("Reordering DONE");
+  }
+}
+
 /** EOF **/

symrs.hh

@@ -344,6 +344,8 @@ class SymRS
 
     size_t getCtxAutStateEncodingSize(void);
 
+    void reorder(void);
+
 };
 
 #endif