diff --git a/NEWS b/NEWS index 61f7c6df7..b6ad95362 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,13 @@ New in spot 2.11.6.dev (not yet released) will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. + - ltlsynt will no check for output atomic propositions that always + have the same polarity in the specification. When this happens, + these output APs are replaced by true or false before running the + synthesis pipeline, and the resulting game, Mealy machine, or + Aiger circuit is eventually patched to include that constant + output. This can be disabled with --polarity=no. + Library: - The following new trivial simplifications have been implemented for SEREs: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 35ac4194b..d2d85caa7 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -55,6 +55,7 @@ enum OPT_HIDE, OPT_INPUT, OPT_OUTPUT, + OPT_POLARITY, OPT_PRINT, OPT_PRINT_AIGER, OPT_PRINT_HOA, @@ -101,6 +102,9 @@ static const argp_option options[] = { "decompose", OPT_DECOMPOSE, "yes|no", 0, "whether to decompose the specification as multiple output-disjoint " "problems to solve independently (enabled by default)", 0 }, + { "polarity", OPT_POLARITY, "yes|no", 0, + "whether to remove atomic propositions that always have the same " + "polarity in the formula to speed things up (enabled by default)", 0 }, { "simplify", OPT_SIMPLIFY, "no|bisim|bwoa|sat|bisim-sat|bwoa-sat", 0, "simplification to apply to the controller (no) nothing, " "(bisim) bisimulation-based reduction, (bwoa) bisimulation-based " @@ -236,6 +240,7 @@ static bool decompose_values[] = }; ARGMATCH_VERIFY(decompose_args, decompose_values); bool opt_decompose_ltl = true; +bool opt_polarity = true; static const char* const simplify_args[] = { @@ -268,8 +273,35 @@ namespace }; static void - dispatch_print_hoa(const spot::const_twa_graph_ptr& game) + dispatch_print_hoa(spot::twa_graph_ptr& game, + const std::vector* input_aps = nullptr, + const spot::relabeling_map* rm = nullptr) { + if (rm && !rm->empty()) // Add any AP we removed + { + assert(input_aps); + auto& sp = spot::get_state_players(game); + + bdd add = bddtrue; + for (auto [k, v]: *rm) + { + int i = game->register_ap(k); + // skip inputs + if (std::find(input_aps->begin(), input_aps->end(), + k.ap_name()) != input_aps->end()) + continue; + if (v.is_tt()) + add &= bdd_ithvar(i); + else if (v.is_ff()) + add &= bdd_nithvar(i); + } + for (auto& e: game->edges()) + if (sp[e.src]) + e.cond &= add; + set_synthesis_outputs(game, + get_synthesis_outputs(game) + & bdd_support(add)); + } if (opt_dot) spot::print_dot(std::cout, game, opt_print_hoa_args); else if (opt_print_pg) @@ -355,10 +387,11 @@ namespace } static int - solve_formula(const spot::formula& f, + solve_formula(spot::formula original_f, const std::vector& input_aps, const std::vector& output_aps) { + spot::formula f = original_f; if (opt_csv) // reset benchmark data gi->bv = spot::synthesis_info::bench_var(); spot::stopwatch sw; @@ -371,47 +404,92 @@ namespace gi->bv->total_time = sw.stop(); }; + // Check if some output propositions are always in positive form, + // or always in negative form. + // In syntcomp, this occurs more frequently for input variables than + // output variable. See issue #529 for some examples. + spot::relabeling_map rm; + if (opt_polarity) + { + std::set lits = spot::collect_litterals(f); + for (const std::string& ap: output_aps) + { + spot::formula pos = spot::formula::ap(ap); + spot::formula neg = spot::formula::Not(pos); + bool has_pos = lits.find(pos) != lits.end(); + bool has_neg = lits.find(neg) != lits.end(); + if (has_pos && !has_neg) + rm[pos] = spot::formula::tt(); + else if (has_neg && !has_pos) + rm[pos] = spot::formula::ff(); + } + for (const std::string& ap: input_aps) + { + spot::formula pos = spot::formula::ap(ap); + spot::formula neg = spot::formula::Not(pos); + bool has_pos = lits.find(pos) != lits.end(); + bool has_neg = lits.find(neg) != lits.end(); + if (has_pos && !has_neg) + rm[pos] = spot::formula::ff(); + else if (has_neg && !has_pos) + rm[pos] = spot::formula::tt(); + } + if (!rm.empty()) + { + if (gi->verbose_stream) + { + *gi->verbose_stream << ("the following APs are polarized, " + "they can be replaced by constants:\n"); + for (auto [k, v]: rm) + *gi->verbose_stream << " " << k << " := " << v <<'\n'; + } + f = spot::relabel_apply(f, &rm); + if (gi->verbose_stream) + *gi->verbose_stream << "new formula: " << f << '\n'; + } + } + std::vector sub_form; std::vector> sub_outs; if (opt_decompose_ltl) { auto subs = split_independant_formulas(f, output_aps); if (gi->verbose_stream) - { - *gi->verbose_stream << "there are " - << subs.first.size() - << " subformulas\n"; - } + { + *gi->verbose_stream << "there are " + << subs.first.size() + << " subformulas\n"; + } if (subs.first.size() > 1) - { - sub_form = subs.first; - sub_outs = subs.second; - } + { + sub_form = subs.first; + sub_outs = subs.second; + } } // When trying to split the formula, we can apply transformations that // increase its size. This is why we will use the original formula if it // has not been cut. if (sub_form.empty()) - { - sub_form = { f }; - sub_outs.resize(1); - std::transform(output_aps.begin(), output_aps.end(), - std::inserter(sub_outs[0], sub_outs[0].begin()), - [](const std::string& name) { - return spot::formula::ap(name); - }); - } + { + sub_form = { f }; + sub_outs.resize(1); + for (const std::string& apstr: output_aps) + { + spot::formula ap = spot::formula::ap(apstr); + if (rm.find(ap) == rm.end()) + sub_outs[0].insert(ap); + } + } std::vector> sub_outs_str; std::transform(sub_outs.begin(), sub_outs.end(), std::back_inserter(sub_outs_str), - [](const auto& forms) - { - std::vector r; - r.reserve(forms.size()); - for (auto f : forms) - r.push_back(f.ap_name()); - return r; - }); + [](const auto& forms) { + std::vector r; + r.reserve(forms.size()); + for (auto f: forms) + r.push_back(f.ap_name()); + return r; + }); assert((sub_form.size() == sub_outs.size()) && (sub_form.size() == sub_outs_str.size())); @@ -463,7 +541,7 @@ namespace } if (want_game) { - dispatch_print_hoa(arena); + dispatch_print_hoa(arena, &input_aps, &rm); continue; } if (!spot::solve_game(arena, *gi)) @@ -552,7 +630,7 @@ namespace sw2.start(); saig = spot::mealy_machines_to_aig(mealy_machines, opt_print_aiger, input_aps, - sub_outs_str); + sub_outs_str, &rm); if (gi->bv) { gi->bv->aig_time = sw2.stop(); @@ -584,6 +662,27 @@ namespace for (size_t i = 1; i < mealy_machines.size(); ++i) tot_strat = spot::mealy_product(tot_strat, mealy_machines[i].mealy_like); + if (!rm.empty()) // Add any AP we removed + { + bdd add = bddtrue; + for (auto [k, v]: rm) + { + int i = tot_strat->register_ap(k); + // skip inputs (they are don't care) + if (std::find(input_aps.begin(), input_aps.end(), k.ap_name()) + != input_aps.end()) + continue; + if (v.is_tt()) + add &= bdd_ithvar(i); + else if (v.is_ff()) + add &= bdd_nithvar(i); + } + for (auto& e: tot_strat->edges()) + e.cond &= add; + set_synthesis_outputs(tot_strat, + get_synthesis_outputs(tot_strat) + & bdd_support(add)); + } printer.print(tot_strat, timer_printer_dummy); } @@ -597,7 +696,7 @@ namespace // TODO: different options to speed up verification?! spot::translator trans(gi->dict, &gi->opt); - auto neg_spec = trans.run(spot::formula::Not(f)); + auto neg_spec = trans.run(spot::formula::Not(original_f)); if (saig) { // Test the aiger @@ -952,6 +1051,10 @@ parse_opt(int key, char *arg, struct argp_state *) split_aps(arg, *all_output_aps); break; } + case OPT_POLARITY: + opt_polarity = XARGMATCH("--polarity", arg, + decompose_args, decompose_values); + break; case OPT_PRINT: opt_print_pg = true; gi->force_sbacc = true; diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index e1f11372d..74790f1c4 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015, 2018 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2015, 2018, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -63,4 +63,72 @@ namespace spot res &= bdd_ithvar(a->register_ap(f)); return res; } + + atomic_prop_set collect_litterals(formula f) + { + atomic_prop_set res; + + // polirity: 0 = negative, 1 = positive, 2 or more = both. + auto rec = [&res](formula f, unsigned polarity, auto self) + { + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::eword: + return; + case op::ap: + if (polarity != 0) + res.insert(f); + if (polarity != 1) + res.insert(formula::Not(f)); + return; + case op::Not: + case op::NegClosure: + case op::NegClosureMarked: + self(f[0], polarity ^ 1, self); + return; + case op::Xor: + case op::Equiv: + self(f[0], 2, self); + self(f[1], 2, self); + return; + case op::Implies: + case op::UConcat: + self(f[0], polarity ^ 1, self); + self(f[1], polarity, self); + return; + case op::U: + case op::R: + case op::W: + case op::M: + case op::EConcat: + case op::EConcatMarked: + self(f[0], polarity, self); + self(f[1], polarity, self); + return; + case op::X: + case op::F: + case op::G: + case op::Closure: + case op::Or: + case op::OrRat: + case op::And: + case op::AndRat: + case op::AndNLM: + case op::Concat: + case op::Fusion: + case op::Star: + case op::FStar: + case op::first_match: + case op::strong_X: + for (formula c: f) + self(c, polarity, self); + return; + } + }; + rec(f, 1, rec); + return res; + } + } diff --git a/spot/tl/apcollect.hh b/spot/tl/apcollect.hh index 012916381..42788dc9c 100644 --- a/spot/tl/apcollect.hh +++ b/spot/tl/apcollect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -59,5 +59,15 @@ namespace spot SPOT_API bdd atomic_prop_collect_as_bdd(formula f, const twa_ptr& a); + + /// \brief Collect the litterals occuring in f + /// + /// This function records each atomic proposition occurring in f + /// along with the polarity of its occurrence. For instance if the + /// formula is `G(a -> b) & X(!b & c)`, then this will output `{!a, + /// b, !b, c}`. + SPOT_API + atomic_prop_set collect_litterals(formula f); + /// @} } diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 7d724b124..e4ba12444 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1541,10 +1541,11 @@ namespace // outputs into an Aig static aig_ptr auts_to_aiger(const std::vector>& - strat_vec, + strat_vec, const char* mode, const std::vector& unused_ins = {}, - const std::vector& unused_outs = {}) + const std::vector& unused_outs = {}, + const relabeling_map* rm = nullptr) { // The aiger circuit can currently noly encode separated mealy machines @@ -1619,6 +1620,23 @@ namespace unused_outs.cbegin(), unused_outs.cend()); + if (rm) + // If we have removed some APs from the original formula, they + // might have dropped out of the output_names list (depending on + // how we split the formula), but they should not have dropped + // from the input_names list. So let's fix the output_names + // lists by adding anything that's not an input and not already + // there. + for (auto [k, v]: *rm) + { + const std::string s = k.ap_name(); + if (std::find(input_names_all.begin(), input_names_all.end(), s) + == input_names_all.end() + && std::find(output_names_all.begin(), output_names_all.end(), s) + == output_names_all.end()) + output_names_all.push_back(s); + } + // Decide on which outcond to use // The edges of the automaton all have the form in&out // due to the unsplit @@ -1962,7 +1980,7 @@ namespace } //Use the best sol circuit.reapply_(sf, ss); - trace << "Finished encoding, reasssigning\n" + trace << "Finished encoding, reassigning\n" << "Final gate count is " << circuit.num_gates() << '\n'; // Reset them for (unsigned i = 0; i < n_outs; ++i) @@ -1970,7 +1988,25 @@ namespace // Add the unused propositions const unsigned n_outs_all = output_names_all.size(); for (unsigned i = n_outs; i < n_outs_all; ++i) - circuit.set_output(i, circuit.aig_false()); + if (rm) + { + if (auto to = rm->find(formula::ap(output_names_all[i])); + to != rm->end()) + { + if (to->second.is_tt()) + { + circuit.set_output(i, circuit.aig_true()); + continue; + } + else if (to->second.is_ff()) + { + circuit.set_output(i, circuit.aig_false()); + continue; + } + } + } + else + circuit.set_output(i, circuit.aig_false()); for (unsigned i = 0; i < n_latches; ++i) circuit.set_next_latch(i, bdd2var_min(latch[i], bddfalse)); return circuit_ptr; @@ -2002,8 +2038,9 @@ namespace spot aig_ptr mealy_machine_to_aig(const twa_graph_ptr &m, const char *mode, - const std::vector& ins, - const std::vector& outs) + const std::vector& ins, + const std::vector& outs, + const relabeling_map* rm) { if (!m) throw std::runtime_error("mealy_machine_to_aig(): " @@ -2036,19 +2073,20 @@ namespace spot } // todo Some additional checks? return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode, - unused_ins, unused_outs); + unused_ins, unused_outs, rm); } aig_ptr mealy_machine_to_aig(mealy_like& m, const char *mode, const std::vector& ins, - const std::vector& outs) + const std::vector& outs, + const relabeling_map* rm) { if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR) throw std::runtime_error("mealy_machine_to_aig(): " "Can only handle regular mealy machine, yet."); - return mealy_machine_to_aig(m.mealy_like, mode, ins, outs); + return mealy_machine_to_aig(m.mealy_like, mode, ins, outs, rm); } aig_ptr @@ -2107,7 +2145,8 @@ namespace spot mealy_machines_to_aig(const std::vector& m_vec, const char *mode, const std::vector& ins, - const std::vector>& outs) + const std::vector>& outs, + const relabeling_map* rm) { if (m_vec.empty()) throw std::runtime_error("mealy_machines_to_aig(): No strategy given."); @@ -2164,14 +2203,15 @@ namespace spot if (!used_aps.count(ai)) unused_ins.push_back(ai); - return auts_to_aiger(new_vec, mode, unused_ins, unused_outs); + return auts_to_aiger(new_vec, mode, unused_ins, unused_outs, rm); } aig_ptr mealy_machines_to_aig(const std::vector& strat_vec, const char* mode, const std::vector& ins, - const std::vector>& outs) + const std::vector>& outs, + const relabeling_map* rm) { // todo extend to TGBA and possibly others const unsigned ns = strat_vec.size(); @@ -2205,7 +2245,7 @@ namespace spot "success identifier."); } } - return mealy_machines_to_aig(m_machines, mode, ins, outs_used); + return mealy_machines_to_aig(m_machines, mode, ins, outs_used, rm); } std::ostream & diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index bd0424e8e..77ef2d827 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -25,6 +25,7 @@ #include #include #include +#include #include #include @@ -436,20 +437,25 @@ namespace spot /// If \a ins and \a outs are specified, the named-property /// synthesis-output is ignored and all properties in \a ins and \a /// outs are guaranteed to appear in the aiger circuit. + /// + /// If \a rm is given and is not empty, it can be used to specify how + /// unused output should be encoded by mapping them to some constant. ///@{ SPOT_API aig_ptr mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode); SPOT_API aig_ptr mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode, const std::vector& ins, - const std::vector& outs); + const std::vector& outs, + const relabeling_map* rm = nullptr); SPOT_API aig_ptr mealy_machine_to_aig(const mealy_like& m, const char* mode); SPOT_API aig_ptr mealy_machine_to_aig(mealy_like& m, const char *mode, const std::vector& ins, - const std::vector& outs); + const std::vector& outs, + const relabeling_map* rm = nullptr); ///@} /// \ingroup synthesis @@ -465,6 +471,9 @@ namespace spot /// during the call to ltl_to_game() are absent. /// If \a ins and \a outs are used, all properties they list are /// guaranteed to appear in the aiger circuit. + /// + /// If \a rm is given and is not empty, it can be used to specify how + /// unused output should be encoded by mapping them to some constant. /// @{ SPOT_API aig_ptr mealy_machines_to_aig(const std::vector& m_vec, @@ -476,12 +485,14 @@ namespace spot mealy_machines_to_aig(const std::vector& m_vec, const char* mode, const std::vector& ins, - const std::vector>& outs); + const std::vector>& outs, + const relabeling_map* rm = nullptr); SPOT_API aig_ptr mealy_machines_to_aig(const std::vector& m_vec, const char* mode, const std::vector& ins, - const std::vector>& outs); + const std::vector>& outs, + const relabeling_map* rm = nullptr); /// @} /// \ingroup twa_io diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 02d248754..ae476e71d 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -227,15 +227,19 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < G(i1 <-> o0) there are 1 subformulas -trying to create strategy directly for G(Fi0 & Fi1 & Fi2) -> G(i1 <-> o0) +trying to create strategy directly for GFi1 -> G(i1 <-> o0) direct strategy might exist but was not found. translating formula done in X seconds -automaton has 2 states and 3 colors +automaton has 2 states and 1 colors LAR construction done in X seconds -DPA has 4 states, 1 colors +DPA has 2 states, 1 colors split inputs and outputs done in X seconds -automaton has 12 states +automaton has 6 states solving game with acceptance: co-Büchi game solved in X seconds EOF @@ -386,7 +390,8 @@ State: 2 [!0] 2 --END-- EOF -ltlsynt --outs=p0 -x tls-impl=0 --simpl=no -f '!XXF(p0 & (p0 M Gp0))' > out +ltlsynt --outs=p0 -x tls-impl=0 --polar=no --simpl=no \ + -f '!XXF(p0 & (p0 M Gp0))' > out diff out exp cat >exp < out +ltlsynt --outs=p0 -x tls-impl=1 --polar=no -f '!XXF(p0 & (p0 M Gp0))' > out +diff out exp +ltlsynt --outs=p0 -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out diff out exp ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out @@ -637,19 +644,19 @@ tanslating formula done in X seconds direct strategy was found. direct strat has 1 states, 2 edges and 0 colors simplification took X seconds -trying to create strategy directly for Gc +trying to create strategy directly for G(c <-> d) direct strategy was found. direct strat has 1 states, 1 edges and 0 colors simplification took X seconds EOF -ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out +ltlsynt -f '(GFa <-> GFb) && (G(c <-> d))' --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)" +# Try to find a direct strategy for (GFa <-> GFb) & G(c <-> d). The +# order should not impact the result +for f in "(GFa <-> GFb) & G(c <-> d)" "(GFb <-> GFa) & G(c <-> d)" \ + "G(c <-> d) & (GFa <-> GFb)" "G(c <-> d) & (GFb <-> GFa)" do cat >exp <exp < GFa) & G(a & c) +the following APs are polarized, they can be replaced by constants: + c := 1 +new formula: (GFb <-> GFa) & Ga +trying to create strategy directly for (GFb <-> GFa) & Ga no strategy exists. EOF ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\ @@ -747,8 +757,43 @@ game solved in X seconds simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF -ltlsynt -f '((a|x) & (b | y) & b) => (x & y)' --outs="x,y" --aiger=ite\ - --verify --verbose 2> out +ltlsynt -f '((a|x) & (b | y) & b) => (x & y)' \ + --outs="x,y" --aiger=ite --pol=no --verify --verbose 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +cat >exp < (x & y)' \ + --outs="x,y" --aiger=ite --verify --verbose 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -765,7 +810,8 @@ direct strat has 1 states, 1 edges and 0 colors simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF -ltlsynt -f 'G!(!x | !y)' --outs="x, y" --aiger=ite --verify --verbose 2> out +ltlsynt -f 'G!(!x | !y)' --outs="x, y" --pol=no --aiger=ite \ + --verify --verbose 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -775,7 +821,8 @@ there are 2 subformulas trying to create strategy directly for G!a no strategy exists. EOF -ltlsynt -f '!F(a|b)' --outs=b --decompose=yes --aiger --verbose 2> out || true +ltlsynt -f '!F(a|b)' --outs=b --pol=no --decompose=yes \ + --aiger --verbose 2> out || true sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -786,7 +833,7 @@ trying to create strategy directly for Ga no strategy exists. EOF ltlsynt -f 'G!(a -> b)' --outs=b --decompose=yes --aiger\ - --verbose 2> out || true + --pol=no --verbose 2> out || true sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -807,7 +854,7 @@ simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f '(a & b) U (b & c)' --outs=b,c --decompose=yes --aiger --verbose\ - --verify 2> out + --pol=no --verify 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -851,7 +898,7 @@ simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF ltlsynt -f 'a => (b & c & d)' --outs=b,c,d, --decompose=yes\ - --verbose --aiger 2> out + --pol=no --verbose --aiger 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -862,7 +909,7 @@ trying to create strategy directly for G!a no strategy exists. EOF ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \ - --verbose --aiger 2> out || true + --verbose --pol=no --aiger 2> out || true sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -887,7 +934,7 @@ ltlsynt --outs="$OUT" -f "$LTL" --aiger=both+ud\ --algo=lar | grep "aag 34 2 3 2 29" ltlsynt -f 'G(c) & (G(a) <-> GFb)' --outs=b,c --decompose=yes\ - --verbose --realizability 2> out + --verbose --pol=no --realizability 2> out cat >exp < GFb)' --outs=b,c --decompose=yes\ +ltlsynt -f 'G(c) & (G(a) <-> GFb)' --outs=b,c --decompose=yes --pol=no \ --verbose --realizability --bypass=no 2> out cat >exp < GFb) && (Gc)' --outs=b,c --verbose --bypass=no\ - --algo=acd 2> out + --algo=acd --pol=no 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -967,7 +1014,7 @@ solving game with acceptance: Büchi game solved in X seconds EOF ltlsynt -f "G(o1) & (GFi <-> GFo1)" --outs="o1" --verbose\ - --bypass=yes 2> out || true + --bypass=yes --pol=no 2> out || true sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp @@ -985,6 +1032,22 @@ solving game with acceptance: Streett 1 game solved in X seconds simplification took X seconds EOF +ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\ + --bypass=yes --pol=no 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +cat >exp < GFo1 +there are 1 subformulas +trying to create strategy directly for GFi <-> GFo1 +tanslating formula done in X seconds +direct strategy was found. +direct strat has 1 states, 2 edges and 0 colors +simplification took X seconds +EOF ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\ --bypass=yes 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test index 546cb0d27..f6c7787fe 100755 --- a/tests/core/ltlsynt2.test +++ b/tests/core/ltlsynt2.test @@ -61,7 +61,7 @@ G(i1 <-> Xo1),lar,1,3 F(i1 xor i2) <-> Fo1,lar,1,2 i1 <-> F(o1 xor o2),lar,1,3 Fi1 <-> Go2,lar,0,0 -o1 & F(i1 <-> o2),lar,1,4 +o1 & F(i1 <-> o2),lar,1,2 EOF diff filtered.csv expected