diff --git a/regression/ebmc-spot/ltl-buechi/implies3.desc b/regression/ebmc-spot/ltl-buechi/implies3.desc new file mode 100644 index 000000000..ee311b162 --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/implies3.desc @@ -0,0 +1,8 @@ +CORE +implies3.smv +--buechi --bound 5 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/ltl-buechi/implies3.smv b/regression/ebmc-spot/ltl-buechi/implies3.smv new file mode 100644 index 000000000..f167e032e --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/implies3.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR x : 0..3; + +ASSIGN + init(x) := 1; + + next(x) := + case + x=3 : 3; + TRUE: x+1; + esac; + +LTLSPEC ! (F x = 1 -> F x = 0) -- should pass diff --git a/regression/ebmc-spot/sva-buechi/if1.k.desc b/regression/ebmc-spot/sva-buechi/if1.k.desc index 2119fbeea..858c53c1d 100644 --- a/regression/ebmc-spot/sva-buechi/if1.k.desc +++ b/regression/ebmc-spot/sva-buechi/if1.k.desc @@ -1,6 +1,6 @@ CORE ../../verilog/SVA/if1.sv ---buechi --k-induction --bound 1 +--buechi --k-induction --bound 2 ^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED$ ^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$ ^EXIT=10$ diff --git a/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc new file mode 100644 index 000000000..43518554e --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sequence_and1.sv +--buechi --bdd +^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$ +^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$ +^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$ +^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$ +^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc new file mode 100644 index 000000000..0f866e2db --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sequence_and1.sv +--buechi --bound 5 +^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$ +^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$ +^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED up to bound \d+$ +^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED up to bound \d+$ +^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp index 68d6a6987..902d4d36d 100644 --- a/src/temporal-logic/hoa.cpp +++ b/src/temporal-logic/hoa.cpp @@ -266,6 +266,28 @@ hoat::headert hoa_parsert::parse_header() return header; } +hoat::ap_mapt hoat::parse_AP() const +{ + for(auto &item : header) + { + if(item.first == "AP:") + { + hoat::ap_mapt result; + std::size_t index = 0; + for(auto &name : item.second) + { + if(index != 0) + result[index - 1] = name; + index++; + } + return result; + } + } + + // header not found + return {}; +} + hoat::bodyt hoa_parsert::parse_body() { if(!tokenizer.consume().is_body()) @@ -323,8 +345,6 @@ hoat::edgest hoa_parsert::parse_edges() return edges; } -#include - hoat::edget hoa_parsert::parse_edge() { edget edge; diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h index c532522d1..e140e0adc 100644 --- a/src/temporal-logic/hoa.h +++ b/src/temporal-logic/hoa.h @@ -68,7 +68,10 @@ class hoat intt max_state_number() const; // atomic propositions - std::map ap_map; + using ap_mapt = std::map; + + // parses the AP header + ap_mapt parse_AP() const; // convert into a graph struct graph_edget diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index 44dd1569c..294295b4c 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include #include #include "ltl.h" @@ -21,8 +22,11 @@ Author: Daniel Kroening, dkr@amazon.com exprt ltl_sva_to_stringt::atom(const std::string &string) const { + if(string.empty() || string[0] != 'a') + throw ebmc_errort{} << "got unexpected atom '" << string << "'"; + // map back to number - auto number = safe_string2size_t(string); + auto number = safe_string2size_t(string.substr(1, std::string::npos)); PRECONDITION(number < atoms.size()); diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h index 02cb9c6e3..f4ac209da 100644 --- a/src/temporal-logic/ltl_sva_to_string.h +++ b/src/temporal-logic/ltl_sva_to_string.h @@ -53,6 +53,8 @@ class ltl_sva_to_stringt std::string s; }; + // This maps our expressions to a number. + // Spot may or may not use the same numbering in the AP header. numberingt atoms; using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN }; diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp index 0b8c59227..e67de4523 100644 --- a/src/temporal-logic/ltl_to_buechi.cpp +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include +#include #include #include @@ -46,12 +47,13 @@ void buechi_transt::rename_state_symbol(const symbol_exprt &new_state_symbol) exprt hoa_label_to_expr( const hoat::labelt &label, - const ltl_sva_to_stringt <l_sva_to_string) + const ltl_sva_to_stringt <l_sva_to_string, + const hoat::ap_mapt &ap_map) { std::vector operands; operands.reserve(label.get_sub().size()); for(auto &sub : label.get_sub()) - operands.push_back(hoa_label_to_expr(sub, ltl_sva_to_string)); + operands.push_back(hoa_label_to_expr(sub, ltl_sva_to_string, ap_map)); if(label.id() == "t") { @@ -78,8 +80,17 @@ exprt hoa_label_to_expr( } else { - // atomic proposition, given as number - return ltl_sva_to_string.atom(label.id_string()); + // Atomic proposition, given as number. This is the numbering + // from the "AP" header, which then maps to a string "aX", which + // is our atom number. These may or may not match. + auto spot_ap_number = safe_string2size_t(label.id_string()); + + auto ap_map_it = ap_map.find(spot_ap_number); + if(ap_map_it == ap_map.end()) + throw ebmc_errort{} << "failed to find atom " << label.id() + << " in AP header"; + + return ltl_sva_to_string.atom(ap_map_it->second); } } @@ -150,6 +161,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) hoa.buechi_acceptance_cleanup(); auto max_state_number = hoa.max_state_number(); + auto ap_map = hoa.parse_AP(); auto state_type = range_typet{0, max_state_number}; const auto buechi_state = symbol_exprt{"buechi::state", state_type}; const auto buechi_next_state = @@ -220,7 +232,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) { auto pre = equal_exprt{ buechi_state, from_integer(state.first.number, state_type)}; - auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string); + auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string, ap_map); error_disjuncts.push_back(and_exprt{pre, cond}); } } @@ -242,7 +254,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) { 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 cond = hoa_label_to_expr(edge.label, ltl_sva_to_string, ap_map); auto post = equal_exprt{ buechi_next_state, from_integer(edge.dest_states.front(), state_type)};