Merge pull request #1224 from diffblue/safety-only-Buechi

Buechi: identify special cases where reachability is sufficient

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.