SVA/LTL property instrumentation

CHANGELOG

@@ -5,6 +5,7 @@
   use --bmc-with-assumptions to re-enable the previous algorithm.
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 * SystemVerilog: set membership operator
+* word-level BMC: LTL/SVA to Buechi with --buechi
 
 # EBMC 5.3
 

regression/ebmc/Buechi/FGp1.desc

@@ -0,0 +1,9 @@
+CORE
+FGp1.smv
+--buechi --bound 2
+^\[.*\] F G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/FGp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F G p

regression/ebmc/Buechi/Fp1.desc

@@ -0,0 +1,9 @@
+CORE
+Fp1.smv
+--buechi --bound 2
+^\[.*\] F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/Fp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F p

regression/ebmc/Buechi/GFp1.desc

@@ -0,0 +1,9 @@
+CORE
+GFp1.smv
+--buechi --bound 2
+^\[.*\] G F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/GFp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := !p;
+
+-- should pass
+LTLSPEC G F p

regression/ebmc/Buechi/Gp1.desc

@@ -0,0 +1,9 @@
+CORE
+Gp1.smv
+--buechi --bound 2
+^\[.*\] G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/Gp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC G p

regression/ebmc/Buechi/Xp1.desc

@@ -0,0 +1,9 @@
+CORE
+Xp1.smv
+--buechi --bound 2
+^\[.*\] X p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/Xp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC X p

regression/ebmc/Buechi/and1.desc

@@ -0,0 +1,9 @@
+CORE
+and1.smv
+--buechi --bound 2
+^\[.*\] X p & X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/and1.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X p & X q
+

regression/ebmc/Buechi/and2.desc

@@ -0,0 +1,9 @@
+CORE
+and2.smv
+--buechi --bound 2
+^\[.*\] X \(p & q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/and2.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X (p & q)
+

regression/ebmc/Buechi/iff1.desc

@@ -0,0 +1,9 @@
+CORE
+iff1.smv
+--buechi --bound 2
+^\[.*\] X p <-> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/iff1.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p <-> X q

regression/ebmc/Buechi/iff2.desc

@@ -0,0 +1,9 @@
+CORE
+iff2.smv
+--buechi --bound 2
+^\[.*\] X \(p <-> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/iff2.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p <-> q)

regression/ebmc/Buechi/implies1.desc

@@ -0,0 +1,9 @@
+CORE
+implies1.smv
+--buechi --bound 2
+^\[.*\] X p -> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/implies1.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p -> X q

regression/ebmc/Buechi/implies2.desc

@@ -0,0 +1,9 @@
+CORE
+implies2.smv
+--buechi --bound 2
+^\[.*\] X \(p -> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/implies2.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p -> q)

regression/ebmc/Buechi/or1.desc

@@ -0,0 +1,9 @@
+CORE
+or1.smv
+--buechi --bound 2
+^\[.*\] X p \| X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/or1.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p | X q

regression/ebmc/Buechi/or2.desc

@@ -0,0 +1,9 @@
+CORE
+or2.smv
+--buechi --bound 2
+^\[.*\] X \(p \| q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/Buechi/or2.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p | q)

src/ebmc/Makefile

@@ -15,6 +15,7 @@ SRC = \
       ebmc_parse_options.cpp \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
+      instrument_buechi.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
       live_signal.cpp \

src/ebmc/ebmc_parse_options.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_error.h"
 #include "ebmc_version.h"
 #include "ic3_engine.h"
+#include "instrument_buechi.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
 #include "property_checker.h"
@@ -241,7 +242,14 @@ int ebmc_parse_optionst::doit()
       if(result != -1)
         return result;
 
-      // possibly apply liveness-to-safety
+      // LTL/SVA to Buechi?
+      if(cmdline.isset("buechi"))
+        instrument_buechi(
+          ebmc_base.transition_system,
+          ebmc_base.properties,
+          ui_message_handler);
+
+      // Liveness to safety?
       if(cmdline.isset("liveness-to-safety"))
         liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
 
@@ -366,6 +374,7 @@ void ebmc_parse_optionst::help()
     " {y--systemverilog}             \t force SystemVerilog instead of Verilog\n"
     " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
+    " {y--buechi}                    \t translate LTL/SVA properties to Buechi acceptance\n"
     "\n"
     "Methods:\n"
     " {y--k-induction}               \t do k-induction with k=bound\n"

src/ebmc/ebmc_parse_options.h

@@ -48,7 +48,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(bmc-with-assumptions)"
-        "(liveness-to-safety)"
+        "(liveness-to-safety)(buechi)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",
         argc,

src/ebmc/instrument_buechi.cpp

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Buechi Automaton Instrumentation
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "instrument_buechi.h"
+
+#include <temporal-logic/ltl.h>
+#include <temporal-logic/ltl_to_buechi.h>
+#include <temporal-logic/temporal_logic.h>
+
+void instrument_buechi(
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
+{
+  for(auto &property : properties.properties)
+  {
+    if(!property.is_unknown())
+      continue;
+
+    // This is for LTL and some fragment of SVA only.
+    if(
+      !is_LTL(property.normalized_expr) &&
+      !is_Buechi_SVA(property.normalized_expr))
+    {
+      continue;
+    }
+
+    messaget message(message_handler);
+    message.debug() << "Translating " << property.description << " to Buechi"
+                    << messaget::eom;
+
+    // make the automaton for the negation of the property
+    auto buechi = ltl_to_buechi(
+      not_exprt{property.normalized_expr}, "buechi::", message_handler);
+
+    // add the automaton to the transition system
+    transition_system.trans_expr.init() =
+      and_exprt{transition_system.trans_expr.init(), buechi.init};
+
+    transition_system.trans_expr.trans() =
+      and_exprt{transition_system.trans_expr.trans(), buechi.trans};
+
+    // replace the normalized property expression
+    property.normalized_expr = G_exprt{F_exprt{buechi.liveness_signal}};
+  }
+}

src/ebmc/instrument_buechi.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Buechi Automaton Instrumentation
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Buechi Automaton Instrumentation
+
+#ifndef EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H
+#define EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H
+
+#include <util/message.h>
+
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+void instrument_buechi(
+  transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);
+
+#endif // EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H

src/temporal-logic/Makefile

@@ -1,4 +1,7 @@
-SRC = nnf.cpp \
+SRC = hoa.cpp \
+      ltl_to_buechi.cpp \
+      ltl_sva_to_string.cpp \
+      nnf.cpp \
       normalize_property.cpp \
       temporal_logic.cpp \
       trivial_sva.cpp \

src/temporal-logic/hoa.h

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+Module: Hanoi Omega Automata (HOA) Format
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_HOA_H
+#define CPROVER_TEMPORAL_LOGIC_HOA_H
+
+#include <util/irep.h>
+#include <util/mp_arith.h>
+
+#include <list>
+#include <map>
+#include <string>
+
+// https://adl.github.io/hoaf/hoaf.pdf
+class hoat
+{
+public:
+  // header
+  using headert = std::list<std::pair<std::string, std::list<std::string>>>;
+  headert header;
+
+  // body
+  using labelt = irept;
+  using acc_sigt = std::vector<std::string>;
+  struct state_namet
+  {
+    mp_integer number;
+    labelt label;
+    acc_sigt acc_sig;
+  };
+  struct edget
+  {
+    labelt label;
+    std::vector<mp_integer> dest_states;
+    acc_sigt acc_sig;
+  };
+  using edgest = std::list<edget>;
+  using bodyt = std::list<std::pair<state_namet, edgest>>;
+  bodyt body;
+
+  hoat(headert _header, bodyt _body)
+    : header(std::move(_header)), body(std::move(_body))
+  {
+  }
+
+  static hoat from_string(const std::string &);
+  void output(std::ostream &) const;
+
+  friend std::ostream &operator<<(std::ostream &out, const hoat &hoa)
+  {
+    hoa.output(out);
+    return out;
+  }
+
+  mp_integer max_state_number() const;
+
+  // atomic propositions
+  std::map<mp_integer, std::string> ap_map;
+};
+
+#endif // CPROVER_TEMPORAL_LOGIC_HOA_H

src/temporal-logic/ltl_sva_to_string.cpp

@@ -0,0 +1,116 @@
+/*******************************************************************\
+
+Module: Property Instrumentation via Buechi Automata
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "ltl_sva_to_string.h"
+
+#include "temporal_expr.h"
+
+ltl_sva_to_stringt::resultt
+ltl_sva_to_stringt::prefix(std::string s, const exprt &expr)
+{
+  auto op_rec = to_string_rec(to_unary_expr(expr).op());
+
+  auto new_e = to_unary_expr(expr);
+  new_e.op() = op_rec.e;
+
+  if(op_rec.p != precedencet::INFIX)
+    return resultt{precedencet::PREFIX, s + op_rec.s, new_e};
+  else
+    return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')', new_e};
+}
+
+ltl_sva_to_stringt::resultt
+ltl_sva_to_stringt::infix(std::string s, const exprt &expr)
+{
+  std::string result;
+  bool first = true;
+  exprt new_e = expr; // copy
+
+  for(auto &op : new_e.operands())
+  {
+    if(first)
+      first = false;
+    else
+      result += s;
+
+    auto op_rec = to_string_rec(op);
+    op = op_rec.e;
+
+    if(op_rec.p == precedencet::ATOM)
+      result += op_rec.s;
+    else
+      result += '(' + op_rec.s + ')';
+  }
+
+  return resultt{precedencet::INFIX, result, new_e};
+}
+
+ltl_sva_to_stringt::resultt ltl_sva_to_stringt::to_string_rec(const exprt &expr)
+{
+  if(expr.id() == ID_F)
+  {
+    return prefix("F", expr);
+  }
+  else if(expr.id() == ID_G)
+  {
+    return prefix("G", expr);
+  }
+  else if(expr.id() == ID_X)
+  {
+    return prefix("X", expr);
+  }
+  else if(expr.id() == ID_U)
+  {
+    return infix("U", expr);
+  }
+  else if(expr.id() == ID_weak_U)
+  {
+    return infix("W", expr);
+  }
+  else if(expr.id() == ID_R)
+  {
+    return infix("R", expr);
+  }
+  else if(expr.id() == ID_strong_R)
+  {
+    return infix("M", expr);
+  }
+  else if(expr.id() == ID_and)
+  {
+    return infix("&", expr);
+  }
+  else if(expr.id() == ID_or)
+  {
+    return infix("|", expr);
+  }
+  else if(expr.id() == ID_xor)
+  {
+    return infix(" xor ", expr);
+  }
+  else if(expr.id() == ID_implies)
+  {
+    return infix("->", expr);
+  }
+  else if(expr.id() == ID_not)
+  {
+    return prefix("!", expr);
+  }
+  else
+  {
+    auto number = atoms.number(expr);
+    std::string s;
+    if(number <= 'z' - 'a')
+      s = std::string(1, 'a' + number);
+    else
+      s = "a" + std::to_string(number);
+
+    symbol_exprt new_e{s, expr.type()};
+
+    return resultt{precedencet::ATOM, s, new_e};
+  }
+}

src/temporal-logic/ltl_sva_to_string.h

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module: Property Instrumentation via Buechi Automata
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H
+#define CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H
+
+#include <util/expr.h>
+#include <util/numbering.h>
+
+/// create formula strings for external LTL to Buechi tools
+class ltl_sva_to_stringt
+{
+public:
+  enum class precedencet
+  {
+    ATOM,
+    PREFIX,
+    INFIX
+  };
+
+  struct resultt
+  {
+    resultt(precedencet _p, std::string _s, exprt _e)
+      : p(_p), s(std::move(_s)), e(std::move(_e))
+    {
+    }
+    precedencet p;
+    std::string s;
+    exprt e;
+  };
+
+  resultt operator()(const exprt &expr)
+  {
+    return to_string_rec(expr);
+  }
+
+  numberingt<exprt, irep_hash> atoms;
+
+protected:
+  resultt prefix(std::string s, const exprt &);
+  resultt infix(std::string s, const exprt &);
+  resultt to_string_rec(const exprt &);
+};
+
+#endif

src/temporal-logic/ltl_to_buechi.cpp

@@ -0,0 +1,119 @@
+/*******************************************************************\
+
+Module: Property Instrumentation via Buechi Automata
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "ltl_to_buechi.h"
+
+#include <util/arith_tools.h>
+#include <util/format_expr.h>
+#include <util/message.h>
+#include <util/run.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+#include <ebmc/ebmc_error.h>
+#include <trans-word-level/next_symbol.h>
+
+#include "hoa.h"
+#include "ltl_sva_to_string.h"
+
+#include <sstream>
+
+buechi_transt ltl_to_buechi(
+  const exprt &property,
+  const std::string &identifier_prefix,
+  message_handlert &message_handler)
+{
+  buechi_transt buechi_trans;
+
+  // Turn the skeleton of the property into a string
+  auto string = ltl_sva_to_stringt{}(property);
+
+  // Run Spot's ltl2tgba
+  std::ostringstream hoa_stream;
+
+  messaget message(message_handler);
+
+  // state-based Buchi acceptance
+  auto run_result = run(
+    "ltl2tgba",
+    {"ltl2tgba", "--sba", "--hoaf=1.1", string.s},
+    "",
+    hoa_stream,
+    "");
+
+  if(run_result != 0)
+    throw ebmc_errort{} << "failed to run ltl2tgba";
+
+  auto hoa = hoat::from_string(hoa_stream.str());
+
+  message.debug() << hoa << messaget::eom;
+
+  auto max_state_number = hoa.max_state_number();
+  auto state_type = range_typet{0, max_state_number};
+  const auto buechi_state =
+    symbol_exprt{identifier_prefix + "state", state_type};
+  const auto buechi_next_state =
+    next_symbol_exprt{identifier_prefix + "state", state_type};
+
+  // construct the initial state constraint
+  std::vector<exprt> init_disjuncts;
+
+  for(auto &item : hoa.header)
+    if(item.first == "Start:")
+    {
+      if(item.second.size() != 1)
+        throw ebmc_errort() << "Start header must have one token";
+      auto state_number = string2integer(item.second.front());
+      init_disjuncts.push_back(
+        equal_exprt{buechi_state, from_integer(state_number, state_type)});
+    }
+
+  buechi_trans.init = disjunction(init_disjuncts);
+
+  message.debug() << "Buechi initial state: " << format(buechi_trans.init)
+                  << messaget::eom;
+
+  // construct the liveness signal
+  std::vector<exprt> liveness_disjuncts;
+
+  for(auto &state : hoa.body)
+    if(!state.first.acc_sig.empty())
+    {
+      liveness_disjuncts.push_back(equal_exprt{
+        buechi_state, from_integer(state.first.number, state_type)});
+    }
+
+  buechi_trans.liveness_signal = disjunction(liveness_disjuncts);
+
+  message.debug() << "Buechi liveness signal: "
+                  << format(buechi_trans.liveness_signal) << messaget::eom;
+
+  // construct the transition relation
+  std::vector<exprt> trans_disjuncts;
+
+  for(auto &state : hoa.body)
+  {
+    auto pre =
+      equal_exprt{buechi_state, from_integer(state.first.number, state_type)};
+    for(auto &edge : state.second)
+    {
+      if(edge.dest_states.size() != 1)
+        throw ebmc_errort() << "edge must have one destination state";
+      auto post = equal_exprt{
+        buechi_next_state, from_integer(edge.dest_states.front(), state_type)};
+      trans_disjuncts.push_back(and_exprt{pre, post});
+    }
+  }
+
+  buechi_trans.trans = disjunction(trans_disjuncts);
+
+  message.debug() << "Buechi transition constraint: "
+                  << format(buechi_trans.trans) << messaget::eom;
+
+  return buechi_trans;
+}

src/temporal-logic/ltl_to_buechi.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Property Instrumentation via Buechi Automata
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_LTL_TO_BUECHI_H
+#define CPROVER_EBMC_LTL_TO_BUECHI_H
+
+#include <util/expr.h>
+
+struct buechi_transt
+{
+  exprt init;
+  exprt trans;
+  exprt liveness_signal;
+};
+
+class message_handlert;
+
+buechi_transt ltl_to_buechi(
+  const exprt &formula,
+  const std::string &identifier_prefix,
+  message_handlert &);
+
+#endif

src/temporal-logic/temporal_logic.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/expr_util.h>
 
+#include "ltl.h"
+
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
@@ -63,6 +65,11 @@ bool is_LTL(const exprt &expr)
   return !has_subexpr(expr, non_LTL_operator);
 }
 
+bool is_Gp(const exprt &expr)
+{
+  return expr.id() == ID_G && !is_temporal_operator(to_G_expr(expr).op());
+}
+
 bool is_SVA_sequence(const exprt &expr)
 {
   auto id = expr.id();
@@ -105,3 +112,11 @@ bool is_SVA(const exprt &expr)
 
   return !has_subexpr(expr, non_SVA_operator);
 }
+
+bool is_Buechi_SVA(const exprt &expr)
+{
+  auto unsupported_operator = [](const exprt &expr)
+  { return is_temporal_operator(expr) && !is_SVA_operator(expr); };
+
+  return !has_subexpr(expr, unsupported_operator);
+}

src/temporal-logic/temporal_logic.h

@@ -35,6 +35,9 @@ bool has_CTL_operator(const exprt &);
 /// Returns true iff the given expression is an LTL formula
 bool is_LTL(const exprt &);
 
+/// Returns true iff the given expression is of the form Gp
+bool is_Gp(const exprt &);
+
 /// Returns true iff the given expression has an LTL operator
 /// as its root
 bool is_LTL_operator(const exprt &);
@@ -48,4 +51,8 @@ bool is_SVA_operator(const exprt &);
 /// Returns true iff the given expression is an SVA expression
 bool is_SVA(const exprt &);
 
+/// Returns true iff the given expression is an SVA expression that
+/// we can convert into a Buechi automaton
+bool is_Buechi_SVA(const exprt &);
+
 #endif

unit/Makefile

@@ -4,7 +4,8 @@
 SRC = unit_tests.cpp
 
 # Test source files
-SRC += temporal-logic/nnf.cpp \
+SRC += temporal-logic/ltl_sva_to_string.cpp \
+       temporal-logic/nnf.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src

unit/temporal-logic/ltl_sva_to_string.cpp

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Property Instrumentation via Buechi Automata
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <temporal-logic/ltl.h>
+#include <temporal-logic/ltl_sva_to_string.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("Generating a string from a formula")
+{
+  GIVEN("A formula")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+    auto q = symbol_exprt{"q", bool_typet{}};
+    REQUIRE(ltl_sva_to_stringt{}(p).s == "a");
+    REQUIRE(ltl_sva_to_stringt{}(not_exprt{G_exprt{p}}).s == "!Ga");
+    REQUIRE(ltl_sva_to_stringt{}(X_exprt{F_exprt{p}}).s == "XFa");
+    REQUIRE(ltl_sva_to_stringt{}(U_exprt{X_exprt{p}, q}).s == "(Xa)Ub");
+    REQUIRE(ltl_sva_to_stringt{}(U_exprt{p, q}).s == "aUb");
+    REQUIRE(ltl_sva_to_stringt{}(and_exprt{p, q}).s == "a&b");
+  }
+}