From 28e4383aba81931c06c6c73ce4ce41747db1375c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 6 Aug 2025 09:51:17 -0700
Subject: [PATCH] Buechi: identify special cases where reachability is
 sufficient
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds treatment for the special case where all nonaccepting states of
the Buechi automaton have an unconditional self-loop.

In this case, when these nonaccepting states is reached, the trace cannot be
extended to an accepting trace, and will hence be rejected.

Hence, in this case, the Buechi acceptance condition is unnecessary, and a
simple reachability property is sufficient.

Among the 74 tests in regression/ebmc-spot/sva-buechi, only 3 require the
Büchi acceptance condition with this change applied.
---
 regression/ebmc-spot/sva-buechi/initial2.desc |  4 +-
 .../ebmc-spot/sva-buechi/static_final1.desc   |  2 +-
 src/ebmc/instrument_buechi.cpp                | 12 +++++
 src/temporal-logic/ltl_to_buechi.cpp          | 45 ++++++++++++++-----
 4 files changed, 49 insertions(+), 14 deletions(-)

diff --git a/regression/ebmc-spot/sva-buechi/initial2.desc b/regression/ebmc-spot/sva-buechi/initial2.desc
index 019005220..d7a98733e 100644
--- a/regression/ebmc-spot/sva-buechi/initial2.desc
+++ b/regression/ebmc-spot/sva-buechi/initial2.desc
@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/initial2.sv
 --buechi --module main
-^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound \d+$
-^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound \d+$
+^\[main\.assert\.1\] main\.counter == 1: PROVED \(1-induction\)$
+^\[main\.assert\.2\] main\.counter == 2: PROVED \(1-induction\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/static_final1.desc b/regression/ebmc-spot/sva-buechi/static_final1.desc
index b3d1c6084..355f116c2 100644
--- a/regression/ebmc-spot/sva-buechi/static_final1.desc
+++ b/regression/ebmc-spot/sva-buechi/static_final1.desc
@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/static_final1.sv
 --buechi
-^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound \d+$
+^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED \(1-induction\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp
index 22e9c1126..b17db5b10 100644
--- a/src/ebmc/instrument_buechi.cpp
+++ b/src/ebmc/instrument_buechi.cpp
@@ -68,19 +68,31 @@ void instrument_buechi(
     // by the Buechi acceptance condition.
     exprt::operandst property_conjuncts;
 
+    bool have_liveness = false, have_safety = false;
+
     if(!buechi.liveness_signal.is_false())
     {
       // Note that we have negated the property,
       // so this is the negation of the Buechi acceptance condition.
       property_conjuncts.push_back(
         F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}});
+      have_liveness = true;
     }
 
     if(!buechi.error_signal.is_true())
     {
       property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
+      have_safety = true;
     }
 
+    if(have_liveness && have_safety)
+      message.debug() << "Buechi automaton has liveness and safety components"
+                      << messaget::eom;
+    else if(have_liveness)
+      message.debug() << "Buechi automaton is liveness only" << messaget::eom;
+    else if(have_safety)
+      message.debug() << "Buechi automaton is safety only" << messaget::eom;
+
     property.normalized_expr = conjunction(property_conjuncts);
 
     message.debug() << "New property: " << format(property.normalized_expr)
diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp
index 153bf7b8a..2e119b99b 100644
--- a/src/temporal-logic/ltl_to_buechi.cpp
+++ b/src/temporal-logic/ltl_to_buechi.cpp
@@ -100,6 +100,17 @@ bool is_error_state(const std::pair<hoat::state_namet, hoat::edgest> &state)
   return false;
 }
 
+/// Returns true iff all accepting states of the automaton have
+/// unconditional self loops
+bool is_safety_only(const hoat &hoa)
+{
+  for(auto &state : hoa.body)
+    if(state.first.is_accepting() && !is_error_state(state))
+      return false;
+
+  return true;
+}
+
 buechi_transt
 ltl_to_buechi(const exprt &property, message_handlert &message_handler)
 {
@@ -162,20 +173,32 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
     message.debug() << "Buechi initial state: " << format(init)
                     << messaget::eom;
 
-    // construct the liveness signal
-    std::vector<exprt> liveness_disjuncts;
+    exprt liveness_signal;
 
-    for(auto &state : hoa.body)
-      if(state.first.is_accepting())
-      {
-        liveness_disjuncts.push_back(equal_exprt{
-          buechi_state, from_integer(state.first.number, state_type)});
-      }
+    // Is safety sufficient?
+    if(is_safety_only(hoa))
+    {
+      liveness_signal = false_exprt{};
 
-    auto liveness_signal = disjunction(liveness_disjuncts);
+      message.debug() << "Buechi liveness signal not required" << messaget::eom;
+    }
+    else
+    {
+      // construct the liveness signal
+      std::vector<exprt> liveness_disjuncts;
 
-    message.debug() << "Buechi liveness signal: " << format(liveness_signal)
-                    << messaget::eom;
+      for(auto &state : hoa.body)
+        if(state.first.is_accepting())
+        {
+          liveness_disjuncts.push_back(equal_exprt{
+            buechi_state, from_integer(state.first.number, state_type)});
+        }
+
+      liveness_signal = disjunction(liveness_disjuncts);
+
+      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.