From 939d51a2b24e11ac83e79d9de22b83fcf7f87b82 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 13 Jul 2025 14:53:42 -0700 Subject: [PATCH] BMC: reconsider lasso-shaped encodings This replaces the lasso-shaped encodings in the word-level BMC property encoding. The lasso and straigth-line encodings are now built as separate obligations. In the lasso encoding, all operators follow the same lasso shape. This avoids spurious traces where the eventually operator follows the lasso but a safety part of the property does not. --- CHANGELOG | 1 + regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc | 9 +- regression/smv/LTL/smv_ltlspec_F4.desc | 5 +- regression/smv/LTL/smv_ltlspec_F6.desc | 7 +- regression/smv/LTL/smv_ltlspec_FG1.bmc.desc | 7 +- regression/smv/LTL/smv_ltlspec_FG1.smv | 4 + regression/smv/LTL/smv_ltlspec_FX1.bdd.desc | 9 + regression/smv/LTL/smv_ltlspec_FX1.bmc.desc | 9 + regression/smv/LTL/smv_ltlspec_FX1.smv | 7 + regression/smv/LTL/smv_ltlspec_U3.desc | 9 + regression/smv/LTL/smv_ltlspec_U3.smv | 6 + regression/smv/LTL/smv_ltlspec_or1.desc | 1 + regression/smv/LTL/smv_ltlspec_or2.desc | 9 + regression/smv/LTL/smv_ltlspec_or2.smv | 11 + src/smvlang/smv_typecheck.cpp | 13 +- src/trans-word-level/property.cpp | 271 ++++++++++++++---- 16 files changed, 298 insertions(+), 80 deletions(-) create mode 100644 regression/smv/LTL/smv_ltlspec_FX1.bdd.desc create mode 100644 regression/smv/LTL/smv_ltlspec_FX1.bmc.desc create mode 100644 regression/smv/LTL/smv_ltlspec_FX1.smv create mode 100644 regression/smv/LTL/smv_ltlspec_U3.desc create mode 100644 regression/smv/LTL/smv_ltlspec_U3.smv create mode 100644 regression/smv/LTL/smv_ltlspec_or2.desc create mode 100644 regression/smv/LTL/smv_ltlspec_or2.smv diff --git a/CHANGELOG b/CHANGELOG index 8d6d9cd54..58340a932 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -7,6 +7,7 @@ * SystemVerilog: fix for |-> and |=> for empty matches * LTL/SVA to Buechi with --buechi * SMV: abs, bool, count, max, min, toint, word1 +* BMC: new encoding for F, avoiding spurious traces # EBMC 5.6 diff --git a/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc b/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc index c9fb26586..7c85bc4c9 100644 --- a/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc +++ b/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc @@ -1,10 +1,9 @@ -KNOWNBUG -smv_ltlspec_AFAG1.smv ---bound 3 -^\[spec1\] AF AG !buechi_state: PROVED$ +CORE +smv_ctlspec_AFAG1.smv +--bound 10 +^\[spec1\] AF AG !buechi_state: PROVED up to bound 10$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -The BMC engine returns the wrong answer. diff --git a/regression/smv/LTL/smv_ltlspec_F4.desc b/regression/smv/LTL/smv_ltlspec_F4.desc index 33154fd01..4ecebf2c6 100644 --- a/regression/smv/LTL/smv_ltlspec_F4.desc +++ b/regression/smv/LTL/smv_ltlspec_F4.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE smv_ltlspec_F4.smv ---bound 3 +--bound 2 ^\[spec1\] F \(some_input <-> X some_input\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -The BMC engine gives the wrong answer. diff --git a/regression/smv/LTL/smv_ltlspec_F6.desc b/regression/smv/LTL/smv_ltlspec_F6.desc index be862b8bc..d0650f0a6 100644 --- a/regression/smv/LTL/smv_ltlspec_F6.desc +++ b/regression/smv/LTL/smv_ltlspec_F6.desc @@ -1,10 +1,11 @@ -KNOWNBUG +CORE smv_ltlspec_F6.smv ---bound 3 --numbered-trace +--bound 1 --numbered-trace ^\[spec1\] F X some_input: REFUTED$ +^some_input@0 = FALSE$ +^some_input@1 = FALSE$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -The BMC engine gives the wrong answer. diff --git a/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc b/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc index be44f81a8..e93a9945d 100644 --- a/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc +++ b/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE smv_ltlspec_FG1.smv ---bound 2 -^\[spec1\] F G x!=1: PROVED$ +--bound 10 +^\[spec1\] F G x != 1: PROVED up to bound 10$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -The BMC engine returns the wrong answer. diff --git a/regression/smv/LTL/smv_ltlspec_FG1.smv b/regression/smv/LTL/smv_ltlspec_FG1.smv index 15da57962..21f20312d 100644 --- a/regression/smv/LTL/smv_ltlspec_FG1.smv +++ b/regression/smv/LTL/smv_ltlspec_FG1.smv @@ -10,4 +10,8 @@ TRANS x=1 -> next(x)=2 TRANS x=2 -> next(x)=2 +-- This should pass. +-- There are traces of two kinds: +-- 0, 0, 0, ... +-- 0, ..., 0, 1, 2, 2, ... LTLSPEC F G x!=1 diff --git a/regression/smv/LTL/smv_ltlspec_FX1.bdd.desc b/regression/smv/LTL/smv_ltlspec_FX1.bdd.desc new file mode 100644 index 000000000..462dcb769 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_FX1.bdd.desc @@ -0,0 +1,9 @@ +CORE +smv_ltlspec_FX1.smv +--bdd +^\[spec1\] F X X p: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/LTL/smv_ltlspec_FX1.bmc.desc b/regression/smv/LTL/smv_ltlspec_FX1.bmc.desc new file mode 100644 index 000000000..7f156ade2 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_FX1.bmc.desc @@ -0,0 +1,9 @@ +CORE +smv_ltlspec_FX1.smv +--bound 1 +^\[spec1\] F X X p: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/LTL/smv_ltlspec_FX1.smv b/regression/smv/LTL/smv_ltlspec_FX1.smv new file mode 100644 index 000000000..d7c382c54 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_FX1.smv @@ -0,0 +1,7 @@ +MODULE main + +VAR p : boolean; + +-- This should fail for any bound >= 1. +-- The shortest lasso is FALSE, FALSE, ... +LTLSPEC F X X p diff --git a/regression/smv/LTL/smv_ltlspec_U3.desc b/regression/smv/LTL/smv_ltlspec_U3.desc new file mode 100644 index 000000000..e28bdd72a --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_U3.desc @@ -0,0 +1,9 @@ +CORE +smv_ltlspec_U3.smv +--bound 5 +^\[.*\] TRUE U x -> F x: PROVED up to bound 5$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/LTL/smv_ltlspec_U3.smv b/regression/smv/LTL/smv_ltlspec_U3.smv new file mode 100644 index 000000000..8e9d840e0 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_U3.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR x : boolean; + +-- should pass +LTLSPEC (TRUE U x) -> F x diff --git a/regression/smv/LTL/smv_ltlspec_or1.desc b/regression/smv/LTL/smv_ltlspec_or1.desc index f097f716c..1a066b834 100644 --- a/regression/smv/LTL/smv_ltlspec_or1.desc +++ b/regression/smv/LTL/smv_ltlspec_or1.desc @@ -6,3 +6,4 @@ smv_ltlspec_or1.smv ^SIGNAL=0$ -- ^warning: ignoring +-- diff --git a/regression/smv/LTL/smv_ltlspec_or2.desc b/regression/smv/LTL/smv_ltlspec_or2.desc new file mode 100644 index 000000000..fe6542295 --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_or2.desc @@ -0,0 +1,9 @@ +KNOWNBUG +smv_ltlspec_or2.smv +--bound 10 +^\[spec1\] F z \| z V x: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/LTL/smv_ltlspec_or2.smv b/regression/smv/LTL/smv_ltlspec_or2.smv new file mode 100644 index 000000000..b418abb2d --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_or2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR x : boolean; + +VAR z : boolean; + +ASSIGN init(z) := FALSE; + next(z) := FALSE; + +-- should fail +LTLSPEC (F z) | (z V x) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 84d3f1041..df5d5e763 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1959,10 +1959,19 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars) symbol.name=var.identifier; symbol.value.make_nil(); - symbol.is_input=true; - symbol.is_state_var=false; symbol.type=var.type; + if(var.type.id() == "submodule") + { + symbol.is_input = false; + symbol.is_state_var = false; + } + else + { + symbol.is_input = true; + symbol.is_state_var = false; + } + symbol_table.add(symbol); } } diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index c5751e052..f40b956d5 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -176,13 +177,27 @@ Function: property_obligations_rec \*******************************************************************/ +/// Timeframe index of the start and end of the loop of the lasso. +struct bmc_lassot +{ + // State 'start' is required to be equal to state 'end'. + mp_integer start, end; +}; + static obligationst property_obligations_rec( const exprt &property_expr, const mp_integer ¤t, - const mp_integer &no_timeframes) + const mp_integer &no_timeframes, + const std::optional &lasso) { PRECONDITION(current >= 0 && current < no_timeframes); + if(lasso.has_value()) + { + PRECONDITION(lasso.value().start < lasso.value().end); + PRECONDITION(lasso.value().end < no_timeframes); + } + if( property_expr.id() == ID_AG || property_expr.id() == ID_G || property_expr.id() == ID_sva_always) @@ -199,11 +214,29 @@ static obligationst property_obligations_rec( PRECONDITION(false); }(property_expr); + mp_integer from, to; + + if(lasso.has_value()) + { + // From 'current', but include the loop of the lasso in case + // we loop back before 'current'. + from = std::min(current, lasso.value().start); + + // Up to the end of the lasso. + to = lasso.value().end; + } + else + { + // From current, including, to the very end. + from = current; + to = no_timeframes - 1; + } + obligationst obligations; - for(mp_integer c = current; c < no_timeframes; ++c) + for(mp_integer c = from; c <= to; ++c) { - obligations.add(property_obligations_rec(phi, c, no_timeframes)); + obligations.add(property_obligations_rec(phi, c, no_timeframes, lasso)); } return obligations; @@ -213,11 +246,9 @@ static obligationst property_obligations_rec( const auto &eventually_expr = to_sva_eventually_expr(property_expr); const auto &op = eventually_expr.op(); + // These are always bounded, no need for a lasso. mp_integer from = numeric_cast_v(eventually_expr.from()); - - mp_integer to; - if(to_integer_non_constant(eventually_expr.to(), to)) - throw "failed to convert sva_eventually index"; + mp_integer to = numeric_cast_v(eventually_expr.to()); // We rely on NNF. if(current + from >= no_timeframes || current + to >= no_timeframes) @@ -230,7 +261,8 @@ static obligationst property_obligations_rec( for(mp_integer u = current + from; u <= current + to; ++u) { - auto obligations_rec = property_obligations_rec(op, u, no_timeframes); + auto obligations_rec = + property_obligations_rec(op, u, no_timeframes, lasso); disjuncts.push_back(obligations_rec.conjunction().second); } @@ -243,41 +275,40 @@ static obligationst property_obligations_rec( { const auto &phi = to_unary_expr(property_expr).op(); - obligationst obligations; + // Counterexamples to Fφ are infinite paths, and we look + // for a lasso. + + if(!lasso.has_value()) + return {}; + + const auto l = lasso.value(); - // Traces with any φ state from "current" onwards satisfy Fφ + // we want counterexamples starting no later than 'current' + if(l.start < current) + return {}; + + // The following needs to be satisfied for a counterexample + // to Fφ that is a lassp with loop from l.start to l.end: + // + // (stem) No state j with current(no_timeframes - current)); + phi_disjuncts.reserve(numeric_cast_v(l.end - current)); - for(mp_integer j = current; j < no_timeframes; ++j) + for(mp_integer j = current; j < l.end; ++j) { - auto tmp = property_obligations_rec(phi, j, no_timeframes); + auto tmp = property_obligations_rec(phi, j, no_timeframes, lasso); phi_disjuncts.push_back(tmp.conjunction().second); } auto phi_disjunction = disjunction(phi_disjuncts); - // Counterexamples to Fφ must have a loop. - // We consider l-k loops with l const exprt & { if(expr.id() == ID_X) @@ -384,14 +414,36 @@ static obligationst property_obligations_rec( PRECONDITION(false); }(property_expr); - if(next < no_timeframes) + if(lasso.has_value()) { - return property_obligations_rec(phi, next, no_timeframes); + mp_integer next; + if(current == lasso.value().end) + { + // we follow the loop + next = lasso.value().start; + } + else + { + PRECONDITION(current < lasso.value().end); + next = current + 1; + } + + return property_obligations_rec(phi, next, no_timeframes, lasso); } else { - DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); - return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only + const auto next = current + 1; + + if(next < no_timeframes) + { + return property_obligations_rec(phi, next, no_timeframes, lasso); + } + else + { + DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); + return obligationst{ + no_timeframes - 1, true_exprt()}; // works on NNF only + } } } else if(property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U) @@ -402,10 +454,13 @@ static obligationst property_obligations_rec( // p U q ≡ Fq ∧ (p W q) exprt tmp = and_exprt{F_exprt{q}, weak_U_exprt{p, q}}; - return property_obligations_rec(tmp, current, no_timeframes); + return property_obligations_rec(tmp, current, no_timeframes, lasso); } else if(property_expr.id() == ID_sva_until || property_expr.id() == ID_weak_U) { + if(lasso.has_value()) + return {}; + // we expand: p W q ≡ q ∨ ( p ∧ X(p W q) ) auto &p = to_binary_expr(property_expr).lhs(); auto &q = to_binary_expr(property_expr).rhs(); @@ -415,10 +470,13 @@ static obligationst property_obligations_rec( q, (current + 1) < no_timeframes ? and_exprt{p, X_exprt{property_expr}} : p}; - return property_obligations_rec(tmp, current, no_timeframes); + return property_obligations_rec(tmp, current, no_timeframes, lasso); } else if(property_expr.id() == ID_R) { + if(lasso.has_value()) + return {}; + // we expand: p R q <=> q ∧ (p ∨ X(p R q)) auto &R_expr = to_R_expr(property_expr); auto &p = R_expr.lhs(); @@ -430,7 +488,7 @@ static obligationst property_obligations_rec( ? and_exprt{q, or_exprt{p, X_exprt{property_expr}}} : q; - return property_obligations_rec(expansion, current, no_timeframes); + return property_obligations_rec(expansion, current, no_timeframes, lasso); } else if(property_expr.id() == ID_strong_R) { @@ -440,7 +498,7 @@ static obligationst property_obligations_rec( // p strongR q ≡ Fp ∧ (p R q) exprt tmp = and_exprt{F_exprt{q}, weak_U_exprt{p, q}}; - return property_obligations_rec(tmp, current, no_timeframes); + return property_obligations_rec(tmp, current, no_timeframes, lasso); } else if(property_expr.id() == ID_sva_until_with) { @@ -448,7 +506,7 @@ static obligationst property_obligations_rec( // Note that lhs and rhs are flipped. auto &until_with = to_sva_until_with_expr(property_expr); auto R = R_exprt{until_with.rhs(), until_with.lhs()}; - return property_obligations_rec(R, current, no_timeframes); + return property_obligations_rec(R, current, no_timeframes, lasso); } else if(property_expr.id() == ID_sva_s_until_with) { @@ -456,7 +514,7 @@ static obligationst property_obligations_rec( // Note that lhs and rhs are flipped. auto &s_until_with = to_sva_s_until_with_expr(property_expr); auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()}; - return property_obligations_rec(strong_R, current, no_timeframes); + return property_obligations_rec(strong_R, current, no_timeframes, lasso); } else if(property_expr.id() == ID_and) { @@ -466,7 +524,8 @@ static obligationst property_obligations_rec( for(auto &op : to_and_expr(property_expr).operands()) { - obligations.add(property_obligations_rec(op, current, no_timeframes)); + obligations.add( + property_obligations_rec(op, current, no_timeframes, lasso)); } return obligations; @@ -481,7 +540,8 @@ static obligationst property_obligations_rec( for(auto &op : to_or_expr(property_expr).operands()) { - auto obligations = property_obligations_rec(op, current, no_timeframes); + auto obligations = + property_obligations_rec(op, current, no_timeframes, lasso); auto conjunction = obligations.conjunction(); t = std::max(t, conjunction.first); disjuncts.push_back(conjunction.second); @@ -498,14 +558,14 @@ static obligationst property_obligations_rec( auto tmp = and_exprt{ implies_exprt{equal_expr.lhs(), equal_expr.rhs()}, implies_exprt{equal_expr.rhs(), equal_expr.lhs()}}; - return property_obligations_rec(tmp, current, no_timeframes); + return property_obligations_rec(tmp, current, no_timeframes, lasso); } else if(property_expr.id() == ID_implies) { // we rely on NNF auto &implies_expr = to_implies_expr(property_expr); auto tmp = or_exprt{not_exprt{implies_expr.lhs()}, implies_expr.rhs()}; - return property_obligations_rec(tmp, current, no_timeframes); + return property_obligations_rec(tmp, current, no_timeframes, lasso); } else if(property_expr.id() == ID_if) { @@ -514,10 +574,12 @@ static obligationst property_obligations_rec( auto cond = instantiate_state_predicate(if_expr.cond(), current, no_timeframes); auto obligations_true = - property_obligations_rec(if_expr.true_case(), current, no_timeframes) + property_obligations_rec( + if_expr.true_case(), current, no_timeframes, lasso) .conjunction(); auto obligations_false = - property_obligations_rec(if_expr.false_case(), current, no_timeframes) + property_obligations_rec( + if_expr.false_case(), current, no_timeframes, lasso) .conjunction(); return obligationst{ std::max(obligations_true.first, obligations_false.first), @@ -529,7 +591,7 @@ static obligationst property_obligations_rec( { // drop reduntant type casts return property_obligations_rec( - to_typecast_expr(property_expr).op(), current, no_timeframes); + to_typecast_expr(property_expr).op(), current, no_timeframes, lasso); } else if(property_expr.id() == ID_not) { @@ -541,7 +603,7 @@ static obligationst property_obligations_rec( if(op_negated_opt.has_value()) { return property_obligations_rec( - op_negated_opt.value(), current, no_timeframes); + op_negated_opt.value(), current, no_timeframes, lasso); } else if( op.id() == ID_sva_strong || op.id() == ID_sva_weak || @@ -583,7 +645,8 @@ static obligationst property_obligations_rec( auto &sva_implies_expr = to_sva_implies_expr(property_expr); auto implies_expr = implies_exprt{sva_implies_expr.lhs(), sva_implies_expr.rhs()}; - return property_obligations_rec(implies_expr, current, no_timeframes); + return property_obligations_rec( + implies_expr, current, no_timeframes, lasso); } else if(property_expr.id() == ID_sva_iff) { @@ -591,7 +654,7 @@ static obligationst property_obligations_rec( // Note that this is not an SVA sequence operator. auto &sva_iff_expr = to_sva_iff_expr(property_expr); auto equal_expr = equal_exprt{sva_iff_expr.lhs(), sva_iff_expr.rhs()}; - return property_obligations_rec(equal_expr, current, no_timeframes); + return property_obligations_rec(equal_expr, current, no_timeframes, lasso); } else if( property_expr.id() == ID_sva_overlapped_implication || @@ -634,8 +697,8 @@ static obligationst property_obligations_rec( } // Get obligations for RHS - auto rhs_obligations_rec = - property_obligations_rec(implication.rhs(), t_rhs, no_timeframes); + auto rhs_obligations_rec = property_obligations_rec( + implication.rhs(), t_rhs, no_timeframes, lasso); for(auto &rhs_obligation : rhs_obligations_rec.map) { @@ -694,7 +757,7 @@ static obligationst property_obligations_rec( { auto obligations_rec = property_obligations_rec( - followed_by.consequent(), property_start, no_timeframes) + followed_by.consequent(), property_start, no_timeframes, lasso) .conjunction(); disjuncts.push_back( @@ -748,6 +811,67 @@ static obligationst property_obligations_rec( /*******************************************************************\ +Function: property_obligations_lasso + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +obligationst property_obligations_lasso( + const exprt &property_expr, + const mp_integer &no_timeframes) +{ + PRECONDITION(no_timeframes >= 1); + + auto uses_lasso_pred = [](const exprt &expr) + { + return expr.id() == ID_F || expr.id() == ID_AF || + expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_s_until || + expr.id() == ID_U || expr.id() == ID_strong_R; + }; + + // Does the property use a lasso? This assumes NNF. + if(!has_subexpr(property_expr, uses_lasso_pred)) + return {}; + + obligationst obligations; + + // This iterates over the possible shapes of a lasso. + // This is quadratic in the bound. + // State loop.start is required to be equal to state loop.end. + bmc_lassot lasso; + + for(lasso.end = 1; lasso.end < no_timeframes; ++lasso.end) + for(lasso.start = 0; lasso.start < lasso.end; ++lasso.start) + { + auto obligations_lasso = + property_obligations_rec(property_expr, 0, no_timeframes, lasso); + + auto lasso_symbol = ::lasso_symbol(lasso.start, lasso.end); + + for(auto &[_, expr_vector] : obligations_lasso.map) + { + for(auto &expr : expr_vector) + { + // add the lasso constraint + auto new_expr = implies_exprt{lasso_symbol, expr}; + + // override the timeframe of the obligation to use the + // end of the lasso -- we want to see the entire lasso + obligations.add(lasso.end, new_expr); + } + } + } + + return obligations; +} + +/*******************************************************************\ + Function: property_obligations Inputs: @@ -760,9 +884,29 @@ Function: property_obligations obligationst property_obligations( const exprt &property_expr, + message_handlert &message_handler, const mp_integer &no_timeframes) { - return property_obligations_rec(property_expr, 0, no_timeframes); + // The word-level BMC encoding works on NNF. + auto nnf = property_nnf(property_expr); + + messaget message{message_handler}; + message.debug() << "NNF: " << format(nnf) << messaget::eom; + + // A counterexample to an LTL property can have one of two forms. + // 1. A linear, finite path + // 2. An infinite path, given in the form of a lasso, i.e., + // a stem followed by a loop. + + obligationst obligations; + + // Form 1 -- linear path + auto form_1 = property_obligations_rec(nnf, 0, no_timeframes, {}); + + // Form 2 -- lasso + auto form_2 = property_obligations_lasso(nnf, no_timeframes); + + return obligations_union(form_1, form_2); } /*******************************************************************\ @@ -785,7 +929,8 @@ exprt::operandst property( // The first element of the pair is the length of the // counterexample, and the second is the condition that // must be valid for the property to hold. - auto obligations = property_obligations(property_expr, no_timeframes); + auto obligations = + property_obligations(property_expr, message_handler, no_timeframes); // Map obligations onto timeframes. exprt::operandst prop_handles{no_timeframes, true_exprt()};