BMC: extend CTL fragment

This extends the fragment of CTL that is accepted by the BMC engine.

Author: kroening

regression/ebmc/smv/smv_ctlspec_F1.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+smv_ctlspec_F1.smv
+--bound 10
+^\[.*\] AF x = 0: REFUTED$
+^\[.*\] AF x = 1: PROVED up to bound 10$
+^\[.*\] AF x = 2: PROVED up to bound 10$
+^\[.*\] AF x = 1 & AF x = 2: PROVED up to bound 10$
+^\[.*\] AF x = 0 & AF x = 1: REFUTED$
+^\[.*\] EF x = 0: FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ctlspec_F1.smv

@@ -0,0 +1,19 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+SPEC AF x = 0 -- should fail
+SPEC AF x = 1 -- should pass
+SPEC AF x = 2 -- should pass
+SPEC AF x = 1 & AF x = 2 -- should pass
+SPEC AF x = 0 & AF x = 1 -- should fail
+SPEC EF x = 0 -- not supported

regression/ebmc/smv/smv_ctlspec_G1.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+smv_ctlspec_G1.smv
+--bound 10
+^\[.*\] AG x != 5: PROVED up to bound 10$
+^\[.*\] AG x != 6: PROVED up to bound 10$
+^\[.*\] AG x != 2: REFUTED$
+^\[.*\] AG x != 5 & AG x != 6: PROVED up to bound 10$
+^\[.*\] AG x != 2 & AG x != 5: REFUTED$
+^\[.*\] EG x != 2: FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/smv/smv_ctlspec_G1.smv

@@ -0,0 +1,19 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+SPEC AG x != 5 -- should pass
+SPEC AG x != 6 -- should pass
+SPEC AG x != 2 -- should fail
+SPEC AG x != 5 & AG x != 6 -- should pass
+SPEC AG x != 2 & AG x != 5 -- should fail
+SPEC EG x != 2 -- not supported

src/temporal-logic/temporal_logic.cpp

@@ -34,6 +34,11 @@ bool is_CTL_operator(const exprt &expr)
          id == ID_AR || id == ID_ER;
 }
 
+bool has_CTL_operator(const exprt &expr)
+{
+  return has_subexpr(expr, is_CTL_operator);
+}
+
 bool is_CTL(const exprt &expr)
 {
   auto non_CTL_operator = [](const exprt &expr) {

src/temporal-logic/temporal_logic.h

@@ -29,6 +29,9 @@ bool is_CTL(const exprt &);
 /// as its root
 bool is_CTL_operator(const exprt &);
 
+/// Returns true iff the given expression contains a CTL operator
+bool has_CTL_operator(const exprt &);
+
 /// Returns true iff the given expression is an LTL formula
 bool is_LTL(const exprt &);
 

src/trans-word-level/property.cpp

@@ -93,42 +93,39 @@ Function: bmc_supports_CTL_property
 
 bool bmc_supports_CTL_property(const exprt &expr)
 {
-  // We support
-  // * formulas that contain no temporal operator besides AX
-  // * GFφ, where φ contains no temporal operator besides AX
-  // * AFφ, where φ contains no temporal operator besides AX
-  // * AGAFφ, where φ contains no temporal operator besides AX
-  // * conjunctions of supported CTL properties
-  auto non_AX_CTL_operator = [](const exprt &expr)
-  { return is_CTL_operator(expr) && expr.id() != ID_AX; };
-
-  if(!has_subexpr(expr, non_AX_CTL_operator))
+  // We map a subset of ACTL to LTL, following
+  // Monika Maidl. "The common fragment of CTL and LTL"
+  // http://dx.doi.org/10.1109/SFCS.2000.892332
+  //
+  // Specificially, we allow
+  // * state predicates
+  // * conjunctions of allowed formulas
+  // * AX φ, where φ is allowed
+  // * AF φ, where φ is allowed
+  // * AG φ, where φ is allowed
+  if(!has_CTL_operator(expr))
   {
     return true;
   }
-  else if(expr.id() == ID_AF)
-  {
-    return !has_subexpr(to_AF_expr(expr).op(), non_AX_CTL_operator);
-  }
-  else if(expr.id() == ID_AG)
-  {
-    auto &op = to_AG_expr(expr).op();
-    if(op.id() == ID_AF)
-    {
-      return !has_subexpr(to_AF_expr(op).op(), non_AX_CTL_operator);
-    }
-    else
-    {
-      return !has_subexpr(op, non_AX_CTL_operator);
-    }
-  }
   else if(expr.id() == ID_and)
   {
     for(auto &op : expr.operands())
       if(!bmc_supports_CTL_property(op))
         return false;
     return true;
   }
+  else if(expr.id() == ID_AX)
+  {
+    return bmc_supports_CTL_property(to_AX_expr(expr).op());
+  }
+  else if(expr.id() == ID_AF)
+  {
+    return bmc_supports_CTL_property(to_AF_expr(expr).op());
+  }
+  else if(expr.id() == ID_AG)
+  {
+    return bmc_supports_CTL_property(to_AG_expr(expr).op());
+  }
   else
     return false;
 }