refactor: rename functions following the paper

src/main.cpp

@@ -228,7 +228,7 @@ void ComputeAbstractPaths(const string& net_file, int bound,
   cout << "\nComputing abstract paths ...";
   auto start_abstract_time = GetTime();
   for (const Path& path : obs_paths) {
-    abstract_paths.insert(pn_sog.AbstractPaths(path, sog));
+    abstract_paths.insert(pn_sog.AbstractPath(path, sog));
   }
   auto abstract_time = GetTime() - start_abstract_time;
   cout << " done\nTime for computing abstract paths: " << abstract_time

src/petri_net_sog.cpp

@@ -404,13 +404,13 @@ Paths PetriNetSOG::ObservablePaths(SOG &sog, map<int, int> trans_obs) const {
   return observable_paths;
 }
 
-stack<AggrPair> PetriNetSOG::RecherchePointsEntree(Path path,
-                                                   const SOG &g) const {
+stack<AggrPair> PetriNetSOG::SearchEntryPoints(Path path,
+                                               const SOG &sog) const {
   AggrPair p;
   stack<AggrPair> pt_entr;
 
   bdd entree = m0;
-  Aggregate *agr = g.initial_state;
+  Aggregate *agr = sog.initial_state;
 
   p.first = agr;
   p.second = entree;
@@ -435,29 +435,28 @@ stack<AggrPair> PetriNetSOG::RecherchePointsEntree(Path path,
   return pt_entr;
 }
 
-Path PetriNetSOG::AbstractPaths(Path path, const SOG &g) const {
+bdd PetriNetSOG::SearchExitPoints(const bdd &from, const int t) const {
+  return bddfalse | (from & relation[t].precond);
+}
+
+Path PetriNetSOG::AbstractPath(Path path, const SOG &sog) const {
   bdd source;
-  vector<int> abstract_paths;
-  stack<AggrPair> entry_point = RecherchePointsEntree(path, g);
+  Path abstract_paths;
+  stack<AggrPair> entry_points = SearchEntryPoints(path, sog);
 
   bool flag = false;
-  while (!entry_point.empty()) {
+  while (!entry_points.empty()) {
     int trans = *(path.end() - 1);
-    const AggrPair entry_aggr = entry_point.top();
-    entry_point.pop();
+    const AggrPair entry_aggr = entry_points.top();
+    entry_points.pop();
 
     const Aggregate *aggr = entry_aggr.first;
     const bdd target = entry_aggr.second;
 
-    if (!flag) {
-      source = FrontiereNodes(aggr->state, trans);
-    }
+    source =
+        flag ? relation[trans][source] : SearchExitPoints(aggr->state, trans);
 
-    if (flag) {
-      source = (relation[trans])[source];
-    }
-
-    vector<int> path_aggregate = SubPathAggregate(&source, target, aggr);
+    Path path_aggregate = SubPathAggregate(&source, target, aggr);
     abstract_paths.insert(abstract_paths.begin(), trans);
     abstract_paths.insert(abstract_paths.begin(), path_aggregate.begin(),
                           path_aggregate.end());
@@ -482,7 +481,3 @@ Path PetriNetSOG::SubPathAggregate(bdd *source, const bdd &target,
   *source = current_state;
   return path;
 }
-
-bdd PetriNetSOG::FrontiereNodes(const bdd &from, const int t) const {
-  return bddfalse | (from & relation[t].precond);
-}

src/petri_net_sog.hpp

@@ -120,24 +120,50 @@ class PetriNetSOG {
   Set FirableObservableTrans(const bdd& from) const;
 
   /**
-   * Extract observable paths. It constructs the SOG of the petri net model
+   * Compute the aggregates traversed along the observable path, each
+   * associated with the set of its input states (i.e., the set of states
+   * reached by the previous observable transition in the trace starting from
+   * the previous aggregate).
+   * @param path observable path
    * @param sog SOG graph
-   * @param trans_obs observable transitions
-   * @return set of observable paths
+   * @return stack of aggregates and their input states
    */
-  Paths ObservablePaths(SOG& sog, std::map<int, int> trans_obs) const;
-
-  // SOG generation
-  std::stack<AggrPair> RecherchePointsEntree(Path path, const SOG& g) const;
+  std::stack<AggrPair> SearchEntryPoints(Path path, const SOG& sog) const;
 
-  // Generate abstract paths
-  Path AbstractPaths(Path path, const SOG& g) const;
+  /**
+   * Compute the exit points of a transition from a marking
+   * @param from marking from which the exit points are computed
+   * @param t transition identifier
+   * @return the set of exit points
+   */
+  bdd SearchExitPoints(const bdd& from, int t) const;
 
-  // Find a path from a source state to a target state in an aggregate
+  /**
+   * Returns the shortest unobservable path linking the entry and exit points of
+   * the aggregate
+   * @param source entry points
+   * @param target exit points
+   * @param aggr aggregate
+   * @return unobservable path
+   */
   Path SubPathAggregate(bdd* source, const bdd& target,
                         const Aggregate* aggr) const;
 
-  bdd FrontiereNodes(const bdd& from, int t) const;
+  /**
+   * Extract observable paths. It constructs the SOG of the petri net model
+   * @param sog SOG graph
+   * @param trans_obs observable transitions
+   * @return set of observable paths
+   */
+  Paths ObservablePaths(SOG& sog, std::map<int, int> trans_obs) const;
+
+  /**
+   * Extract the abstract path from an observable path
+   * @param path observable path
+   * @param sog built SOG
+   * @return abstract path
+   */
+  Path AbstractPath(Path path, const SOG& sog) const;
 };
 
 #endif  // PETRI_NET_SOG_H_