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>
@@ -47,7 +48,7 @@ class hoat
     acc_sigt acc_sig; // acceptance sets
   };
   using edgest = std::list<edget>;
-  using bodyt = std::list<std::pair<state_namet, edgest>>;
+  using bodyt = std::vector<std::pair<state_namet, edgest>>;
   bodyt body;
 
   hoat(headert _header, bodyt _body)
@@ -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};

unit/Makefile

@@ -5,6 +5,7 @@ SRC = unit_tests.cpp
 
 # Test source files
 SRC += smvlang/expr2smv.cpp \
+       temporal-logic/hoa.cpp \
        temporal-logic/ltl_sva_to_string.cpp \
        temporal-logic/sva_sequence_match.cpp \
        temporal-logic/nnf.cpp \

unit/temporal-logic/hoa.cpp

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: Hanoi Omega Automata (HOA) Format
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <temporal-logic/hoa.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("Parsing a HOA from a string")
+{
+  GIVEN("A HOA string for Xp")
+  {
+    auto hoa_string =
+      "HOA: v1.1\n"
+      "name: X!a0\n"
+      "States: 4\n"
+      "Start: 1\n"
+      "AP: 1 a0\n"
+      "acc-name: Buchi\n"
+      "Acceptance: 1 Inf ( 0 )\n"
+      "properties: trans-labels explicit-labels state-acc complete\n"
+      "properties: deterministic terminal very-weak\n"
+      "--BODY--\n"
+      "State: 0 {0}\n"
+      "[!0] 2\n"
+      "[0] 3\n"
+      "State: 1 {0}\n"
+      "[t] 0\n"
+      "State: 2 {0}\n"
+      "[t] 2\n"
+      "State: 3\n"
+      "[t] 3\n"
+      "--END--\n";
+
+    auto hoa = hoat::from_string(hoa_string);
+
+    REQUIRE(hoa.body.size() == 4);
+
+    REQUIRE(hoa.body[0].first.is_accepting());
+    REQUIRE(hoa.body[1].first.is_accepting());
+    REQUIRE(hoa.body[2].first.is_accepting());
+    REQUIRE(!hoa.body[3].first.is_accepting());
+
+    // now remove the extra accepting states
+    hoa.buechi_acceptance_cleanup();
+
+    REQUIRE(!hoa.body[0].first.is_accepting());
+    REQUIRE(!hoa.body[1].first.is_accepting());
+    REQUIRE(hoa.body[2].first.is_accepting());
+    REQUIRE(!hoa.body[3].first.is_accepting());
+  }
+}