LTL to CTL conversion

This adds conversion from a fragment of LTL to CTL, for the benefit of the
BDD engine.

Author: kroening

regression/smv/smv/bdd_unsupported_property.desc

@@ -3,7 +3,7 @@ bdd_unsupported_property.smv
 --bdd
 ^EXIT=10$
 ^SIGNAL=0$
-^\[spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
+^\[spec1\] G x \| F x: FAILURE: property not supported by BDD engine$
 ^\[spec2\] G x = FALSE: REFUTED$
 --
 ^warning: ignoring

regression/smv/smv/bdd_unsupported_property.smv

@@ -4,5 +4,5 @@ VAR x : boolean;
 
 ASSIGN init(x) := TRUE;
 
-LTLSPEC !G x=FALSE
+LTLSPEC G x | F x
 LTLSPEC G x=FALSE

src/ebmc/bdd_engine.cpp

@@ -458,7 +458,7 @@ bool bdd_enginet::property_supported(const exprt &expr)
   if(is_LTL(expr))
   {
     // We can map selected path properties to CTL.
-    return is_Gp(expr) || is_GFp(expr);
+    return LTL_to_CTL(expr).has_value();
   }
 
   if(is_SVA(expr))
@@ -514,23 +514,6 @@ void bdd_enginet::check_property(propertyt &property)
   message.status() << "Checking " << property.name << messaget::eom;
   property.status=propertyt::statust::UNKNOWN;
 
-  // Our engine knows CTL only.
-  // We map selected path properties to CTL.
-
-  if(is_Gp(property.normalized_expr))
-  {
-    // G p --> AG  p
-    auto p = to_G_expr(property.normalized_expr).op();
-    property.normalized_expr = AG_exprt{p};
-  }
-
-  if(is_GFp(property.normalized_expr))
-  {
-    // G F p --> AG AF p
-    auto p = to_F_expr(to_G_expr(property.normalized_expr).op()).op();
-    property.normalized_expr = AG_exprt{AF_exprt{p}};
-  }
-
   if(
     property.normalized_expr.id() == ID_sva_always &&
     to_sva_always_expr(property.normalized_expr).op().id() ==
@@ -555,6 +538,18 @@ void bdd_enginet::check_property(propertyt &property)
     property.normalized_expr = AG_exprt{p};
   }
 
+  // Our engine knows CTL only.
+  // We map selected path properties to CTL.
+  if(
+    has_temporal_operator(property.normalized_expr) &&
+    is_LTL(property.normalized_expr))
+  {
+    auto CTL_opt = LTL_to_CTL(property.normalized_expr);
+    CHECK_RETURN(CTL_opt.has_value());
+    property.normalized_expr = CTL_opt.value();
+    CHECK_RETURN(is_CTL(property.normalized_expr));
+  }
+
   if(is_AGp(property.normalized_expr))
   {
     check_AGp(property);

src/temporal-logic/temporal_logic.cpp

@@ -12,6 +12,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <verilog/sva_expr.h>
 
+#include "ctl.h"
+#include "ltl.h"
+
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
@@ -152,3 +155,58 @@ bool is_SVA_always_s_eventually_p(const exprt &expr)
          !has_temporal_operator(
            to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op());
 }
+
+std::optional<exprt> LTL_to_CTL(exprt expr)
+{
+  // We map a subset of LTL to ACTL, 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
+  // * X φ, where φ is allowed
+  // * F φ, where φ is allowed
+  // * G φ, where φ is allowed
+  if(!has_temporal_operator(expr))
+  {
+    return expr;
+  }
+  else if(expr.id() == ID_and)
+  {
+    for(auto &op : expr.operands())
+    {
+      auto rec = LTL_to_CTL(op);
+      if(!rec.has_value())
+        return {};
+      op = *rec;
+    }
+    return expr;
+  }
+  else if(expr.id() == ID_X)
+  {
+    auto rec = LTL_to_CTL(to_X_expr(expr).op());
+    if(rec.has_value())
+      return AX_exprt{*rec};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_F)
+  {
+    auto rec = LTL_to_CTL(to_F_expr(expr).op());
+    if(rec.has_value())
+      return AF_exprt{*rec};
+    else
+      return {};
+  }
+  else if(expr.id() == ID_G)
+  {
+    auto rec = LTL_to_CTL(to_G_expr(expr).op());
+    if(rec.has_value())
+      return AG_exprt{*rec};
+    else
+      return {};
+  }
+  else
+    return {};
+}

src/temporal-logic/temporal_logic.h

@@ -77,4 +77,8 @@ bool is_SVA_always_p(const exprt &);
 /// Returns true iff the given expression is always s_eventually p
 bool is_SVA_always_s_eventually_p(const exprt &);
 
+/// Turns some fragment of LTL into equivalent CTL, or
+/// returns {} if not possible
+std::optional<exprt> LTL_to_CTL(exprt);
+
 #endif