diff --git a/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc b/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc new file mode 100644 index 000000000..df05c054a --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_first_match1.desc @@ -0,0 +1,11 @@ +CORE +../../verilog/SVA/sequence_first_match1.sv +--buechi --bound 5 +^error: failed to convert sva_sequence_first_match$ +^EXIT=6$ +^SIGNAL=0$ +-- +^warning: ignoring +^\[.*\] first_match\(main\.x == 0\): PROVED up to bound 5$ +^\[.*\] first_match\(main\.x == 0, main\.x\+\+\): PROVED up to bound 5$ +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_first_match2.desc b/regression/ebmc-spot/sva-buechi/sequence_first_match2.desc new file mode 100644 index 000000000..35c642a6b --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_first_match2.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sequence_first_match2.sv +--buechi --bound 5 +^error: failed to convert sva_sequence_first_match$ +^EXIT=6$ +^SIGNAL=0$ +-- +^\[.*\] \(\(##1 1\) or \(##2 1\)\) \|-> main.x == 1: REFUTED$ +^\[.*\] first_match\(\(##1 1\) or \(##2 1\)\) \|-> main\.x == 1: PROVED up to bound 5$ +^\[.*\] \(1 or \(##1 1\)\) \|-> main\.x == 0: REFUTED$ +^\[.*\] first_match\(1 or \(##1 1\)\) \|-> main\.x == 0: PROVED up to bound 5$ +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc b/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc new file mode 100644 index 000000000..a40e404fe --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_throughout1.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/sequence_throughout1.sv +--buechi --bound 10 +^error: failed to convert sva_sequence_throughout$ +^EXIT=6$ +^SIGNAL=0$ +-- +^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): PROVED up to bound 10$ +^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): REFUTED$ +^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): REFUTED$ +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_within1.desc b/regression/ebmc-spot/sva-buechi/sequence_within1.desc new file mode 100644 index 000000000..7e842c87a --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_within1.desc @@ -0,0 +1,14 @@ +CORE +../../verilog/SVA/sequence_within1.sv +--buechi --bound 20 +^error: failed to convert sva_sequence_within$ +^EXIT=6$ +^SIGNAL=0$ +-- +^\[main\.p0\] main\.x == 0 within main\.x == 1: REFUTED$ +^\[main\.p1\] main\.x == 0 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p2\] main\.x == 5 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p3\] main\.x == 10 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p4\] main\.x == 11 within \(##10 1\): REFUTED$ +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/unbounded1.desc b/regression/ebmc-spot/sva-buechi/unbounded1.desc new file mode 100644 index 000000000..0b0841f64 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/unbounded1.desc @@ -0,0 +1,7 @@ +CORE +../../verilog/SVA/unbounded1.sv +--buechi --module main --bound 1 +^error: failed to convert sva_cycle_delay$ +^EXIT=6$ +^SIGNAL=0$ +-- diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index c279d52dd..f0df3e0b5 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include #include #include "ltl.h" @@ -378,8 +377,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) if(from == 0) { // requires treatment of empty sequences on lhs - throw ebmc_errort{} - << "cannot convert 0.. ranged sequence concatenation to Buechi"; + throw ltl_sva_to_string_unsupportedt{expr}; } else if(delay.is_unbounded()) // f ##[n:$] g { @@ -448,7 +446,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) } else if(repetition.is_empty_match()) { - throw ebmc_errort{} << "cannot convert [*0] to Buechi"; + throw ltl_sva_to_string_unsupportedt{expr}; } else if(repetition.is_singleton()) { @@ -547,5 +545,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) return resultt{precedencet::ATOM, s}; } else - throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi"; + { + throw ltl_sva_to_string_unsupportedt{expr}; + } } diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h index 0337ed0ae..02cb9c6e3 100644 --- a/src/temporal-logic/ltl_sva_to_string.h +++ b/src/temporal-logic/ltl_sva_to_string.h @@ -12,10 +12,22 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +class ltl_sva_to_string_unsupportedt +{ +public: + explicit ltl_sva_to_string_unsupportedt(exprt __expr) + : expr(std::move(__expr)) + { + } + + exprt expr; +}; + /// create formula strings for external LTL to Buechi tools class ltl_sva_to_stringt { public: + // throws ltl_sva_to_string_unsupportedt when the conversion fails std::string operator()(const exprt &expr) { return rec(expr, PROPERTY).s; diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp index d6e6ed33b..393fa72d3 100644 --- a/src/temporal-logic/ltl_to_buechi.cpp +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -84,98 +84,109 @@ exprt hoa_label_to_expr( buechi_transt ltl_to_buechi(const exprt &property, message_handlert &message_handler) { - // Turn the skeleton of the property into a string ltl_sva_to_stringt ltl_sva_to_string; - auto string = ltl_sva_to_string(property); - // Run Spot's ltl2tgba - std::ostringstream hoa_stream; + try + { + // Turn the skeleton of the property into a string + auto string = ltl_sva_to_string(property); - messaget message(message_handler); + // Run Spot's ltl2tgba + std::ostringstream hoa_stream; - message.debug() << "ltl2tgba property: " << string << messaget::eom; + messaget message(message_handler); - // State-based Buchi acceptance. Should compare with transition-based - // acceptance. - // Use --complete to be able to have multiple properties in one - // model. - auto run_result = run( - "ltl2tgba", - {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string}, - "", - hoa_stream, - ""); + message.debug() << "ltl2tgba property: " << string << messaget::eom; - if(run_result != 0) - throw ebmc_errort{} << "failed to run ltl2tgba"; + // State-based Buchi acceptance. Should compare with transition-based + // acceptance. + // Use --complete to be able to have multiple properties in one + // model. + auto run_result = run( + "ltl2tgba", + {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string}, + "", + hoa_stream, + ""); - auto hoa = hoat::from_string(hoa_stream.str()); + if(run_result != 0) + throw ebmc_errort{} << "failed to run ltl2tgba"; - message.debug() << hoa << messaget::eom; + auto hoa = hoat::from_string(hoa_stream.str()); - auto max_state_number = hoa.max_state_number(); - auto state_type = range_typet{0, max_state_number}; - const auto buechi_state = symbol_exprt{"buechi::state", state_type}; - const auto buechi_next_state = next_symbol_exprt{"buechi::state", state_type}; + message.debug() << hoa << messaget::eom; - // construct the initial state constraint - std::vector init_disjuncts; + auto max_state_number = hoa.max_state_number(); + auto state_type = range_typet{0, max_state_number}; + const auto buechi_state = symbol_exprt{"buechi::state", state_type}; + const auto buechi_next_state = + next_symbol_exprt{"buechi::state", state_type}; - 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)}); - } + // construct the initial state constraint + std::vector init_disjuncts; - auto init = disjunction(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)}); + } - message.debug() << "Buechi initial state: " << format(init) << messaget::eom; + auto init = disjunction(init_disjuncts); - // construct the liveness signal - std::vector liveness_disjuncts; + message.debug() << "Buechi initial state: " << format(init) + << messaget::eom; - 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)}); - } + // construct the liveness signal + std::vector liveness_disjuncts; - auto liveness_signal = disjunction(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)}); + } - message.debug() << "Buechi liveness signal: " << format(liveness_signal) - << messaget::eom; + auto liveness_signal = disjunction(liveness_disjuncts); - // construct the transition relation - std::vector trans_disjuncts; + message.debug() << "Buechi liveness signal: " << format(liveness_signal) + << messaget::eom; - for(auto &state : hoa.body) - { - auto pre = - equal_exprt{buechi_state, from_integer(state.first.number, state_type)}; - for(auto &edge : state.second) + // construct the transition relation + std::vector trans_disjuncts; + + for(auto &state : hoa.body) { - if(edge.dest_states.size() != 1) - throw ebmc_errort() << "edge must have one destination state"; - auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string); - auto post = equal_exprt{ - buechi_next_state, from_integer(edge.dest_states.front(), state_type)}; - trans_disjuncts.push_back(and_exprt{pre, cond, post}); + 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 cond = hoa_label_to_expr(edge.label, ltl_sva_to_string); + auto post = equal_exprt{ + buechi_next_state, + from_integer(edge.dest_states.front(), state_type)}; + trans_disjuncts.push_back(and_exprt{pre, cond, post}); + } } - } - auto trans = disjunction(trans_disjuncts); + auto trans = disjunction(trans_disjuncts); - message.debug() << "Buechi transition constraint: " << format(trans) - << messaget::eom; + message.debug() << "Buechi transition constraint: " << format(trans) + << messaget::eom; - return { - buechi_state, - std::move(init), - std::move(trans), - std::move(liveness_signal)}; + return { + buechi_state, + std::move(init), + std::move(trans), + std::move(liveness_signal)}; + } + catch(ltl_sva_to_string_unsupportedt error) + { + throw ebmc_errort{} << "failed to convert " << error.expr.id(); + } }