Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
SVA/LTL property instrumentation
Browse files Browse the repository at this point in the history
kroening committed Nov 26, 2024
1 parent d3d0bcd commit 28db225
Showing 43 changed files with 1,304 additions and 4 deletions.
1 change: 1 addition & 0 deletions CHANGELOG
Original file line number Diff line number Diff line change
@@ -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

9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/FGp1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
FGp1.smv
--buechi --bound 2
^\[.*\] F G p: PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/FGp1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR p : boolean;

ASSIGN init(p) := FALSE;
next(p) := TRUE;

-- should pass
LTLSPEC F G p
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Fp1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Fp1.smv
--buechi --bound 2
^\[.*\] F p: PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Fp1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR p : boolean;

ASSIGN init(p) := FALSE;
next(p) := TRUE;

-- should pass
LTLSPEC F p
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/GFp1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
GFp1.smv
--buechi --bound 2
^\[.*\] G F p: PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/GFp1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR p : boolean;

ASSIGN init(p) := FALSE;
next(p) := !p;

-- should pass
LTLSPEC G F p
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Gp1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Gp1.smv
--buechi --bound 2
^\[.*\] G p: PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Gp1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR p : boolean;

ASSIGN init(p) := TRUE;
next(p) := TRUE;

-- should pass
LTLSPEC G p
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Xp1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Xp1.smv
--buechi --bound 2
^\[.*\] X p: PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/Xp1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR p : boolean;

ASSIGN init(p) := FALSE;
next(p) := TRUE;

-- should pass
LTLSPEC X p
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/and1.desc
Original file line number Diff line number Diff line change
@@ -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
--
15 changes: 15 additions & 0 deletions regression/ebmc/Buechi/and1.smv
Original file line number Diff line number Diff line change
@@ -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

9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/and2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
and2.smv
--buechi --bound 2
^\[.*\] X \(p & q\): PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
15 changes: 15 additions & 0 deletions regression/ebmc/Buechi/and2.smv
Original file line number Diff line number Diff line change
@@ -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)

9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/iff1.desc
Original file line number Diff line number Diff line change
@@ -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
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/iff1.smv
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/iff2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
iff2.smv
--buechi --bound 2
^\[.*\] X \(p <-> q\): PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/iff2.smv
Original file line number Diff line number Diff line change
@@ -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)
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/implies1.desc
Original file line number Diff line number Diff line change
@@ -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
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/implies1.smv
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/implies2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
implies2.smv
--buechi --bound 2
^\[.*\] X \(p -> q\): PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/implies2.smv
Original file line number Diff line number Diff line change
@@ -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)
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/or1.desc
Original file line number Diff line number Diff line change
@@ -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
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/or1.smv
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions regression/ebmc/Buechi/or2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
or2.smv
--buechi --bound 2
^\[.*\] X \(p \| q\): PROVED up to bound 2$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
14 changes: 14 additions & 0 deletions regression/ebmc/Buechi/or2.smv
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions src/ebmc/Makefile
Original file line number Diff line number Diff line change
@@ -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 \
11 changes: 10 additions & 1 deletion src/ebmc/ebmc_parse_options.cpp
Original file line number Diff line number Diff line change
@@ -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"
2 changes: 1 addition & 1 deletion src/ebmc/ebmc_parse_options.h
Original file line number Diff line number Diff line change
@@ -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,
46 changes: 46 additions & 0 deletions src/ebmc/instrument_buechi.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
/*******************************************************************\
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 only.
if(!is_LTL(property.normalized_expr))
continue;

// But ignore Gp
if(is_Gp(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

// replace the normalized property expression
property.normalized_expr = G_exprt{F_exprt{buechi.liveness_signal}};
}
}
25 changes: 25 additions & 0 deletions src/ebmc/instrument_buechi.h
Original file line number Diff line number Diff line change
@@ -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
5 changes: 4 additions & 1 deletion src/temporal-logic/Makefile
Original file line number Diff line number Diff line change
@@ -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 \
530 changes: 530 additions & 0 deletions src/temporal-logic/hoa.cpp

Large diffs are not rendered by default.

62 changes: 62 additions & 0 deletions src/temporal-logic/hoa.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
/*******************************************************************\
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 <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;
};

#endif // CPROVER_TEMPORAL_LOGIC_HOA_H
116 changes: 116 additions & 0 deletions src/temporal-logic/ltl_sva_to_string.cpp
Original file line number Diff line number Diff line change
@@ -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};
}
}
50 changes: 50 additions & 0 deletions src/temporal-logic/ltl_sva_to_string.h
Original file line number Diff line number Diff line change
@@ -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
116 changes: 116 additions & 0 deletions src/temporal-logic/ltl_to_buechi.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
/*******************************************************************\
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 "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};

// 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.liveness_signal) << 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_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;
}
28 changes: 28 additions & 0 deletions src/temporal-logic/ltl_to_buechi.h
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions src/temporal-logic/temporal_logic.cpp
Original file line number Diff line number Diff line change
@@ -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();
3 changes: 3 additions & 0 deletions src/temporal-logic/temporal_logic.h
Original file line number Diff line number Diff line change
@@ -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 &);
3 changes: 2 additions & 1 deletion unit/Makefile
Original file line number Diff line number Diff line change
@@ -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
26 changes: 26 additions & 0 deletions unit/temporal-logic/ltl_sva_to_string.cpp
Original file line number Diff line number Diff line change
@@ -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");
}
}

0 comments on commit 28db225

Please sign in to comment.