Hanoi Omega-Automata as graphs

The HOAs generated by Spot are now transformed into a graph as an
intermediate step.

Author: kroening

src/temporal-logic/hoa.cpp

@@ -543,3 +543,22 @@ void hoat::output(std::ostream &out) const
 
   out << "--END--\n";
 }
+
+grapht<graph_nodet<hoat::graph_edget>> hoat::graph() const
+{
+  grapht<graph_nodet<hoat::graph_edget>> graph;
+
+  graph.resize(numeric_cast_v<std::size_t>(max_state_number() + 1));
+
+  for(auto &state : body)
+  {
+    for(auto &edge : state.second)
+      for(auto &dest : edge.dest_states)
+      {
+        graph.add_edge(state.first.number, dest);
+        graph.edge(state.first.number, dest).label = edge.label;
+      }
+  }
+
+  return graph;
+}

src/temporal-logic/hoa.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_TEMPORAL_LOGIC_HOA_H
 #define CPROVER_TEMPORAL_LOGIC_HOA_H
 
+#include <util/graph.h>
 #include <util/irep.h>
 
 #include <cstdint>
@@ -68,6 +69,14 @@ class hoat
 
   // atomic propositions
   std::map<intt, std::string> ap_map;
+
+  // convert into a graph
+  struct graph_edget
+  {
+    labelt label;
+  };
+
+  grapht<graph_nodet<graph_edget>> graph() const;
 };
 
 #endif // CPROVER_TEMPORAL_LOGIC_HOA_H