BUG FIX: node comparator used to produce output of covreach graphs wa…

…s not calling the expected tchecker::lexical_cmp function (fixes #41)
ticktac-project · Dec 7, 2019 · faf06bd · faf06bd
1 parent 5ab0ce7
commit faf06bd
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 22 deletions.
diff --git a/include/tchecker/algorithms/covreach/output.hh b/include/tchecker/algorithms/covreach/output.hh
@@ -76,6 +76,9 @@ namespace tchecker {
       /*!
        \brief Graph output
        \tparam GRAPH : type of graph, should inherit from tchecker::covreach::graph_t
+       \tparam NODE_LT : type of total ordering on GRAPH::node_ptr_t, should be deterministic in order to guarantee
+       that the output does not depend on the way the graph has been built (memory allocation, order of exploration, etc).
+       This can be achieved using tchecker::lexical_cmp for instance.
        \tparam HASH : type of hash function on GRAPH::node_ptr_t
        \tparam EQUAL : type of equality predicate on GRAPH::node_ptr_t
        \param os : output stream
@@ -85,18 +88,20 @@ namespace tchecker {
        \return os after g has been output
        */
       template
-      <class GRAPH, class HASH=std::hash<typename GRAPH::node_ptr_t>, class EQUAL=std::equal_to<typename GRAPH::node_ptr_t>>
+      <class GRAPH,
+      class NODE_LT,
+      class HASH=std::hash<typename GRAPH::node_ptr_t>,
+      class EQUAL=std::equal_to<typename GRAPH::node_ptr_t>
+      >
       std::ostream & output(std::ostream & os, GRAPH const & g, std::string const & name)
       {
         using node_ptr_t = typename GRAPH::node_ptr_t;
         using edge_ptr_t = typename GRAPH::edge_ptr_t;
 
-        auto cmp = [](node_ptr_t const &p1, node_ptr_t const &p2) {
-          return tchecker::lexical_cmp(*p1, *p2) < 0;
-        };
-
-        std::set<node_ptr_t, decltype (cmp)> nodes(cmp);
-        std::map<node_ptr_t, std::size_t, decltype (cmp)> index(cmp);
+        NODE_LT node_lt;
+
+        std::set<node_ptr_t, NODE_LT> nodes(node_lt);
+        std::map<node_ptr_t, std::size_t, NODE_LT> index(node_lt);
 
         if (_all_nodes)
           {
@@ -144,7 +149,7 @@ namespace tchecker {
           index.emplace(n, index.size() + 1);
         }
         for(auto n : nodes) {
-          output_node (os, g, n, index);
+          output_node (os, g, n, index, node_lt);
         }
         os << "}" << std::endl;
 
@@ -154,21 +159,20 @@ namespace tchecker {
         return os;
       }
     private:
-      template <class GRAPH, class NODEPTR=typename GRAPH::node_ptr_t, class MAP>
-      void output_node(std::ostream & os, GRAPH const &g, NODEPTR const &n,
-                       MAP const &index)
+      template <class GRAPH, class NODEPTR=typename GRAPH::node_ptr_t, class MAP, class NODE_LT>
+      void output_node(std::ostream & os, GRAPH const &g, NODEPTR const &n, MAP const &index, NODE_LT && node_lt)
       {
         using edge_ptr_t = typename GRAPH::edge_ptr_t;
 
         os << "n" << index.at(n) << " [label=\"";
         _node_outputter.output(os, *n);
         os << "\"]" << std::endl;
 
-        auto cmp = [&g](edge_ptr_t const &e1, edge_ptr_t const &e2) {
-            return tchecker::lexical_cmp(*(g.edge_tgt(e1)),*(g.edge_tgt(e2))) < 0;
+        auto edge_lt = [&g,&node_lt](edge_ptr_t const &e1, edge_ptr_t const &e2) {
+          return node_lt(g.edge_tgt(e1), g.edge_tgt(e2));
         };
 
-        std::set<edge_ptr_t, decltype (cmp)> edges(cmp);
+        std::set<edge_ptr_t, decltype (edge_lt)> edges(edge_lt);
         auto outgoing_edges = g.outgoing_edges(n);
         for(edge_ptr_t const &e : outgoing_edges)
           edges.insert(e);

diff --git a/include/tchecker/algorithms/covreach/run.hh b/include/tchecker/algorithms/covreach/run.hh
@@ -79,6 +79,14 @@ namespace tchecker {
               }
             };
 
+            class node_lt_t {
+            public:
+              bool operator() (node_ptr_t const & n1, node_ptr_t const & n2) const
+              {
+                return tchecker::lexical_cmp(*n1, *n2) < 0;
+              }
+            };
+
             static std::tuple<> state_predicate_args(model_t const & model)
             {
               return std::tuple<>();
@@ -150,6 +158,14 @@ namespace tchecker {
               }
             };
 
+            class node_lt_t {
+            public:
+              bool operator() (node_ptr_t const & n1, node_ptr_t const & n2) const
+              {
+                return tchecker::lexical_cmp(*n1, *n2) < 0;
+              }
+            };
+
             static std::tuple<> state_predicate_args(model_t const & model)
             {
               return std::tuple<>();
@@ -258,9 +274,9 @@ namespace tchecker {
         if (options.output_format() == tchecker::covreach::options_t::DOT) {
           tchecker::covreach::dot_outputter_t<typename ALGORITHM_MODEL::node_outputter_t>
           dot_outputter(false, ALGORITHM_MODEL::node_outputter_args(model));
-          dot_outputter.template output<graph_t, tchecker::instrusive_shared_ptr_hash_t>(options.output_stream(),
-                                                                                         graph,
-                                                                                         model.system().name());
+
+          dot_outputter.template output<graph_t, typename ALGORITHM_MODEL::node_lt_t>
+          (options.output_stream(), graph, model.system().name());
         }
 
         gc.stop();

diff --git a/include/tchecker/utils/shared_objects.hh b/include/tchecker/utils/shared_objects.hh
@@ -75,7 +75,7 @@ namespace tchecker {
      \param ptr : pointer to an allocated zone
      \param args : parameters to a constructor of type T
      \pre ptr points sizeof(refcount_t) bytes after the beginning of an
-     allocated zone of size at least 
+     allocated zone of size at least
      tchecker::allocation_size_t<shared_ptr_t<T>>
      \see tchecker::make_shared_t::make_shared_t
      */
@@ -134,7 +134,7 @@ namespace tchecker {
      \param t : shared object
      \post t has been assign to this
      \note the reference counter is not touched
-     */		
+     */
     make_shared_t<T, REFCOUNT, RESERVED> & operator= (tchecker::make_shared_t<T, REFCOUNT, RESERVED> const & t)
     {
       this->T::operator=(t);
@@ -315,7 +315,7 @@ namespace tchecker {
   /*!
    \class intrusive_shared_ptr_t
    \brief Shared pointers with intrusive reference counter
-   \tparam T : type of internal pointer. Must be make_shared_t<Y> for some type 
+   \tparam T : type of internal pointer. Must be make_shared_t<Y> for some type
    Y.
    */
   template <class T>
@@ -579,8 +579,6 @@ namespace tchecker {
   }
 
 
-
-
   /*!
    \class intrusive_shared_ptr_hash_t
    \brief Hash
@@ -638,5 +636,30 @@ namespace tchecker {
 
 } // end of namespace tchecker
 
+
+
+namespace std {
+
+  /*!
+   \class hash
+   \brief Specialisation of std::hash<> for tchecker::intrusive_shared_ptr_t
+   \tparam T : type of internal pointer (see tchecker::intrusive_shared_ptr_t)
+   */
+  template <class T>
+  class hash<tchecker::intrusive_shared_ptr_t<T>> {
+  public:
+    /*!
+     \brief Hash function
+     \param p : intrusive shared pointer
+     \return hash value for the internal pointer in p
+     */
+    std::size_t operator() (tchecker::intrusive_shared_ptr_t<T> const & p) const
+    {
+      return tchecker::hash_value(p);
+    }
+  };
+
+} // end of namespace std
+
 #endif // TCHECKER_SHARED_OBJECTS_HH