From 9633ac852c5ba9854ed49c8ce7c29ce90c2c2afe Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 4 Aug 2025 12:44:59 -0700 Subject: [PATCH] LTL/SVA->Buechi: reject error traces early The Buechi automaton accepts counterexamples to the original property. The Buechi acceptance condition requires a lasso where the loop contains an accepting state. A proof of that requires satisfying the looping condition, which may require a very long counterexample. This adds a shortcut using a sufficient condition for a counterexample: we can reject the property when we reach a state in which the Buechi automaton transitions into an accepting state that has an unconditional self-loop on it. Such traces can always be extended to a lasso as above. --- regression/ebmc-spot/sva-buechi/case1.desc | 10 ++++ regression/ebmc-spot/sva-buechi/cover1.desc | 13 +++++ regression/ebmc-spot/sva-buechi/cover2.desc | 13 +++++ .../sva-buechi/cover_sequence1.bmc.desc | 10 ++++ .../sva-buechi/cover_sequence2.bmc.desc | 12 +++++ .../sva-buechi/cover_sequence3.bmc.desc | 12 +++++ .../sva-buechi/cover_sequence4.bmc.desc | 12 +++++ .../sva-buechi/disable_iff1.bmc.desc | 12 +++++ .../sva-buechi/empty_sequence1.bmc.desc | 13 +++++ .../sva-buechi/followed-by4.bmc.desc | 3 +- regression/ebmc-spot/sva-buechi/if1.bmc.desc | 10 ++++ .../ebmc-spot/sva-buechi/initial1.bmc.desc | 14 +++++ .../ebmc-spot/sva-buechi/s_always1.desc | 3 +- .../ebmc-spot/sva-buechi/sequence1.desc | 12 +++++ .../ebmc-spot/sva-buechi/sequence_and3.desc | 12 +++++ .../sva-buechi/sequence_or1.bmc.desc | 13 +++++ .../sva-buechi/sequence_repetition1.bdd.desc | 13 +++++ .../sva-buechi/sequence_repetition1.bmc.desc | 14 +++++ .../sva-buechi/sequence_repetition3.bmc.desc | 11 ++++ .../ebmc-spot/sva-buechi/sva_abort1.bmc.desc | 13 +++++ regression/verilog/SVA/cover1.desc | 1 - regression/verilog/SVA/if1.desc | 1 - src/ebmc/instrument_buechi.cpp | 9 ++++ src/temporal-logic/hoa.h | 4 ++ src/temporal-logic/ltl_to_buechi.cpp | 53 ++++++++++++++++++- src/temporal-logic/ltl_to_buechi.h | 3 ++ 26 files changed, 289 insertions(+), 7 deletions(-) create mode 100644 regression/ebmc-spot/sva-buechi/case1.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover1.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover2.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/if1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/initial1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_and3.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_or1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition1.bdd.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition3.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/sva_abort1.bmc.desc diff --git a/regression/ebmc-spot/sva-buechi/case1.desc b/regression/ebmc-spot/sva-buechi/case1.desc new file mode 100644 index 000000000..a9eeca33e --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/case1.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/case1.sv +--buechi --bound 20 --numbered-trace +^\[main\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$ +^Counterexample with 11 states:$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/cover1.desc b/regression/ebmc-spot/sva-buechi/cover1.desc new file mode 100644 index 000000000..88ab4ea34 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover1.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/cover1.sv +--buechi --bound 10 --numbered-trace +^\[main\.p0\] cover main\.counter == 1: PROVED$ +^Trace with 2 states:$ +^main\.counter@0 = 0$ +^main\.counter@1 = 1$ +^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/cover2.desc b/regression/ebmc-spot/sva-buechi/cover2.desc new file mode 100644 index 000000000..69f93eb11 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover2.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/cover2.sv +--buechi --bound 10 --numbered-trace +^\[main\.p0\] cover main\.counter == 1: PROVED$ +^Trace with 2 states:$ +^main\.counter@0 = 0$ +^main\.counter@1 = 1$ +^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc new file mode 100644 index 000000000..09ded4191 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/cover_sequence1.sv +--buechi --bound 10 --numbered-trace +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc new file mode 100644 index 000000000..0dda3d634 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/cover_sequence2.sv +--buechi --bound 5 +^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$ +^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: not convertible to Buechi$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc new file mode 100644 index 000000000..0289ca371 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc @@ -0,0 +1,12 @@ +KNOWNBUG +../../verilog/SVA/cover_sequence3.sv +--buechi --bound 3 +^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$ +^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$ +^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Trace one too short. diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc new file mode 100644 index 000000000..caa25fb8d --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc @@ -0,0 +1,12 @@ +KNOWNBUG +../../verilog/SVA/cover_sequence4.sv +--buechi --bound 3 +^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$ +^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$ +^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Trace one too short. diff --git a/regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc b/regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc new file mode 100644 index 000000000..3737f5bc4 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/disable_iff1.sv +--buechi --module main --bound 10 --numbered-trace +^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED up to bound 10$ +^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED up to bound 10$ +^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$ +^Counterexample with 3 states:$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc b/regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc new file mode 100644 index 000000000..20f6fe296 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/empty_sequence1.sv +--buechi --bound 5 +^\[main\.p0\] 1 \[\*0\]: REFUTED$ +^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$ +^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$ +^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$ +^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc b/regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc index 226b61fdb..8893fad17 100644 --- a/regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE ../../verilog/SVA/followed-by4.sv --buechi --bound 3 ^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$ @@ -9,4 +9,3 @@ KNOWNBUG -- ^warning: ignoring -- -p1 is not refuted. diff --git a/regression/ebmc-spot/sva-buechi/if1.bmc.desc b/regression/ebmc-spot/sva-buechi/if1.bmc.desc new file mode 100644 index 000000000..1d0e35c72 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/if1.bmc.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/if1.sv +--buechi --bound 2 +^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED up to bound 2$ +^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/initial1.bmc.desc b/regression/ebmc-spot/sva-buechi/initial1.bmc.desc new file mode 100644 index 000000000..f9cf4f7e2 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/initial1.bmc.desc @@ -0,0 +1,14 @@ +CORE +../../verilog/SVA/initial1.sv +--buechi --bound 5 +^\[main\.p0\] main\.counter == 0: PROVED up to bound 5$ +^\[main\.p1\] main\.counter == 100: REFUTED$ +^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 5$ +^\[main\.p3\] ##1 main\.counter == 100: REFUTED$ +^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 5$ +^\[main\.p5\] always \[1:1\] main\.counter == 1: PROVED up to bound 5$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/s_always1.desc b/regression/ebmc-spot/sva-buechi/s_always1.desc index cb3006ce5..1327bd31c 100644 --- a/regression/ebmc-spot/sva-buechi/s_always1.desc +++ b/regression/ebmc-spot/sva-buechi/s_always1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE ../../verilog/SVA/s_always1.sv --buechi --bound 20 ^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$ @@ -8,4 +8,3 @@ KNOWNBUG -- ^warning: ignoring -- -main.p1 is not refuted. diff --git a/regression/ebmc-spot/sva-buechi/sequence1.desc b/regression/ebmc-spot/sva-buechi/sequence1.desc new file mode 100644 index 000000000..63d567d5b --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence1.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/sequence1.sv +--buechi --bound 20 --numbered-trace +^\[main\.p0\] ##\[0:9\] main\.x == 100: REFUTED$ +^Counterexample with 10 states:$ +^main\.x@0 = 0$ +^main\.x@9 = 9$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_and3.desc b/regression/ebmc-spot/sva-buechi/sequence_and3.desc new file mode 100644 index 000000000..82aee44e8 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_and3.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/sequence_and3.sv +--buechi --bound 5 +^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 2: REFUTED$ +^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 2: REFUTED$ +^\[.*\] \(\(1 or \(##2 1\)\) and 1\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$ +^\[.*\] \(1 and \(1 or \(##2 1\)\)\) \|-> main\.x == 0 \|\| main\.x == 2: PROVED up to bound 5$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_or1.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_or1.bmc.desc new file mode 100644 index 000000000..77782e203 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_or1.bmc.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sequence_or1.sv +--buechi --bound 5 +^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED up to bound \d+$ +^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED up to bound \d+$ +^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED up to bound \d+$ +^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED up to bound \d+$ +^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition1.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bdd.desc new file mode 100644 index 000000000..5da6cf7b5 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bdd.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sequence_repetition1.sv +--buechi --bdd +^\[.*\] main\.half_x == 0 \[\*2\]: PROVED$ +^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BDD engine$ +^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BDD engine$ +^\[.*\] main\.x == 0 \[\*2\]: REFUTED$ +^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BDD engine$ +^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BDD engine$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc new file mode 100644 index 000000000..5b64f65ef --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc @@ -0,0 +1,14 @@ +CORE +../../verilog/SVA/sequence_repetition1.sv +--buechi --bound 10 +^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$ +^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$ +^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$ +^\[.*\] main\.x == 0 \[\*2\]: REFUTED$ +^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$ +^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition3.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition3.bmc.desc new file mode 100644 index 000000000..384f106dc --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition3.bmc.desc @@ -0,0 +1,11 @@ +CORE +../../verilog/SVA/sequence_repetition3.sv +--buechi --bound 10 +^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED up to bound 10$ +^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED up to bound 10$ +^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sva_abort1.bmc.desc b/regression/ebmc-spot/sva-buechi/sva_abort1.bmc.desc new file mode 100644 index 000000000..e913175e1 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sva_abort1.bmc.desc @@ -0,0 +1,13 @@ +CORE +../../verilog/SVA/sva_abort1.sv +--buechi --module main --bound 10 +^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED up to bound 10$ +^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED up to bound 10$ +^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$ +^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$ +^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc index 88ce2095a..f2d98e520 100644 --- a/regression/verilog/SVA/cover1.desc +++ b/regression/verilog/SVA/cover1.desc @@ -11,4 +11,3 @@ cover1.sv -- ^warning: ignoring -- -Back-end support is missing. diff --git a/regression/verilog/SVA/if1.desc b/regression/verilog/SVA/if1.desc index 6b4847587..30bf4bc6b 100644 --- a/regression/verilog/SVA/if1.desc +++ b/regression/verilog/SVA/if1.desc @@ -8,4 +8,3 @@ if1.sv -- ^warning: ignoring -- -SMT-back end doesn't do cast from bool to bool. diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp index d94adcf8a..e082aeb08 100644 --- a/src/ebmc/instrument_buechi.cpp +++ b/src/ebmc/instrument_buechi.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, dkr@amazon.com #include "instrument_buechi.h" +#include + #include #include #include @@ -67,5 +69,12 @@ void instrument_buechi( // so this is the negation of the Buechi acceptance condition. property.normalized_expr = F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}}; + + if(!buechi.error_signal.is_true()) + property.normalized_expr = and_exprt{ + property.normalized_expr, G_exprt{not_exprt{buechi.error_signal}}}; + + message.debug() << "New property: " << format(property.normalized_expr) + << messaget::eom; } } diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h index 72f5e52c1..394699544 100644 --- a/src/temporal-logic/hoa.h +++ b/src/temporal-logic/hoa.h @@ -32,6 +32,10 @@ class hoat mp_integer number; labelt label; // in-state condition acc_sigt acc_sig; + bool is_accepting() const + { + return !acc_sig.empty(); + } }; struct edget { diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp index 393fa72d3..a87114419 100644 --- a/src/temporal-logic/ltl_to_buechi.cpp +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "ltl_to_buechi.h" #include +#include #include #include #include @@ -37,6 +38,7 @@ void buechi_transt::rename_state_symbol(const symbol_exprt &new_state_symbol) replace_expr(replace_map, init); replace_expr(replace_map, trans); + replace_expr(replace_map, error_signal); replace_expr(replace_map, liveness_signal); state_symbol = new_state_symbol; @@ -81,6 +83,23 @@ exprt hoa_label_to_expr( } } +// a nonaccepting state with an unconditional self-loop +bool is_error_state(const std::pair &state) +{ + if(!state.first.is_accepting()) + return false; + + for(auto &edge : state.second) + { + if(edge.label.id() == "t") + for(auto &dest : edge.dest_states) + if(dest == state.first.number) + return true; + } + + return false; +} + buechi_transt ltl_to_buechi(const exprt &property, message_handlert &message_handler) { @@ -144,7 +163,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) std::vector liveness_disjuncts; for(auto &state : hoa.body) - if(!state.first.acc_sig.empty()) + if(state.first.is_accepting()) { liveness_disjuncts.push_back(equal_exprt{ buechi_state, from_integer(state.first.number, state_type)}); @@ -155,6 +174,37 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) message.debug() << "Buechi liveness signal: " << format(liveness_signal) << messaget::eom; + // construct the error signal -- true when the next automaton state + // is nonaccepting with an unconditional self-loop. + std::vector error_disjuncts; + + std::map> state_map; + for(auto &state : hoa.body) + state_map[state.first.number] = state; + + for(auto &state : hoa.body) + { + for(auto &edge : state.second) + { + if(edge.dest_states.size() != 1) + throw ebmc_errort() << "edge must have one destination state"; + auto dest_state_it = state_map.find(edge.dest_states.front()); + CHECK_RETURN(dest_state_it != state_map.end()); + if(is_error_state(dest_state_it->second)) + { + 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); + error_disjuncts.push_back(and_exprt{pre, cond}); + } + } + } + + auto error_signal = disjunction(error_disjuncts); + + message.debug() << "Buechi error signal: " << format(error_signal) + << messaget::eom; + // construct the transition relation std::vector trans_disjuncts; @@ -183,6 +233,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) buechi_state, std::move(init), std::move(trans), + std::move(error_signal), std::move(liveness_signal)}; } catch(ltl_sva_to_string_unsupportedt error) diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h index 39e8b4a4e..d842302ac 100644 --- a/src/temporal-logic/ltl_to_buechi.h +++ b/src/temporal-logic/ltl_to_buechi.h @@ -17,16 +17,19 @@ struct buechi_transt exprt init; exprt trans; + exprt error_signal; exprt liveness_signal; buechi_transt( symbol_exprt __state_symbol, exprt __init, exprt __trans, + exprt __error_signal, exprt __liveness_signal) : state_symbol(std::move(__state_symbol)), init(std::move(__init)), trans(std::move(__trans)), + error_signal(std::move(__error_signal)), liveness_signal(std::move(__liveness_signal)) { }