From 09578a075ff2c06d6016e797dbdb503793983bd9 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sat, 21 Apr 2018 19:15:06 +0100
Subject: [PATCH] Quantification for only the i-th process

---
 mc.cc | 24 ++++++++++++++++++++++++
 mc.hh |  5 +++++
 2 files changed, 29 insertions(+)

diff --git a/mc.cc b/mc.cc
index e4be58e..d6da428 100644
--- a/mc.cc
+++ b/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()) {
diff --git a/mc.hh b/mc.hh
index 31fe9ae..12497d9 100644
--- a/mc.hh
+++ b/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: