refactor: ReachableBDD2

src/RdPBDD.cpp

@@ -238,40 +238,33 @@ bdd RdPBDD::ReachableBDD1() const {
   return m2;
 }
 
-bdd RdPBDD::ReachableBDD2() {
-  bdd M1;
-  bdd M2 = m0;
-  // double tps;
-  // double d = (double)clock() / (double)CLOCKS_PER_SEC;
+bdd RdPBDD::ReachableBDD2() const {
+  bdd m2 = m0;
+
   nb_iter = 0;
   max_bdd_nodes = bdd_nodecount(m0);
-  while (M1 != M2) {
-    M1 = M2;
-    bdd Reached;
-    for (vector<Trans>::const_iterator i = relation.begin();
-         i != relation.end(); i++) {
-      bdd succ = (*i)(M2);
-      Reached = succ | Reached;
-      // cout << bdd_nodecount(succ) << endl;
-      // if(succ!=bddfalse)
+
+  bdd m1;
+  while (m1 != m2) {
+    m1 = m2;
+
+    bdd reached;
+    for (const auto &i : relation) {
+      reached = i(m2) | reached;
     }
+    m2 = m2 | reached;
+
+    const int current_size = bdd_nodecount(m2);
+    if (max_bdd_nodes < current_size) {
+      max_bdd_nodes = current_size;
+    }
+
     nb_iter++;
-    M2 = M2 | Reached;
-    int Current_size = bdd_nodecount(M2);
-    if (max_bdd_nodes < Current_size)
-      max_bdd_nodes = Current_size;
-    // cout<<"Iteration numero "<<NbIt<<" nb node de reached
-    // :"<<bdd_nodecount(M2)<<endl;
-    //		//cout << bdd_nodecount(M2) << endl;
   }
-  // cout << endl;
-  // tps = ((double)(clock()) / CLOCKS_PER_SEC) - d;
-  // cout<<"-----------------------------------------------------\n";
-  // cout << "CONSTRUCTION TIME  " << tps << endl;
-  // cout<<"Max Intermediary BDD "<<MaxIntBdd<<endl;
-  // cout<<"Nombre d'iteration : "<<NbIt<<endl;
-  return M2;
+
+  return m2;
 }
+
 bdd RdPBDD::ReachableBDD3() {
   // double tps;
   // double d = (double)clock() / (double)CLOCKS_PER_SEC;

src/RdPBDD.hpp

@@ -63,7 +63,7 @@ class RdPBDD {
   ~RdPBDD() = default;
 
   bdd ReachableBDD1() const;
-  bdd ReachableBDD2();
+  bdd ReachableBDD2() const;
   bdd ReachableBDD3();
 
   // SOG generation