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..a806f3a9f --- /dev/null +++ b/regression/smv/LTL/smv_ltlspec_or2.desc @@ -0,0 +1,9 @@ +CORE +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/regression/verilog/SVA/sva_or1.bmc.desc b/regression/verilog/SVA/sva_or1.bmc.desc new file mode 100644 index 000000000..4cc348bf8 --- /dev/null +++ b/regression/verilog/SVA/sva_or1.bmc.desc @@ -0,0 +1,9 @@ +KNOWNBUG +sva_or1.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Wrong answer on ##[*] diff --git a/regression/verilog/SVA/sva_or1.sv b/regression/verilog/SVA/sva_or1.sv new file mode 100644 index 000000000..32328f249 --- /dev/null +++ b/regression/verilog/SVA/sva_or1.sv @@ -0,0 +1,7 @@ +module main(input a); + + initial p0: assert property ((s_eventually a) or (always !a)); + initial p1: assert property ((s_eventually a) or not ##[*] a); + initial p2: assert property ((##[*] a) or (always !a)); + +endmodule 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..a174883b1 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,35 +454,80 @@ 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) { - // 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(); + auto &binary_expr = to_binary_expr(property_expr); + auto &p = binary_expr.lhs(); + auto &q = binary_expr.rhs(); - // Once we reach the end of the unwinding, replace X(p W q) by 'true'. - auto tmp = or_exprt{ - q, - (current + 1) < no_timeframes ? and_exprt{p, X_exprt{property_expr}} : p}; + // p has to to be true until (not including) q is true + exprt::operandst q_disjuncts; + obligationst obligations; + + mp_integer start, end; + + if(lasso.has_value()) + { + start = std::min(current, lasso.value().start); + end = lasso.value().end; + } + else + { + start = current; + end = no_timeframes; + } + + for(mp_integer j = start; j < end; ++j) + { + auto q_rec = property_obligations_rec(q, j, no_timeframes, lasso); + q_disjuncts.push_back(q_rec.conjunction().second); - return property_obligations_rec(tmp, current, no_timeframes); + auto p_rec = property_obligations_rec(p, j, no_timeframes, lasso); + auto cond = + or_exprt{p_rec.conjunction().second, disjunction(q_disjuncts)}; + + obligations.add(current, cond); + } + + return obligations; } else if(property_expr.id() == ID_R) { - // we expand: p R q <=> q ∧ (p ∨ X(p R q)) auto &R_expr = to_R_expr(property_expr); auto &p = R_expr.lhs(); auto &q = R_expr.rhs(); - // Once we reach the end of the unwinding, we replace X(p R q) by - // true, and hence the expansion becomes "q" only. - exprt expansion = (current + 1) < no_timeframes - ? and_exprt{q, or_exprt{p, X_exprt{property_expr}}} - : q; + mp_integer start, end; + + if(lasso.has_value()) + { + start = std::min(current, lasso.value().start); + end = lasso.value().end; + } + else + { + start = current; + end = no_timeframes; + } + + // q has to be true until (including) p is true + exprt::operandst p_disjuncts; + obligationst obligations; + + for(mp_integer j = start; j < end; ++j) + { + auto q_rec = property_obligations_rec(q, j, no_timeframes, lasso); + auto cond = + or_exprt{q_rec.conjunction().second, disjunction(p_disjuncts)}; + obligations.add(current, cond); - return property_obligations_rec(expansion, current, no_timeframes); + auto p_rec = property_obligations_rec(p, j, no_timeframes, lasso); + p_disjuncts.push_back(p_rec.conjunction().second); + } + + return obligations; } else if(property_expr.id() == ID_strong_R) { @@ -440,7 +537,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 +545,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 +553,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 +563,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 +579,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 +597,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 +613,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 +630,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 +642,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 +684,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 +693,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 +736,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 +796,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 +850,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 +923,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 +968,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()};