LTL/SVA->Buechi: reject error traces early

The Buechi automaton accepts counterexamples to the original property.  The
Buechi acceptance condition requires a lasso where the loop contains an
accepting state.  A proof of that requires satisfying the looping condition,
which may require a very long counterexample.

This adds a shortcut using a sufficient condition for a counterexample: we
can reject the property when we reach a state in which the Buechi automaton
transitions into an accepting state that has an unconditional self-loop on
it.  Such traces can always be extended to a lasso as above.

Author: kroening

regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/followed-by4.sv
 --buechi --bound 3
 ^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
@@ -9,4 +9,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-p1 is not refuted.

regression/ebmc-spot/sva-buechi/s_always1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/s_always1.sv
 --buechi --bound 20
 ^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
@@ -8,4 +8,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-main.p1 is not refuted.

src/ebmc/instrument_buechi.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "instrument_buechi.h"
 
+#include <util/format_expr.h>
+
 #include <temporal-logic/ltl.h>
 #include <temporal-logic/ltl_to_buechi.h>
 #include <temporal-logic/temporal_logic.h>
@@ -67,5 +69,12 @@ void instrument_buechi(
     // so this is the negation of the Buechi acceptance condition.
     property.normalized_expr =
       F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}};
+
+    if(!buechi.error_signal.is_true())
+      property.normalized_expr = and_exprt{
+        property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}};
+
+    message.debug() << "New property: " << format(property.normalized_expr)
+                    << messaget::eom;
   }
 }

src/temporal-logic/hoa.h

@@ -32,6 +32,10 @@ class hoat
     mp_integer number;
     labelt label; // in-state condition
     acc_sigt acc_sig;
+    bool is_accepting() const
+    {
+      return !acc_sig.empty();
+    }
   };
   struct edget
   {

src/temporal-logic/ltl_to_buechi.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "ltl_to_buechi.h"
 
 #include <util/arith_tools.h>
+#include <util/expr_util.h>
 #include <util/format_expr.h>
 #include <util/message.h>
 #include <util/replace_expr.h>
@@ -37,6 +38,7 @@ void buechi_transt::rename_state_symbol(const symbol_exprt &new_state_symbol)
 
   replace_expr(replace_map, init);
   replace_expr(replace_map, trans);
+  replace_expr(replace_map, error_signal);
   replace_expr(replace_map, liveness_signal);
 
   state_symbol = new_state_symbol;
@@ -81,6 +83,23 @@ exprt hoa_label_to_expr(
   }
 }
 
+// an accepting state with an unconditional self-loop
+bool is_error_state(const std::pair<hoat::state_namet, hoat::edgest> &state)
+{
+  if(!state.first.is_accepting())
+    return false;
+
+  for(auto &edge : state.second)
+  {
+    if(edge.label.id() == "t")
+      for(auto &dest : edge.dest_states)
+        if(dest == state.first.number)
+          return true;
+  }
+
+  return false;
+}
+
 buechi_transt
 ltl_to_buechi(const exprt &property, message_handlert &message_handler)
 {
@@ -100,8 +119,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
 
     // State-based Buchi acceptance. Should compare with transition-based
     // acceptance.
-    // Use --complete to be able to have multiple properties in one
-    // model.
+    // The generated automata may have deadend states.
     auto run_result = run(
       "ltl2tgba",
       {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string},
@@ -144,7 +162,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
     std::vector<exprt> liveness_disjuncts;
 
     for(auto &state : hoa.body)
-      if(!state.first.acc_sig.empty())
+      if(state.first.is_accepting())
       {
         liveness_disjuncts.push_back(equal_exprt{
           buechi_state, from_integer(state.first.number, state_type)});
@@ -155,6 +173,37 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
     message.debug() << "Buechi liveness signal: " << format(liveness_signal)
                     << messaget::eom;
 
+    // construct the error signal -- true when the next automaton state
+    // is nonaccepting with an unconditional self-loop.
+    std::vector<exprt> error_disjuncts;
+
+    std::map<mp_integer, std::pair<hoat::state_namet, hoat::edgest>> state_map;
+    for(auto &state : hoa.body)
+      state_map[state.first.number] = state;
+
+    for(auto &state : hoa.body)
+    {
+      for(auto &edge : state.second)
+      {
+        if(edge.dest_states.size() != 1)
+          throw ebmc_errort() << "edge must have one destination state";
+        auto dest_state_it = state_map.find(edge.dest_states.front());
+        CHECK_RETURN(dest_state_it != state_map.end());
+        if(is_error_state(dest_state_it->second))
+        {
+          auto pre = equal_exprt{
+            buechi_state, from_integer(state.first.number, state_type)};
+          auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string);
+          error_disjuncts.push_back(and_exprt{pre, cond});
+        }
+      }
+    }
+
+    auto error_signal = disjunction(error_disjuncts);
+
+    message.debug() << "Buechi error signal: " << format(error_signal)
+                    << messaget::eom;
+
     // construct the transition relation
     std::vector<exprt> trans_disjuncts;
 
@@ -183,6 +232,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
       buechi_state,
       std::move(init),
       std::move(trans),
+      std::move(error_signal),
       std::move(liveness_signal)};
   }
   catch(ltl_sva_to_string_unsupportedt error)

src/temporal-logic/ltl_to_buechi.h

@@ -17,16 +17,19 @@ struct buechi_transt
 
   exprt init;
   exprt trans;
+  exprt error_signal;
   exprt liveness_signal;
 
   buechi_transt(
     symbol_exprt __state_symbol,
     exprt __init,
     exprt __trans,
+    exprt __error_signal,
     exprt __liveness_signal)
     : state_symbol(std::move(__state_symbol)),
       init(std::move(__init)),
       trans(std::move(__trans)),
+      error_signal(std::move(__error_signal)),
       liveness_signal(std::move(__liveness_signal))
   {
   }