diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 64cbde3fd..a6c172a6b 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -359,22 +359,27 @@ namespace for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { + spot::strategy_like_t strat + { + spot::strategy_like_t::realizability_code::UNKNOWN, + nullptr, + bddfalse + }; // If we want to print a game, // we never use the direct approach - spot::strategy_like_t strat{0, nullptr, bddfalse}; if (!want_game) strat = spot::try_create_direct_strategy(*sub_f, *sub_o, *gi); switch (strat.success) { - case -1: + case spot::strategy_like_t::realizability_code::UNREALIZABLE: { std::cout << "UNREALIZABLE" << std::endl; safe_tot_time(); return 1; } - case 0: + case spot::strategy_like_t::realizability_code::UNKNOWN: { auto arena = spot::ltl_to_game(*sub_f, *sub_o, *gi); if (gi->bv) @@ -400,14 +405,15 @@ namespace if (!opt_real) { spot::strategy_like_t sl; - sl.success = 1; + sl.success = + spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR; sl.strat_like = spot::create_strategy(arena, *gi); sl.glob_cond = bddfalse; strategies.push_back(sl); } break; } - case 1: + case spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR: { // the direct approach yielded a strategy // which can now be minimized @@ -439,7 +445,7 @@ namespace } SPOT_FALLTHROUGH; } - case 2: + case spot::strategy_like_t::realizability_code::REALIZABLE_DTGBA: if (!opt_real) strategies.push_back(strat); break; @@ -498,8 +504,11 @@ namespace } else { - assert(std::all_of(strategies.begin(), strategies.end(), - [](const auto& sl){return sl.success == 1; }) + assert(std::all_of( + strategies.begin(), strategies.end(), + [](const auto& sl) + {return sl.success == + spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR; }) && "ltlsynt: Can not handle TGBA as strategy."); tot_strat = strategies.front().strat_like; for (size_t i = 1; i < strategies.size(); ++i) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index a7c2edafc..8b9aaba66 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1956,19 +1956,19 @@ namespace spot { switch (strat_vec[i].success) { - case -1: + case strategy_like_t::realizability_code::UNREALIZABLE: throw std::runtime_error("strategies_to_aig(): Partial strat is " "not feasible!"); - case 0: + case strategy_like_t::realizability_code::UNKNOWN: throw std::runtime_error("strategies_to_aig(): Partial strat has " "unknown status!"); - case 1: + case strategy_like_t::realizability_code::REALIZABLE_REGULAR: { strategies.push_back(strat_vec[i].strat_like); outs_used.push_back(outs[i]); break; } - case 2: + case strategy_like_t::realizability_code::REALIZABLE_DTGBA: throw std::runtime_error("strategies_to_aig(): TGBA not " "yet supported."); default: diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index c0a655d73..5d14c2155 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1246,175 +1246,208 @@ namespace spot const std::vector& output_aps, synthesis_info &gi) { - formula_2_inout_props form2props(output_aps); auto vs = gi.verbose_stream; + auto& bv = gi.bv; if (vs) - *vs << "trying to create strategy directly\n"; + *vs << "trying to create strategy directly for " << f << '\n'; auto ret_sol_maybe = [&vs]() - { - if (vs) - *vs << "direct strategy might exist but was not found.\n"; - return strategy_like_t{0, nullptr, bddfalse}; - }; + { + if (vs) + *vs << "direct strategy might exist but was not found.\n"; + return strategy_like_t{ + strategy_like_t::realizability_code::UNKNOWN, + nullptr, + bddfalse}; + }; auto ret_sol_none = [&vs]() { if (vs) - *vs << "no direct strategy exists.\n"; - return strategy_like_t{-1, nullptr, bddfalse}; + *vs << "no strategy exists.\n"; + return strategy_like_t{ + strategy_like_t::realizability_code::UNREALIZABLE, + nullptr, + bddfalse}; }; + auto ret_sol_exists = [&vs](auto strat) + { + if (vs) { - if (vs) - { - *vs << "direct strategy was found.\n" - << "direct strat has " << strat->num_states() - << " states and " << strat->num_sets() << " colors\n"; - } - return strategy_like_t{1, strat, bddfalse}; - }; + *vs << "direct strategy was found.\n" + << "direct strat has " << strat->num_states() + << " states and " << strat->num_sets() << " colors\n"; + } + return strategy_like_t{ + strategy_like_t::realizability_code::REALIZABLE_REGULAR, + strat, + bddfalse}; + }; + formula_2_inout_props form2props(output_aps); - // We need a lot of look-ups auto output_aps_set = std::set(output_aps.begin(), - output_aps.end()); + output_aps.end()); - bool is_and = f.is(op::And); - formula f_g, f_equiv; - // Rewrite a conjunction as G(…) ∧ … - if (is_and) + formula f_g = formula::tt(), f_left, f_right; + + // If we have a formula like G(b₁) ∧ (φ ↔ GFb₂), we extract b₁ and + // continue the construction for (φ ↔ GFb₂). + if (f.is(op::And)) + { + if (f.size() != 2) + return ret_sol_maybe(); + if (f[0].is(op::G) && f[0][0].is_boolean()) { - if (f.size() != 2) - return ret_sol_maybe(); - if (f[1].is(op::G)) - f = formula::And({f[1], f[0]}); - f_equiv = f[1]; f_g = f[0]; + f = f[1]; } - else + else if (f[1].is(op::G) && f[1][0].is_boolean()) { - f_equiv = f; - f_g = spot::formula::tt(); + f_g = f[1]; + f = f[0]; } + else + return ret_sol_maybe(); + } + if (f.is(op::Equiv)) + { + auto [left_ins, left_outs] = form2props.aps_of(f[0]); + auto [right_ins, right_outs] = form2props.aps_of(f[1]); - if (!f_equiv.is(op::Equiv) || (!f_g.is_tt() && (!f_g.is(op::G) - || !f_g[0].is_boolean()))) - return ret_sol_maybe(); -// stopwatch sw; - twa_graph_ptr res; - - formula left = f_equiv[0], - right = f_equiv[1]; - - auto [left_ins, left_outs] = form2props.aps_of(left); - auto [right_ins, right_outs] = form2props.aps_of(right); - - bool has_left_outs = !left_outs.empty(); - bool has_left_ins = !left_ins.empty(); - bool has_right_outs = !right_outs.empty(); - bool has_right_ins = !right_ins.empty(); - - // Try to rewrite the equivalence as f(b1) <-> f(b2) where b2 has not any - // input - if (has_right_ins) + auto properties_vector = [](const formula& f, + const std::set& ins, + const std::set& outs) + { + return std::vector + { + f.is({op::G, op::F}) && f[0][0].is_boolean() && ins.empty(), + f.is_syntactic_recurrence() && outs.empty(), + // f is FG(bool) + f.is({op::F, op::G}) && f[0][0].is_boolean() && ins.empty(), + f.is_syntactic_persistence() && outs.empty() + }; + }; + // We need to detect + // GF(outs) ↔ recurrence(ins), + // recurrence(ins) ↔ GF(outs), + // FG(outs) ↔ persistence(ins), + // persistence(ins) ↔ FG(outs) + const auto left_properties = properties_vector(f[0], left_ins, left_outs), + right_properties = properties_vector(f[1], right_ins, right_outs); + unsigned combin = -1U; + for (unsigned i = 0; i < 4; ++i) + { + if (left_properties[i] && right_properties[(i%2) ? (i-1) : (i+1)]) + { + combin = i; + break; + } + } + if (combin == -1U) + return ret_sol_maybe(); + + // left is the recurrence (resp. persistence) + // right is GF(outs) (resp. GF(outs)) + // If f[0] is GF or FG + f_left = f[(combin+1)%2]; + f_right = f[combin%2]; + if (!(combin%2)) { - std::swap(left, right); - std::swap(has_left_ins, has_right_ins); - std::swap(has_left_outs, has_right_outs); std::swap(left_ins, right_ins); std::swap(left_outs, right_outs); } - // We need to have f(inputs) <-> f(outputs) - if (has_right_ins || has_left_outs || !has_right_outs) - return ret_sol_maybe(); - bool is_gf_bool_right = right.is({op::G, op::F}); - bool is_fg_bool_right = right.is({op::F, op::G}); + auto trans = create_translator(gi); + trans.set_type(combin < 2 ? postprocessor::Buchi + : postprocessor::CoBuchi); + trans.set_pref(postprocessor::Deterministic | postprocessor::Complete); - // Now we have to detect if we have persistence(ins) <-> FG(outs) - // or Büchi(ins) <-> GF(outs). + stopwatch sw; + if (bv) + sw.start(); + auto res = trans.run(f_left); - bool is_ok = ((is_gf_bool_right && left.is_syntactic_recurrence()) - || (is_fg_bool_right && left.is_syntactic_guarantee())); - - // TODO: synthesis_info not updated - // TODO: Verbose - auto& bv = gi.bv; - stopwatch sw; - if (is_ok) + if (bv) { - bool right_bool = right[0][0].is_boolean(); - if (!right_bool) - return ret_sol_maybe(); - auto trans = create_translator(gi); - trans.set_type(postprocessor::Buchi); - trans.set_pref(postprocessor::Deterministic | postprocessor::Complete); - - - auto right_sub = right[0][0]; - - if (bv) - sw.start(); - res = trans.run(left); - if (bv) - { - auto delta = sw.stop(); - bv->trans_time += delta; - if (vs) - *vs << "tanslating formula done in " << delta << " seconds\n"; - } - - for (auto& out : right_outs) - res->register_ap(out.ap_name()); - if (!is_deterministic(res)) - return ret_sol_maybe(); - bdd form_bdd = bddtrue; - if (is_and) - { - bdd output_bdd = bddtrue; - for (auto &out : output_aps_set) - output_bdd &= bdd_ithvar(res->register_ap(out)); - form_bdd = f_g.is_tt() ? (bdd) bddtrue : - formula_to_bdd(f_g[0], - res->get_dict(), res); - if (bdd_exist(form_bdd, output_bdd) != bddtrue) - return ret_sol_maybe(); - } - bdd right_bdd = formula_to_bdd(right_sub, res->get_dict(), res); - bdd neg_right_bdd = bdd_not(right_bdd); - assert(right_ins.empty()); - const bool is_true = res->acc().is_t(); - scc_info si(res, scc_info_options::NONE); - for (auto& e : res->edges()) - { - // Here the part describing the outputs is based on the fact that - // they must be seen infinitely often. As these edges are seen - // finitely often, we can let the minimization choose the value. - if (si.scc_of(e.src) == si.scc_of(e.dst)) - { - if (e.acc || is_true) - e.cond &= (right_bdd); - else - e.cond &= (neg_right_bdd); - } - // form_bdd has to be true all the time. So we cannot only do it - // between SCCs. - if (!bdd_have_common_assignment(e.cond, form_bdd)) - return ret_sol_none(); - e.acc = {}; - } - - bdd output_bdd = bddtrue; - for (auto &out : output_aps_set) - output_bdd &= bdd_ithvar(res->register_ap(out)); - - set_synthesis_outputs(res, output_bdd); - res->set_acceptance(acc_cond::acc_code::t()); - - res->prop_complete(trival::maybe()); - return ret_sol_exists(res); + auto delta = sw.stop(); + bv->trans_time += delta; + if (vs) + *vs << "tanslating formula done in " << delta << " seconds\n"; } - return ret_sol_maybe(); + + if (!is_deterministic(res)) + return ret_sol_maybe(); + for (auto& out : right_outs) + res->register_ap(out.ap_name()); + + // The BDD that describes the content of the G in a conjunction + bdd g_bdd = bddtrue; + + // Convert the set of outputs to a BDD + bdd output_bdd = bddtrue; + for (auto &out : output_aps_set) + output_bdd &= bdd_ithvar(res->register_ap(out)); + + if (!f_g.is_tt()) + { + g_bdd = formula_to_bdd(f_g[0], res->get_dict(), res); + // If the content of G is not input-complete, a simple strategy for + // env is to play this missing value. + if (bdd_exist(g_bdd, output_bdd) != bddtrue) + { + return ret_sol_none(); + } + } + + // For the GF(outs) (resp. GF(outs)), the content and its negation can be + // converted to a BDD. + bdd right_bdd, neg_right_bdd; + if (combin < 2) + { + right_bdd = formula_to_bdd(f_right[0][0], res->get_dict(), res); + neg_right_bdd = bdd_not(right_bdd); + } + else + { + neg_right_bdd = formula_to_bdd(f_right[0][0], res->get_dict(), res); + right_bdd = bdd_not(neg_right_bdd); + } + // Monitor is a special case. As we color accepting transitions, if the + // acceptance is true, we cannot say that a transition is accepting if + // a color is seen. + const bool is_true = res->acc().is_t(); + scc_info si(res, scc_info_options::NONE); + for (auto& e : res->edges()) + { + // Here the part describing the outputs is based on the fact that + // they must be seen infinitely often. As these edges are seen + // finitely often, we can let the minimization choose the value. + if (si.scc_of(e.src) == si.scc_of(e.dst)) + { + if (e.acc || is_true) + e.cond &= right_bdd; + else + e.cond &= neg_right_bdd; + } + // g_bdd has to be true all the time. So we cannot only do it + // between SCCs. + e.cond &= g_bdd; + if (e.cond == bddfalse) + return ret_sol_maybe(); + // The recurrence is Büchi but the strategy is a monitor. We need + // to remove the color. + e.acc = {}; + } + + set_synthesis_outputs(res, output_bdd); + res->set_acceptance(acc_cond::acc_code::t()); + + res->prop_complete(trival::maybe()); + return ret_sol_exists(res); + } + else + return ret_sol_maybe(); } } // spot diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 80c8a33eb..e69d2982c 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -224,11 +224,17 @@ namespace spot struct SPOT_API strategy_like_t { - // -1 : Unrealizable - // 0 : Unknown - // 1 : Realizable -> regular strat - // 2 : Realizable -> strat is DTGBA and a glob_cond // todo - int success; + + enum class realizability_code + { + UNREALIZABLE, + UNKNOWN, + REALIZABLE_REGULAR, + // strat is DTGBA and a glob_cond + REALIZABLE_DTGBA + }; + + realizability_code success; twa_graph_ptr strat_like; bdd glob_cond; }; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 4fbba5fd8..da93550cc 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -192,7 +192,7 @@ ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ diff out exp cat >exp < GFb tanslating formula done in X seconds direct strategy was found. direct strat has 1 states and 0 colors @@ -202,7 +202,7 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < GFb tanslating formula done in X seconds direct strategy was found. direct strat has 1 states and 0 colors @@ -214,7 +214,7 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < GFe tanslating formula done in X seconds direct strategy was found. direct strat has 16 states and 0 colors @@ -225,7 +225,7 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < G(i1 <-> o0) direct strategy might exist but was not found. translating formula done in X seconds automaton has 2 states and 3 colors @@ -551,3 +551,86 @@ grep "both.*but 'b' is unlisted" stderr ltlsynt -f 'GFa | FGb | GFc' 2>stderr && : test $? -eq 2 grep "one of --ins or --outs" stderr + +# Try to find a direct strategy for GFa <-> GFb and a direct strategy for +# Gc +cat >exp < GFb +tanslating formula done in X seconds +direct strategy was found. +direct strat has 1 states and 0 colors +final strategy has 1 states and 2 edges +minimization took X seconds +trying to create strategy directly for Gc +direct strategy might exist but was not found. +translating formula done in X seconds +automaton has 1 states and 1 colors +LAR construction done in X seconds +DPA has 1 states, 2 colors +split inputs and outputs done in X seconds +automaton has 2 states +solving game with acceptance: parity max odd 4 +game solved in X seconds +EOF +ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +# Try to find a direct strategy for (GFa <-> GFb) & Gc. THe order should not +# impact the result +for f in "(GFa <-> GFb) & Gc" "(GFb <-> GFa) & Gc" \ + "Gc & (GFa <-> GFb)" "Gc & (GFb <-> GFa)" +do +cat >exp < out + sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx + diff outx exp +done + +# # Ltlsynt should be able to detect that G(a&c) is not input-complete so it is +# # impossible to find a strategy. +cat >exp < GFa) & G(a & c) +tanslating formula done in X seconds +no strategy exists. +EOF +ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\ + --decompose=0 2> out || true +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +# # Ltlsynt should be able to create a strategy when the last G +# is input-complete. +cat >exp < GFa) & G((a & c) | (!a & !c)) +tanslating formula done in X seconds +direct strategy was found. +direct strat has 1 states and 0 colors +final strategy has 1 states and 2 edges +minimization took X seconds +EOF +ltlsynt -f '(GFb <-> GFa) && (G((a&c)|(!a&!c)))' --outs=b,c --verbose\ + --verify --decompose=0 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +# Direct strategy for persistence + +cat >exp < FGb +tanslating formula done in X seconds +direct strategy was found. +direct strat has 2 states and 0 colors +final strategy has 2 states and 3 edges +minimization took X seconds +EOF +ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp \ No newline at end of file