refactor: CanonizeR

src/RdPBDD.cpp

@@ -19,7 +19,7 @@ constexpr int BDD_SIZE_CACHES = 1000000;
 
 // TODO: why these global variables ?
 int nb_iter;
-int itext, itint;
+int it_ext, it_int;
 int max_bdd_nodes;
 bdd *TabMeta;
 int nb_meta_state;
@@ -422,7 +422,7 @@ set<chem> RdPBDD::ChemObs(SOG &g, map<int, int> trans_obs) const {
   nb_meta_state = 0;
   max_bdd_nodes = 0;
   nb_iter = 0;
-  itext = itint = 0;
+  it_ext = it_int = 0;
 
   bool ancien = true;
 
@@ -471,8 +471,8 @@ set<chem> RdPBDD::ChemObs(SOG &g, map<int, int> trans_obs) const {
       st.push(e);
 
       // double nbnode;
-      auto *reached_class = new ClassOfState;
       {
+        auto *reached_class = new ClassOfState;
         bdd complete_meta_state =
             AccessibleEpsilon(GetSuccessor(e.first.second, t));
         reached_class->state = complete_meta_state;
@@ -558,112 +558,95 @@ stack<Couple> RdPBDD::RecherchePointsEntree(chem path, const SOG &g) const {
   return pt_entr;
 }
 
-////////////////////////////////////////////
-
-chem RdPBDD::ChemAbs(chem path, SOG &g) {
-  vector<int> ch_abstrait, ch_agregat;
-  int trans;
-  Couple agr_entree;
-  stack<Couple> point_entree;
-  bdd cible, source;
-  ClassOfState *agr = new ClassOfState;
-  // agr=dernier agr
-  point_entree = RecherchePointsEntree(path, g);
+chem RdPBDD::AbstractPaths(chem path, const SOG &g) {
+  bdd source;
+  vector<int> abstract_paths;
+  stack<Couple> point_entree = RecherchePointsEntree(path, g);
+
   int i = 0;
   while (!point_entree.empty()) {
-    trans = *(path.end() - 1);
-    // cout<<"on traite "<< trans+1<<endl;
-    agr_entree = point_entree.top();
-    // cout<<" l'agr trait� "<<agr_entree.first->class_state.id()<<endl;
-    point_entree.pop();  // effacer l'element le dernier element
-    cible = agr_entree.second;
-    agr = agr_entree.first;
+    int trans = *(path.end() - 1);
+    const Couple agr_entree = point_entree.top();
+    point_entree.pop();
+
+    ClassOfState *agr = agr_entree.first;
+    const bdd target = agr_entree.second;
+
     if (i == 0) {
       source = FrontiereNodes1(agr->state, trans);
     }
+
     if (i == 1) {
       source = (relation[trans])[source];
     }
-    ch_agregat = SubPathAgregate(&source, cible, agr);
-    // cout<<"sub_path found "<<endl;
-    ch_abstrait.insert(ch_abstrait.begin(), trans);
-    ch_abstrait.insert(ch_abstrait.begin(), ch_agregat.begin(),
-                       ch_agregat.end());
+
+    vector<int> path_aggregate = SubPathAggregate(&source, target, agr);
+    abstract_paths.insert(abstract_paths.begin(), trans);
+    abstract_paths.insert(abstract_paths.begin(), path_aggregate.begin(),
+                          path_aggregate.end());
     path.pop_back();
     i = 1;
   }
 
-  return ch_abstrait;
+  return abstract_paths;
 }
 
-///////----------------- trouver un chemain de la source � cible dans un agregat
-/// agr---
-vector<int> RdPBDD::SubPathAgregate(bdd *source, bdd target,
-                                    ClassOfState *aggr) {
-  vector<int> ch_agregat;
-
-  pair<int, bdd> couple;
-  // int transition;
-  // int i = 0;
-  bdd courant = *source;
-  bdd egalite = target & courant;
-
-  // cout<<"a difference between source and target "<< (egalite ==
-  // bdd_false())<<endl;
-  while (egalite == bdd_false()) {
-    couple = StepBackward1(courant, aggr);
-    ch_agregat.insert(ch_agregat.begin(), couple.first);
-    courant = couple.second;
-    egalite = (target & courant);
-
-    // cout<<"a difference between source and target  "<< (egalite ==
-    // bdd_false())<<endl;
+vector<int> RdPBDD::SubPathAggregate(bdd *source, const bdd &target,
+                                     const ClassOfState *aggr) const {
+  vector<int> path;
+
+  bdd current_state = *source;
+  while ((target & current_state) == bdd_false()) {
+    pair<int, bdd> couple = StepBackward1(current_state, aggr);
+    path.insert(path.begin(), couple.first);
+    current_state = couple.second;
   }
 
-  *source = courant;
-  return ch_agregat;
+  *source = current_state;
+  return path;
 }
 
-/*-----------------------CanonizeR()----------------*/
 bdd RdPBDD::CanonizeR(bdd s, unsigned int i) {
   bdd s1, s2;
   do {
-    itext++;
+    it_ext++;
     s1 = s - bdd_nithvar(2 * i);
     s2 = s - s1;
-    if ((!(s1 == bddfalse)) && (!(s2 == bddfalse))) {
+
+    // TODO: extract the loop into a function
+    if (s1 != bddfalse && s2 != bddfalse) {
       bdd front = s1;
       bdd reached = s1;
       do {
-        // cout<<"premiere boucle interne \n";
-        itint++;
+        it_int++;
         front = StepForward(front) - reached;
         reached = reached | front;
         s2 = s2 - front;
-      } while ((!(front == bddfalse)) && (!(s2 == bddfalse)));
+      } while (front != bddfalse && s2 != bddfalse);
     }
-    if ((!(s1 == bddfalse)) && (!(s2 == bddfalse))) {
+
+    if (s1 != bddfalse && s2 != bddfalse) {
       bdd front = s2;
       bdd reached = s2;
       do {
-        // //cout<<"deuxieme boucle interne \n";
-        itint++;
+        it_int++;
         front = StepForward(front) - reached;
         reached = reached | front;
         s1 = s1 - front;
-      } while ((!(front == bddfalse)) && (!(s1 == bddfalse)));
+      } while (front != bddfalse && s1 != bddfalse);
     }
+
     s = s1 | s2;
     i++;
-  } while ((i < nb_places) && ((s1 == bddfalse) || (s2 == bddfalse)));
+  } while (i < nb_places && (s1 == bddfalse || s2 == bddfalse));
+
   if (i >= nb_places) {
-    // cout<<"____________oooooooppppppppsssssssss________\n";
     return s;
-  } else {
-    // cout<<"________________p a s o o o p p p s s s ______\n";
-    return (CanonizeR(s1, i) | CanonizeR(s2, i));
   }
+
+  return (CanonizeR(s1, i) | CanonizeR(s2, i));
 }
+
 /*---------------------------  Set_Bloc()  -------*/
 bool RdPBDD::SetBloc(bdd &s) const {
   // cout<<"Ici detect blocage \n";

src/RdPBDD.hpp

@@ -107,8 +107,14 @@ class RdPBDD {
   // SOG generation
   std::stack<Couple> RecherchePointsEntree(chem path, const SOG& g) const;
 
-  chem ChemAbs(chem path, SOG& g);
-  std::vector<int> SubPathAgregate(bdd* source, bdd target, ClassOfState* aggr);
+  // Generate abstract paths
+  chem AbstractPaths(chem path, const SOG& g);
+
+  // Find a path from a source state to a target state in an aggregate
+  std::vector<int> SubPathAggregate(bdd* source, const bdd& target,
+                                    const ClassOfState* aggr) const;
+
+  bdd CanonizeR(bdd s, unsigned int i);
 
   bdd EmersonLey(bdd state, bool trace);
   void GeneralizedSynchProduct1(ModularSOG& Gv, int nb_subnets,
@@ -117,7 +123,6 @@ class RdPBDD {
   bool SetBloc(bdd& s) const;
   bdd FrontiereNodes(bdd from) const;
   bdd FrontiereNodes1(bdd from, int t);
-  bdd CanonizeR(bdd s, unsigned int i);
 };
 
 #endif  // RdPBDD_H_

src/main.cpp

@@ -233,7 +233,7 @@ void compute_abstract_paths(const string& net_file, int bound,
   cout << "\nComputing abstract paths ...";
   auto start_abstract_time = getTime();
   for (const path_t& path : obs_paths) {
-    abstract_paths.insert(R.ChemAbs(path, sog));
+    abstract_paths.insert(R.AbstractPaths(path, sog));
   }
   auto abstract_time = getTime() - start_abstract_time;
   cout << " done\nTime for computing abstract paths: " << abstract_time