LTL/SVA->Buechi: reject error traces early

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

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/case1.sv
+--buechi --bound 20 --numbered-trace
+^\[main\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$
+^Counterexample with 11 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/cover1.sv
+--buechi --bound 10 --numbered-trace
+^\[main\.p0\] cover main\.counter == 1: PROVED$
+^Trace with 2 states:$
+^main\.counter@0 = 0$
+^main\.counter@1 = 1$
+^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/cover2.sv
+--buechi --bound 10 --numbered-trace
+^\[main\.p0\] cover main\.counter == 1: PROVED$
+^Trace with 2 states:$
+^main\.counter@0 = 0$
+^main\.counter@1 = 1$
+^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/cover_sequence1.sv
+--buechi --bound 10 --numbered-trace
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/cover_sequence2.sv
+--buechi --bound 5
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+../../verilog/SVA/cover_sequence3.sv
+--buechi --bound 3
+^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$
+^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$
+^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Trace one too short.

regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+../../verilog/SVA/cover_sequence4.sv
+--buechi --bound 3
+^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$
+^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$
+^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Trace one too short.

regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/disable_iff1.sv
+--buechi --module main --bound 10 --numbered-trace
+^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
+^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED up to bound 10$
+^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^Counterexample with 3 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/empty_sequence1.sv
+--buechi --bound 5
+^\[main\.p0\] 1 \[\*0\]: REFUTED$
+^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$
+^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$
+^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
+^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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/if1.bmc.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/if1.sv
+--buechi --bound 2
+^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED up to bound 2$
+^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/initial1.bmc.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/initial1.sv
+--buechi --bound 5
+^\[main\.p0\] main\.counter == 0: PROVED up to bound 5$
+^\[main\.p1\] main\.counter == 100: REFUTED$
+^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$
+^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
+^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 5$
+^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED up to bound 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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.

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

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence1.sv
+--buechi --bound 20 --numbered-trace
+^\[main\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
+^Counterexample with 10 states:$
+^main\.x@0 = 0$
+^main\.x@9 = 9$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_and3.sv
+--buechi --bound 5
+^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 2: REFUTED$
+^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 2: REFUTED$
+^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$
+^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_or1.bmc.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_or1.sv
+--buechi --bound 5
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED up to bound \d+$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED up to bound \d+$
+^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$
+^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition1.bdd.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sequence_repetition1.sv
+--buechi --bdd
+^\[.*\] main\.half_x == 0 \[\*2\]: PROVED$
+^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
+^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc

@@ -0,0 +1,14 @@
+CORE
+../../verilog/SVA/sequence_repetition1.sv
+--buechi --bound 10
+^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$
+^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$
+^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$
+^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
+^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$
+^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition3.bmc.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_repetition3.sv
+--buechi --bound 10
+^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED up to bound 10$
+^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED up to bound 10$
+^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sva_abort1.bmc.desc

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sva_abort1.sv
+--buechi --module main --bound 10
+^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
+^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED up to bound 10$
+^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$
+^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cover1.desc

@@ -11,4 +11,3 @@ cover1.sv
 --
 ^warning: ignoring
 --
-Back-end support is missing.

regression/verilog/SVA/if1.desc

@@ -8,4 +8,3 @@ if1.sv
 --
 ^warning: ignoring
 --
-SMT-back end doesn't do cast from bool to bool.

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(
   }
 }
 
+// a nonaccepting 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)
 {
@@ -144,7 +163,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 +174,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 +233,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)