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.

Author: kroening

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sequence5.sv
 --buechi
-^\[main\.p0\] 1: PROVED up to bound \d+$
+^\[main\.p0\] 1: PROVED \(1-induction\)$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_and1.sv
 --buechi
-^\[main\.p0\] always \(1 and 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 and 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_iff1.sv
 --buechi
-^\[main\.p0\] always \(1 iff 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 iff 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
 ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_implies1.sv
 --buechi
-^\[main\.p0\] always \(1 implies 1\): PROVED up to bound \d+$
+^\[main\.p0\] always \(1 implies 1\): PROVED \(1-induction\)$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
 ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/sva_not1.sv
 --buechi
-^\[main\.p0] always not 0: PROVED up to bound \d+$
+^\[main\.p0] always not 0: PROVED \(1-induction\)$
 ^\[main\.p1] always not 1: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

src/ebmc/instrument_buechi.cpp

@@ -64,15 +64,24 @@ void instrument_buechi(
     transition_system.trans_expr.trans() =
       and_exprt{transition_system.trans_expr.trans(), buechi.trans};
 
-    // Replace the normalized property expression.
-    // Note that we have negated the property,
-    // so this is the negation of the Buechi acceptance condition.
-    property.normalized_expr =
-      F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}};
+    // Replace the normalized property expression
+    // by the Buechi acceptance condition.
+    exprt::operandst property_conjuncts;
+
+    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}}});
+    }
 
     if(!buechi.error_signal.is_true())
-      property.normalized_expr = and_exprt{
-        property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}};
+    {
+      property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
+    }
+
+    property.normalized_expr = conjunction(property_conjuncts);
 
     message.debug() << "New property: " << format(property.normalized_expr)
                     << messaget::eom;

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)
 {
@@ -159,20 +170,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.