Quantification for only the i-th process

mc.cc

@@ -430,6 +430,30 @@ BDD ModelChecker::statesEFctx(const BDD *contexts, const BDD &states)
   return x;
 }
 
+BDD ModelChecker::getIthOnly(Process proc_id)
+{
+  /* if possible, we return the BDD from cache */
+  if (ith_only_E.count(proc_id) == 1) {
+    return ith_only_E[proc_id];
+  }
+
+  /* nothing has been found in the cache */
+  BDD bdd = BDD_TRUE;
+
+  for (auto i = 0; i < pv_drs_E->size(); ++i) {
+
+    if (i == proc_id) {
+      continue;
+    }
+
+    bdd *= (*pv_drs_E)[i];
+  }
+
+  ith_only_E[proc_id] = bdd;
+
+  return bdd;
+}
+
 bool ModelChecker::checkRSCTL(FormRSCTL *form)
 {
   if (form->isERSCTL()) {

mc.hh

@@ -31,6 +31,8 @@ class ModelChecker
     vector<BDD> *trp;
     BDD *trm;
 
+    std::map<Process, BDD> ith_only_E;
+
     // Context Automaton
     bool using_ctx_aut;
     vector<BDD> *pv_ca;
@@ -58,6 +60,9 @@ class ModelChecker
     BDD statesEGctx(const BDD *contexts, const BDD &states);
     BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB);
     BDD statesEFctx(const BDD *contexts, const BDD &states);
+
+    BDD getIthOnly(Process proc_id);
+
     void cleanup(void);
 
   public: