Merge pull request #450 from diffblue/bmc-Fphi

BMC for F φ

Author: tautschnig

regression/ebmc/smv/bmc_unsupported_property1.desc

@@ -3,7 +3,7 @@ bmc_unsupported_property1.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
+^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$
 ^\[main::spec2\] G main::var::x = FALSE: REFUTED$
 --
 ^warning: ignoring

regression/ebmc/smv/bmc_unsupported_property1.smv

@@ -4,5 +4,5 @@ VAR x : boolean;
 
 ASSIGN init(x) := 1;
 
-LTLSPEC !G x=0
+SPEC EG x=0
 LTLSPEC G x=0

regression/ebmc/smv/bmc_unsupported_property2.desc

@@ -3,7 +3,7 @@ bmc_unsupported_property2.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
+^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$
 ^\[main::spec2\] G main::var::x = TRUE: PROVED up to bound 1$
 --
 ^warning: ignoring

regression/ebmc/smv/bmc_unsupported_property2.smv

@@ -5,5 +5,5 @@ VAR x : boolean;
 ASSIGN init(x) := 1;
 ASSIGN next(x) := x;
 
-LTLSPEC !G x=0 -- unsupported
+SPEC EG x=0 -- unsupported
 LTLSPEC G x=1 -- should pass

regression/ebmc/smv/smv_ltlspec4.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+smv_ltlspec4.smv
+--bound 10 --numbered-trace
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] F main::var::x = 0: REFUTED$
+^main::var::x@0 = 1$
+^main::var::x@1 = 2$
+^main::var::x@2 = 2$
+^\[main::spec2\] F main::var::x = 2: PROVED up to bound 10$
+--
+^warning: ignoring
+--

regression/ebmc/smv/smv_ltlspec4.smv

@@ -0,0 +1,10 @@
+MODULE main
+
+VAR x : 0..2;
+
+ASSIGN
+  init(x) := 1;
+  next(x) := 2;
+
+LTLSPEC F x=0 -- fails
+LTLSPEC F x=2 -- holds

src/temporal-logic/normalize_property.cpp

@@ -36,6 +36,16 @@ exprt normalize_pre_not(not_exprt expr)
   {
     return to_not_expr(op).op();
   }
+  else if(op.id() == ID_G)
+  {
+    // ¬Gφ --> F¬φ
+    return F_exprt{not_exprt{to_G_expr(op).op()}};
+  }
+  else if(op.id() == ID_F)
+  {
+    // ¬Fφ --> G¬φ
+    return G_exprt{not_exprt{to_F_expr(op).op()}};
+  }
 
   return std::move(expr);
 }

src/temporal-logic/normalize_property.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// ¬¬φ --> φ
+/// ¬Gφ --> F¬φ
+/// ¬Fφ --> G¬φ
 exprt normalize_property(exprt);
 
 #endif

src/trans-word-level/property.cpp

@@ -54,6 +54,10 @@ bool bmc_supports_property(const exprt &expr)
     return true;
   else if(expr.id() == ID_G)
     return true;
+  else if(expr.id() == ID_AF)
+    return true;
+  else if(expr.id() == ID_F)
+    return true;
   else if(expr.id() == ID_X)
     return bmc_supports_property(to_X_expr(expr).op());
   else if(expr.id() == ID_sva_always)
@@ -117,6 +121,37 @@ static void property_obligations_rec(
       property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
     }
   }
+  else if(
+    property_expr.id() == ID_AF || property_expr.id() == ID_F ||
+    property_expr.id() == ID_sva_s_eventually)
+  {
+    const auto &phi = to_unary_expr(property_expr).op();
+
+    // Counterexamples to Fφ must have a loop.
+    // We consider l-k loops with l<k.
+    for(mp_integer k = current + 1; k < no_timeframes; ++k)
+    {
+      // The following needs to be satisfied for a counterexample
+      // to Fφ that loops back in timeframe k:
+      //
+      // (1) There is a loop from timeframe k back to
+      //     some earlier state l with current<=l<k.
+      // (2) No state j with current<=j<=k to the end of the
+      //     lasso satisfies 'φ'.
+      for(mp_integer l = current; l < k; ++l)
+      {
+        exprt::operandst disjuncts = {not_exprt(lasso_symbol(l, k))};
+
+        for(mp_integer j = current; j <= k; ++j)
+        {
+          exprt tmp = instantiate(phi, j, no_timeframes, ns);
+          disjuncts.push_back(std::move(tmp));
+        }
+
+        obligations[k].push_back(disjunction(disjuncts));
+      }
+    }
+  }
   else if(
     property_expr.id() == ID_sva_ranged_always ||
     property_expr.id() == ID_sva_s_always)