Buechi: identify special cases where reachability is sufficient

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.

Author: kroening

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$
 --

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$
 --

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)

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.