diff --git a/NEWS b/NEWS index 1da2a9cde..aa16106f3 100644 --- a/NEWS +++ b/NEWS @@ -16,13 +16,25 @@ 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 + - ltlsynt will now check for 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. + - ltlsynt will now check for atomic propositions that are specified + as equivalent. When this is detected, equivalent atomic + propositions are replaced by one representative of their class, to + limit the number of different APs processed by the synthesis + pipeline. The resulting game, Mealy machine, or Aiger circuit is + eventually patched to include the removed APs. This optimization + can be disabled with --global-equivalence=no. As an exception, an + equivalence between input and output signals (such as G(in<->out)) + will be ignored if ltlsynt is configured to output a game (because + patching the game a posteriori is cumbersome if the equivalence + concerns different players). + Library: - The following new trivial simplifications have been implemented for SEREs: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 59fe52494..05d190994 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -31,6 +31,7 @@ #include #include #include +#include #include #include #include @@ -52,6 +53,7 @@ enum OPT_DECOMPOSE, OPT_DOT, OPT_FROM_PGAME, + OPT_GEQUIV, OPT_HIDE, OPT_INPUT, OPT_OUTPUT, @@ -105,6 +107,9 @@ static const argp_option options[] = { "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 }, + { "global-equivalence", OPT_GEQUIV, "yes|no", 0, + "whether to remove atomic propositions that are always equivalent to " + "another one (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 " @@ -241,6 +246,7 @@ static bool decompose_values[] = ARGMATCH_VERIFY(decompose_args, decompose_values); bool opt_decompose_ltl = true; bool opt_polarity = true; +bool opt_gequiv = true; static const char* const simplify_args[] = { @@ -265,6 +271,11 @@ ARGMATCH_VERIFY(simplify_args, simplify_values); namespace { + static bool want_game() + { + return opt_print_pg || opt_print_hoa; + } + auto str_tolower = [] (std::string s) { std::transform(s.begin(), s.end(), s.begin(), @@ -272,12 +283,17 @@ namespace return s; }; + static void 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 + // Add any AP we removed. This is a game, so player moves are + // separated. Consequently at this point we cannot deal with + // removed signals such as "o1 <-> i2": if the game has to be + // printed, we can only optimize for signals such as o1 <-> o2. + if (rm && !rm->empty()) { assert(input_aps); auto& sp = spot::get_state_players(game); @@ -294,6 +310,15 @@ namespace add &= bdd_ithvar(i); else if (v.is_ff()) add &= bdd_nithvar(i); + else + { + bdd bv; + if (v.is(spot::op::ap)) + bv = bdd_ithvar(game->register_ap(v.ap_name())); + else // Not Ap + bv = bdd_nithvar(game->register_ap(v[0].ap_name())); + add &= bdd_biimp(bdd_ithvar(i), bv); + } } for (auto& e: game->edges()) if (sp[e.src]) @@ -417,53 +442,156 @@ namespace return; if (first_dap) { - *gi->verbose_stream << ("the following APs are polarized, " - "they can be replaced by constants:\n"); + *gi->verbose_stream + << "the following signals can be temporarily removed:\n"; first_dap = false; } *gi->verbose_stream << " " << p << " := " << rm[p] <<'\n'; }; spot::formula oldf; - if (opt_polarity) - do - { - bool rm_has_new_terms = false; - 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] = has_pos ? spot::formula::tt() : spot::formula::ff(); - rm_has_new_terms = true; - display_ap(pos); - } - } - 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] = has_neg ? spot::formula::tt() : spot::formula::ff(); - rm_has_new_terms = true; - display_ap(pos); - } - } - oldf = f; - if (rm_has_new_terms) - { - f = spot::relabel_apply(f, &rm); - if (gi->verbose_stream) - *gi->verbose_stream << "new formula: " << f << '\n'; - } - } - while (oldf != f); + if (opt_polarity || opt_gequiv) + { + robin_hood::unordered_set ap_inputs; + for (const std::string& ap: input_aps) + ap_inputs.insert(spot::formula::ap(ap)); + + do + { + bool rm_has_new_terms = false; + oldf = f; + + if (opt_polarity) + { + std::set lits = spot::collect_literals(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] = + has_pos ? spot::formula::tt() : spot::formula::ff(); + rm_has_new_terms = true; + display_ap(pos); + } + } + 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] = + has_neg ? spot::formula::tt() : spot::formula::ff(); + rm_has_new_terms = true; + display_ap(pos); + } + } + if (rm_has_new_terms) + { + f = spot::relabel_apply(f, &rm); + if (gi->verbose_stream) + *gi->verbose_stream << "new formula: " << f << '\n'; + rm_has_new_terms = false; + } + } + if (opt_gequiv) + { + // check for equivalent terms + spot::formula_ptr_less_than_bool_first cmp; + for (std::vector& equiv: + spot::collect_equivalent_literals(f)) + { + // For each set of equivalent literals, we want to + // pick a representative. That representative + // should be an input if one of the literal is an + // input. (If we have two inputs or more, the + // formula is not realizable.) + spot::formula repr = nullptr; + bool repr_is_input = false; + spot::formula input_seen = nullptr; + for (spot::formula lit: equiv) + { + spot::formula ap = lit; + if (ap.is(spot::op::Not)) + ap = ap[0]; + if (ap_inputs.find(ap) != ap_inputs.end()) + { + if (input_seen) + { + // ouch! we have two equivalent inputs. + // This means the formula is simply + // unrealizable. Make it false for the + // rest of the algorithm. + f = spot::formula::ff(); + goto done; + } + input_seen = lit; + // Normally, we want the input to be the + // representative. However as a special + // case, we ignore the input literal from + // the set if we are asked to print a + // game. Fixing the game to add a i<->o + // equivalence would require more code + // than I care to write. + // + // So if the set was {i,o1,o2}, instead + // of the desirable + // o1 := i + // o2 := i + // we only do + // o2 := o1 + // when printing games. + if (!want_game()) + { + repr_is_input = true; + repr = lit; + } + } + else if (!repr_is_input && (!repr || cmp(ap, repr))) + repr = lit; + } + // now map equivalent each atomic proposition to the + // representative + spot::formula not_repr = spot::formula::Not(repr); + for (spot::formula lit: equiv) + { + // input or representative are not removed + // (we have repr != input_seen either when input_seen + // is nullptr, or if want_game is true) + if (lit == repr || lit == input_seen) + continue; + if (lit.is(spot::op::Not)) + { + spot::formula ap = lit[0]; + rm[ap] = not_repr; + display_ap(ap); + } + else + { + rm[lit] = repr; + display_ap(lit); + } + rm_has_new_terms = true; + } + } + if (rm_has_new_terms) + { + f = spot::relabel_apply(f, &rm); + if (gi->verbose_stream) + *gi->verbose_stream << "new formula: " << f << '\n'; + rm_has_new_terms = false; + } + } + } + while (oldf != f); + done: + /* can't have a label followed by closing brace */; + } std::vector sub_form; std::vector> sub_outs; @@ -510,8 +638,6 @@ namespace assert((sub_form.size() == sub_outs.size()) && (sub_form.size() == sub_outs_str.size())); - const bool want_game = opt_print_pg || opt_print_hoa; - std::vector arenas; auto sub_f = sub_form.begin(); @@ -528,7 +654,7 @@ namespace }; // If we want to print a game, // we never use the direct approach - if (!want_game && opt_bypass) + if (!want_game() && opt_bypass) m_like = spot::try_create_direct_strategy(*sub_f, *sub_o, *gi, !opt_real); @@ -555,7 +681,7 @@ namespace assert((spptr->at(arena->get_init_state_number()) == false) && "Env needs first turn"); } - if (want_game) + if (want_game()) { dispatch_print_hoa(arena, &input_aps, &rm); continue; @@ -615,7 +741,7 @@ namespace } // If we only wanted to print the game we are done - if (want_game) + if (want_game()) { safe_tot_time(); return 0; @@ -681,6 +807,7 @@ namespace if (!rm.empty()) // Add any AP we removed { bdd add = bddtrue; + bdd additional_outputs = bddtrue; for (auto [k, v]: rm) { int i = tot_strat->register_ap(k); @@ -689,15 +816,39 @@ namespace != input_aps.end()) continue; if (v.is_tt()) - add &= bdd_ithvar(i); + { + bdd bv = bdd_ithvar(i); + additional_outputs &= bv; + add &= bv; + } else if (v.is_ff()) - add &= bdd_nithvar(i); + { + additional_outputs &= bdd_ithvar(i); + add &= bdd_nithvar(i); + } + else + { + bdd left = bdd_ithvar(i); // this is necessarily an output + additional_outputs &= left; + bool pos = v.is(spot::op::ap); + const std::string apname = + pos ? v.ap_name() : v[0].ap_name(); + bdd right = bdd_ithvar(tot_strat->register_ap(apname)); + // right might be an input + if (std::find(input_aps.begin(), input_aps.end(), apname) + == input_aps.end()) + additional_outputs &= right; + if (pos) + add &= bdd_biimp(left, right); + else + add &= bdd_xor(left, right); + } } for (auto& e: tot_strat->edges()) e.cond &= add; set_synthesis_outputs(tot_strat, get_synthesis_outputs(tot_strat) - & bdd_support(add)); + & additional_outputs); } printer.print(tot_strat, timer_printer_dummy); } @@ -1052,6 +1203,10 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_FROM_PGAME: jobs.emplace_back(arg, job_type::AUT_FILENAME); break; + case OPT_GEQUIV: + opt_gequiv = XARGMATCH("--global-equivalence", arg, + decompose_args, decompose_values); + break; case OPT_HIDE: show_status = false; break; diff --git a/python/spot/impl.i b/python/spot/impl.i index 2408486e6..668ccff89 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -524,6 +524,7 @@ namespace std { %template(vectorint) vector; %template(pair_formula_vectorstring) pair>; %template(atomic_prop_set) set; + %template(vectorofvectorofformulas) vector>; %template(setunsigned) set; %template(relabeling_map) map; } diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index 74790f1c4..87d5e5b3e 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -21,9 +21,13 @@ // along with this program. If not, see . #include "config.h" +#include #include #include +#include #include +#include +#include namespace spot { @@ -64,7 +68,7 @@ namespace spot return res; } - atomic_prop_set collect_litterals(formula f) + atomic_prop_set collect_literals(formula f) { atomic_prop_set res; @@ -131,4 +135,150 @@ namespace spot return res; } + std::vector> + collect_equivalent_literals(formula f) + { + std::map l2s; + // represent the implication graph as a twa_graph so we cab reuse + // scc_info. Literals can be converted to states using the l2s + // map. + twa_graph_ptr igraph = make_twa_graph(make_bdd_dict()); + + auto state_of = [&](formula a) + { + auto [it, b] = l2s.insert({a, 0}); + if (b) + it->second = igraph->new_state(); + return it->second; + }; + + auto implies = [&](formula a, formula b) + { + unsigned pos_a = state_of(a); + unsigned neg_a = state_of(formula::Not(a)); + unsigned pos_b = state_of(b); + unsigned neg_b = state_of(formula::Not(b)); + igraph->new_edge(pos_a, pos_b, bddtrue); + igraph->new_edge(neg_b, neg_a, bddtrue); + }; + + auto collect = [&](formula f, bool in_g, auto self) + { + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::eword: + case op::ap: + case op::UConcat: + case op::Not: + case op::NegClosure: + case op::NegClosureMarked: + case op::U: + case op::R: + case op::W: + case op::M: + case op::EConcat: + case op::EConcatMarked: + case op::X: + case op::F: + case op::Closure: + case op::OrRat: + 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: + return; + case op::Xor: + if (in_g && f[0].is_literal() && f[1].is_literal()) + { + implies(f[0], formula::Not(f[1])); + implies(formula::Not(f[0]), f[1]); + } + return; + case op::Equiv: + if (in_g && f[0].is_literal() && f[1].is_literal()) + { + implies(f[0], f[1]); + implies(formula::Not(f[0]), formula::Not(f[1])); + } + return; + case op::Implies: + if (in_g && f[0].is_literal() && f[1].is_literal()) + implies(f[0], f[1]); + return; + case op::G: + self(f[0], true, self); + return; + case op::Or: + if (f.size() == 2 && f[0].is_literal() && f[1].is_literal()) + implies(formula::Not(f[0]), f[1]); + return; + case op::And: + for (formula c: f) + self(c, in_g, self); + return; + } + }; + collect(f, false, collect); + + scc_info si(igraph, scc_info_options::PROCESS_UNREACHABLE_STATES); + + // print_hoa(std::cerr, igraph); + + // Build sets of equivalent literals. + unsigned nscc = si.scc_count(); + std::vector> scc(nscc); + for (auto [f, i]: l2s) + scc[si.scc_of(i)].push_back(f); + + // For each set, we will decide if we keep it or not. + std::vector keep(nscc, true); + + for (unsigned i = 0; i < nscc; ++i) + { + if (keep[i] == false) + continue; + // We don't keep trivial SCCs + if (scc[i].size() <= 1) + { + keep[i] = false; + continue; + } + // Each SCC will appear twice. Because if {a,!b,c,!d,!e} are + // equivalent literals, then so are {!a,b,!c,d,e}. We will + // keep the SCC with the fewer negation if we can. + unsigned neg_count = 0; + for (formula f: scc[i]) + { + SPOT_ASSUME(f != nullptr); + neg_count += f.is(op::Not); + } + if (neg_count > scc[i].size()/2) + { + keep[i] = false; + continue; + } + // We will keep the current SCC. Just + // mark the dual one for removal. + keep[si.scc_of(state_of(formula::Not(*scc[i].begin())))] = false; + } + // purge unwanted SCCs + unsigned j = 0; + for (unsigned i = 0; i < nscc; ++i) + { + if (keep[i] == false) + continue; + if (i > j) + scc[j] = std::move(scc[i]); + ++j; + } + scc.resize(j); + return scc; + } + } diff --git a/spot/tl/apcollect.hh b/spot/tl/apcollect.hh index 42788dc9c..7cc8ccb3c 100644 --- a/spot/tl/apcollect.hh +++ b/spot/tl/apcollect.hh @@ -24,6 +24,7 @@ #include #include +#include #include #include @@ -60,14 +61,22 @@ namespace spot atomic_prop_collect_as_bdd(formula f, const twa_ptr& a); - /// \brief Collect the litterals occuring in f + /// \brief Collect the literals 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); + atomic_prop_set collect_literals(formula f); + /// \brief Collect equivalent APs + /// + /// Looks for patterns like `...&G(...&(x->y)&...)&...` or + /// other forms of constant implications, then build a graph + /// of implications to compute equivalence classes of literals. + SPOT_API + std::vector> + collect_equivalent_literals(formula f); /// @} } diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 370a50e8f..294c8cb5b 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019, 2021, 2022 Laboratoire de Recherche et +// Copyright (C) 2015-2019, 2021, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -2071,4 +2071,11 @@ namespace spot { return print_psl(os, f); } + + bool + formula_ptr_less_than_bool_first::operator()(const formula& left, + const formula& right) const + { + return operator()(left.ptr_, right.ptr_); + } } diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 0c7377e1c..7b7a5c174 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -652,6 +652,8 @@ namespace spot SPOT_API int atomic_prop_cmp(const fnode* f, const fnode* g); + class SPOT_API formula; + struct formula_ptr_less_than_bool_first { bool @@ -718,7 +720,10 @@ namespace spot right->dump(ord); return old.str() < ord.str(); } - }; + + SPOT_API bool + operator()(const formula& left, const formula& right) const; +}; #endif // SWIG @@ -726,6 +731,7 @@ namespace spot /// \brief Main class for temporal logic formula class SPOT_API formula final { + friend struct formula_ptr_less_than_bool_first; const fnode* ptr_; public: /// \brief Create a formula from an fnode. diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index e4ba12444..455400f7d 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1986,6 +1986,21 @@ namespace for (unsigned i = 0; i < n_outs; ++i) circuit.set_output(i, bdd2var_min(out[i], out_dc[i])); // Add the unused propositions + // + // RM contains assignments like + // out1 := 1 + // out2 := 0 + // out3 := in1 + // out4 := !out3 + // but it is possible that the rhs could refer to a variable + // that is not yet defined because of the ordering. For + // this reason, the first pass will store signals it could not + // complete in the POSTPONE vector. + // + // In that vector, (u,v,b) means that output u should be mapped to + // the same formula as output v, possibly negated (if b). + std::vector> postpone; + const unsigned n_outs_all = output_names_all.size(); for (unsigned i = n_outs; i < n_outs_all; ++i) if (rm) @@ -2003,10 +2018,61 @@ namespace circuit.set_output(i, circuit.aig_false()); continue; } + else + { + formula repr = to->second; + bool neg_repr = false; + if (repr.is(op::Not)) + { + neg_repr = true; + repr = repr[0]; + } + // is repr an input? + if (auto it = std::find(input_names_all.begin(), + input_names_all.end(), + repr.ap_name()); + it != input_names_all.end()) + { + unsigned ivar = + circuit.input_var(it - input_names_all.begin(), + neg_repr); + circuit.set_output(i, ivar); + } + // is repr an output? + else if (auto it = std::find(output_names_all.begin(), + output_names_all.end(), + repr.ap_name()); + it != output_names_all.end()) + { + unsigned outnum = it - output_names_all.begin(); + unsigned outvar = circuit.output(outnum); + if (outvar == -1u) + postpone.emplace_back(i, outnum, neg_repr); + else + circuit.set_output(i, outvar + neg_repr); + } + } } } else circuit.set_output(i, circuit.aig_false()); + unsigned postponed = postpone.size(); + while (postponed) + { + unsigned postponed_again = 0; + for (auto [u, v, b]: postpone) + { + unsigned outvar = circuit.output(v); + if (outvar == -1u) + ++postponed_again; + else + circuit.set_output(u, outvar + b); + } + if (postponed_again >= postponed) + throw std::runtime_error("aiger encoding bug: " + "postponed output shunts not decreasing"); + postponed = postponed_again; + } for (unsigned i = 0; i < n_latches; ++i) circuit.set_next_latch(i, bdd2var_min(latch[i], bddfalse)); return circuit_ptr; diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 77ef2d827..9f55f3f00 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -174,6 +174,15 @@ namespace spot [](unsigned o){return o == -1u; })); return outputs_; } + + /// \brief return the variable associated to output \a num + /// + /// This will be equal to -1U if aig::set_output() hasn't been called. + unsigned output(unsigned num) const + { + return outputs_[num]; + } + /// \brief Get the set of output names const std::vector& output_names() const { diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index cd48cf18e..d6f5815f5 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -227,7 +227,7 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < G(i1 <-> o0) @@ -638,16 +638,15 @@ 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 +there are 1 subformulas trying to create strategy directly for GFa <-> GFb 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 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) && (G(c <-> d))' --outs=b,c --verbose 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx @@ -658,14 +657,15 @@ diff outx exp 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 < out + ltlsynt -f "$f" --outs=b,c --verbose --decompose=0 \ + --global-equiv=no --verify 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp done @@ -673,7 +673,7 @@ 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) & Ga trying to create strategy directly for (GFb <-> GFa) & Ga @@ -763,7 +763,7 @@ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < outx diff outx exp cat >exp < GFo1 there are 1 subformulas @@ -1038,6 +1038,36 @@ ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\ sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp + +# Test the loop around polarity/global-equiv +cat >exp < o) & G(o <-> o2) & G(!o | !o3) & GFo3 + o := i + o2 := i +new formula: GFo3 & G(!i | !o3) + i := 1 +new formula: GFo3 & G!o3 +there are 1 subformulas +trying to create strategy directly for GFo3 & G!o3 +direct strategy might exist but was not found. +translating formula done in X seconds +automaton has 1 states and 0 colors +LAR construction done in X seconds +DPA has 1 states, 0 colors +split inputs and outputs done in X seconds +automaton has 3 states +solving game with acceptance: co-Büchi +game solved in X seconds +UNREALIZABLE +EOF +ltlsynt -f 'G(o<->i) & G(o2 <-> o) & G(!o | !o3) & G(r3 -> Fo3)' \ + --ins=i,r3 --verbose 2>out 1>&2 && exit 1 +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + + # Test --dot and --hide-status ltlsynt -f 'i <-> Fo' --ins=i --aiger --dot | grep arrowhead=dot ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot | grep 'shape="diamond"'