clean up HOA accepting states

The HOAs generated by Spot can now be transformed into a graph.

This graph is used to remove accepting states that are not part of a cycle.

Author: kroening

src/temporal-logic/hoa.cpp

@@ -543,3 +543,40 @@ 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;
+}
+
+void hoat::buechi_acceptance_cleanup()
+{
+  using hoa_grapht = grapht<graph_nodet<hoat::graph_edget>>;
+  auto as_graph = graph();
+  for(auto &state : body)
+  {
+    if(state.first.is_accepting())
+    {
+      hoa_grapht::patht loop_path;
+      as_graph.shortest_loop(state.first.number, loop_path);
+      // when this state is not part of any cycle,
+      // then we cannot have Buechi acceptance via this state
+      if(loop_path.empty())
+        state.first.acc_sig.clear();
+    }
+  }
+}

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,19 @@ 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;
+
+  // Remove accepting states that are not part of a cycle.
+  // These are irrelevant when using the standard Buechi
+  // acceptance criterion.
+  void buechi_acceptance_cleanup();
 };
 
 #endif // CPROVER_TEMPORAL_LOGIC_HOA_H

src/temporal-logic/ltl_to_buechi.cpp

@@ -135,6 +135,9 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
 
     message.debug() << hoa << messaget::eom;
 
+    // clean up accepting states
+    hoa.buechi_acceptance_cleanup();
+
     auto max_state_number = hoa.max_state_number();
     auto state_type = range_typet{0, max_state_number};
     const auto buechi_state = symbol_exprt{"buechi::state", state_type};