diff --git a/regression/ebmc/Buechi/FGp1.desc b/regression/ebmc/Buechi/FGp1.desc new file mode 100644 index 00000000..bc71b789 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/FGp1.smv b/regression/ebmc/Buechi/FGp1.smv new file mode 100644 index 00000000..0dd410b7 --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/Fp1.desc b/regression/ebmc/Buechi/Fp1.desc new file mode 100644 index 00000000..25032d4f --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/Fp1.smv b/regression/ebmc/Buechi/Fp1.smv new file mode 100644 index 00000000..4c220d22 --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/GFp1.desc b/regression/ebmc/Buechi/GFp1.desc new file mode 100644 index 00000000..878331a9 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/GFp1.smv b/regression/ebmc/Buechi/GFp1.smv new file mode 100644 index 00000000..cd99bc0f --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/Gp1.desc b/regression/ebmc/Buechi/Gp1.desc new file mode 100644 index 00000000..87af6367 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/Gp1.smv b/regression/ebmc/Buechi/Gp1.smv new file mode 100644 index 00000000..d0fcb3ab --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/Xp1.desc b/regression/ebmc/Buechi/Xp1.desc new file mode 100644 index 00000000..75c6937f --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/Xp1.smv b/regression/ebmc/Buechi/Xp1.smv new file mode 100644 index 00000000..424cf3f0 --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/and1.desc b/regression/ebmc/Buechi/and1.desc new file mode 100644 index 00000000..ff3daa95 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/and1.smv b/regression/ebmc/Buechi/and1.smv new file mode 100644 index 00000000..fa313d5e --- /dev/null +++ b/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 + diff --git a/regression/ebmc/Buechi/and2.desc b/regression/ebmc/Buechi/and2.desc new file mode 100644 index 00000000..ae9c56f2 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/and2.smv b/regression/ebmc/Buechi/and2.smv new file mode 100644 index 00000000..3ad65c69 --- /dev/null +++ b/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) + diff --git a/regression/ebmc/Buechi/iff1.desc b/regression/ebmc/Buechi/iff1.desc new file mode 100644 index 00000000..bde2e436 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/iff1.smv b/regression/ebmc/Buechi/iff1.smv new file mode 100644 index 00000000..6fc3d251 --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/iff2.desc b/regression/ebmc/Buechi/iff2.desc new file mode 100644 index 00000000..737e3edc --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/iff2.smv b/regression/ebmc/Buechi/iff2.smv new file mode 100644 index 00000000..6af00543 --- /dev/null +++ b/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) diff --git a/regression/ebmc/Buechi/implies1.desc b/regression/ebmc/Buechi/implies1.desc new file mode 100644 index 00000000..d90489e7 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/implies1.smv b/regression/ebmc/Buechi/implies1.smv new file mode 100644 index 00000000..4651e134 --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/implies2.desc b/regression/ebmc/Buechi/implies2.desc new file mode 100644 index 00000000..d574e71c --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/implies2.smv b/regression/ebmc/Buechi/implies2.smv new file mode 100644 index 00000000..345654ca --- /dev/null +++ b/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) diff --git a/regression/ebmc/Buechi/or1.desc b/regression/ebmc/Buechi/or1.desc new file mode 100644 index 00000000..63337efa --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/or1.smv b/regression/ebmc/Buechi/or1.smv new file mode 100644 index 00000000..35a424fd --- /dev/null +++ b/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 diff --git a/regression/ebmc/Buechi/or2.desc b/regression/ebmc/Buechi/or2.desc new file mode 100644 index 00000000..82e0c51a --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc/Buechi/or2.smv b/regression/ebmc/Buechi/or2.smv new file mode 100644 index 00000000..b037a3c4 --- /dev/null +++ b/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) diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index 68f93133..109be310 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "bmc.h" #include +#include #include #include @@ -20,6 +21,7 @@ Author: Daniel Kroening, dkr@amazon.com void bmc( std::size_t bound, bool convert_only, + bool buechi, const transition_systemt &transition_system, ebmc_propertiest &properties, const ebmc_solver_factoryt &solver_factory, @@ -46,6 +48,12 @@ void bmc( if(property.is_disabled() || property.is_failure()) continue; + // LTL/SVA to Buechi? + if(buechi) + { + auto buechi = ltl_to_buechi(property.normalized_expr); + } + // Is it supported by the BMC engine? if(!bmc_supports_property(property.normalized_expr)) { diff --git a/src/ebmc/bmc.h b/src/ebmc/bmc.h index 33536a67..b8092c55 100644 --- a/src/ebmc/bmc.h +++ b/src/ebmc/bmc.h @@ -22,6 +22,7 @@ class transition_systemt; void bmc( std::size_t bound, bool convert_only, + bool buechi, const transition_systemt &, ebmc_propertiest &, const ebmc_solver_factoryt &, diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index f2a30cec..86234beb 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -241,7 +241,6 @@ int ebmc_parse_optionst::doit() if(result != -1) return result; - // possibly apply liveness-to-safety if(cmdline.isset("liveness-to-safety")) liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties); @@ -366,6 +365,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" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 5929d086..09667edd 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -46,7 +46,7 @@ class ebmc_parse_optionst:public parse_options_baset "(compute-ct)(dot-netlist)(smv-netlist)(vcd):" "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" - "(liveness-to-safety)" + "(liveness-to-safety)(buechi)" "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" "(warn-implicit-nets)", argc, diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index c90b73b4..bb709602 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -202,7 +202,8 @@ void k_inductiont::induction_base() bmc( k, - false, + false, // convert_only + false, // buechi transition_system, properties, solver_factory, diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index d0b8373a..b8affdcf 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -83,6 +83,7 @@ property_checker_resultt word_level_bmc( bmc( bound, convert_only, + cmdline.isset("buechi"), transition_system, properties, solver_factory, diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index 2cb1e020..3f97da6b 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -1,4 +1,5 @@ -SRC = nnf.cpp \ +SRC = ltl_to_buechi.cpp \ + nnf.cpp \ normalize_property.cpp \ temporal_logic.cpp \ trivial_sva.cpp \ diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp new file mode 100644 index 00000000..cadb5dc8 --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -0,0 +1,160 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ltl_to_buechi.h" + +#include + +#include + +#include "temporal_expr.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 atoms; + +protected: + resultt 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}; + } + + resultt 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}; + } + + resultt to_string_rec(const exprt &); +}; + +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}; + } +} + +#include + +buechi_transt ltl_to_buechi(const exprt &property) +{ + std::cout << "FORMULA: " << ltl_sva_to_stringt{}(property).s << '\n'; + return buechi_transt{}; +} diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h new file mode 100644 index 00000000..4b3adf60 --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +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 + +struct buechi_transt +{ + exprt init; + exprt trans; + exprt liveness_signal; +}; + +buechi_transt ltl_to_buechi(const exprt &); + +#endif