diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index d2957855f..2062b6340 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -104,12 +104,14 @@ 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, + { "polarity", OPT_POLARITY, "yes|no|before-decompose", 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, + "polarity in the formula to speed things up (enabled by default, " + "both before and after decomposition)", 0 }, + { "global-equivalence", OPT_GEQUIV, "yes|no|before-decompose", 0, "whether to remove atomic propositions that are always equivalent to " - "another one (enabled by default)", 0 }, + "another one (enabled by default, both before and after decomposition)", + 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 " @@ -252,9 +254,25 @@ static bool decompose_values[] = false, false, false, false, }; ARGMATCH_VERIFY(decompose_args, decompose_values); +static const char* const polarity_args[] = + { + "yes", "true", "enabled", "1", + "no", "false", "disabled", "0", + "before-decompose", + nullptr + }; +enum polarity_choice { pol_no, pol_yes, pol_before_decompose }; +static polarity_choice polarity_values[] = + { + pol_yes, pol_yes, pol_yes, pol_yes, + pol_no, pol_no, pol_no, pol_no, + pol_before_decompose + }; +ARGMATCH_VERIFY(polarity_args, polarity_values); + bool opt_decompose_ltl = true; -bool opt_polarity = true; -bool opt_gequiv = true; +polarity_choice opt_polarity = pol_yes; +polarity_choice opt_gequiv = pol_yes; static const char* const simplify_args[] = { @@ -407,12 +425,12 @@ namespace // Attempt to remove superfluous atomic propositions spot::realizability_simplifier* rs = nullptr; - if (opt_polarity || opt_gequiv) + if (opt_polarity != pol_no || opt_gequiv != pol_no) { unsigned opt = 0; - if (opt_polarity) + if (opt_polarity != pol_no) opt |= spot::realizability_simplifier::polarity; - if (opt_gequiv) + if (opt_gequiv != pol_no) { if (want_game()) opt |= spot::realizability_simplifier::global_equiv_output_only; @@ -420,9 +438,7 @@ namespace opt |= spot::realizability_simplifier::global_equiv; } rs = - new spot::realizability_simplifier(original_f, - input_aps, - opt, + new spot::realizability_simplifier(original_f, input_aps, opt, gi ? gi->verbose_stream : nullptr); f = rs->simplified_formula(); } @@ -493,6 +509,7 @@ namespace auto sub_f = sub_form.begin(); auto sub_o = sub_outs_str.begin(); std::vector mealy_machines; + unsigned numsubs = sub_form.size(); for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { @@ -502,6 +519,28 @@ namespace nullptr, bddfalse }; + + if (numsubs > 1 && (opt_polarity == pol_yes || opt_gequiv == pol_yes)) + { + unsigned opt = 0; + if (opt_polarity == pol_yes) + opt |= spot::realizability_simplifier::polarity; + if (opt_gequiv == pol_yes) + { + if (want_game()) + opt |= spot::realizability_simplifier::global_equiv_output_only; + else + opt |= spot::realizability_simplifier::global_equiv; + } + if (gi->verbose_stream) + *gi->verbose_stream << "working on subformula " << *sub_f << '\n'; + spot::realizability_simplifier rsub(*sub_f, input_aps, opt, + gi ? + gi->verbose_stream : nullptr); + *sub_f = rsub.simplified_formula(); + rs->merge_mapping(rsub); + } + // If we want to print a game, // we never use the direct approach if (!want_game() && opt_bypass) @@ -1049,7 +1088,7 @@ parse_opt(int key, char *arg, struct argp_state *) break; case OPT_GEQUIV: opt_gequiv = XARGMATCH("--global-equivalence", arg, - decompose_args, decompose_values); + polarity_args, polarity_values); break; case OPT_HIDE: show_status = false; @@ -1068,7 +1107,7 @@ parse_opt(int key, char *arg, struct argp_state *) } case OPT_POLARITY: opt_polarity = XARGMATCH("--polarity", arg, - decompose_args, decompose_values); + polarity_args, polarity_values); break; case OPT_PRINT: opt_print_pg = true; diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index 72e4335f9..504f624ae 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -429,6 +429,13 @@ namespace spot while (oldf != f_); } + void + realizability_simplifier::merge_mapping(const realizability_simplifier& other) + { + for (auto [from, from_is_input, to]: other.get_mapping()) + mapping_.emplace_back(from, from_is_input, to); + } + void realizability_simplifier::patch_mealy(twa_graph_ptr mealy) const { bdd add = bddtrue; diff --git a/spot/tl/apcollect.hh b/spot/tl/apcollect.hh index a4ccfdaa6..d35461035 100644 --- a/spot/tl/apcollect.hh +++ b/spot/tl/apcollect.hh @@ -107,6 +107,10 @@ namespace spot return mapping_; } + /// \brief Augment the current mapping with output variable renaming from + /// another realizability_simplifier. + void merge_mapping(const realizability_simplifier& other); + /// \brief Patch a Mealy machine to add the missing APs. void patch_mealy(twa_graph_ptr mealy) const; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 28b846abd..cbc49b1c9 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -732,6 +732,7 @@ diff outx exp cat >exp < y trying to create strategy directly for (b & (b | y)) -> y direct strategy might exist but was not found. translating formula done in X seconds @@ -743,6 +744,7 @@ automaton has 4 states solving game with acceptance: all game solved in X seconds simplification took X seconds +working on subformula (a | x) -> x trying to create strategy directly for (a | x) -> x direct strategy might exist but was not found. translating formula done in X seconds @@ -784,10 +786,12 @@ diff outx exp # Here, G!(!x | !y) should be Gx & Gy cat >exp <exp < b) should be G(a) & G(!b) cat >exp < b) & (a => c) & (a => d) cat >exp < b trying to create strategy directly for a -> b direct strategy might exist but was not found. translating formula done in X seconds @@ -857,6 +864,7 @@ automaton has 4 states solving game with acceptance: all game solved in X seconds simplification took X seconds +working on subformula a -> c trying to create strategy directly for a -> c direct strategy might exist but was not found. translating formula done in X seconds @@ -868,6 +876,7 @@ automaton has 4 states solving game with acceptance: all game solved in X seconds simplification took X seconds +working on subformula a -> d trying to create strategy directly for a -> d direct strategy might exist but was not found. translating formula done in X seconds @@ -889,6 +898,7 @@ diff outx exp # Here, !(F(a | b)) should be G!a & G!b cat >exp < GFb)' --outs=b,c --decompose=yes\ --verbose --pol=no --realizability 2> out cat >exp < GFb trying to create strategy directly for Ga <-> GFb direct strategy was found. EOF @@ -932,6 +944,7 @@ ltlsynt -f 'G(c) & (G(a) <-> GFb)' --outs=b,c --decompose=yes --pol=no \ --verbose --realizability --bypass=no 2> out cat >exp < GFb translating formula done in X seconds automaton has 2 states and 2 colors LAR construction done in X seconds @@ -956,6 +970,7 @@ diff outx exp # ACD verbose cat >exp < GFb translating formula done in X seconds automaton has 1 states and 2 colors ACD construction done in X seconds @@ -965,6 +980,7 @@ automaton has 6 states solving game with acceptance: generalized-Streett 1 1 game solved in X seconds simplification took X seconds +working on subformula Gc translating formula done in X seconds automaton has 1 states and 0 colors ACD construction done in X seconds @@ -1147,3 +1163,140 @@ grep 'controlenv.*matches both' err ltlsynt --polarity=1 --global-e=1 -f 'G(i -> Xo) & G(!i -> F!o)' --real ltlsynt --polarity=0 --global-e=0 -f 'G(i -> Xo) & G(!i -> F!o)' --real + +cat >exp < (o1 | !o2)) & G(i2 -> X(!o1 | o2)) +the following signals can be temporarily removed: + i1 := 1 + i2 := 1 +new formula: G(o1 | !o2) & GX(!o1 | o2) +trying to create strategy directly for G(o1 | !o2) & GX(!o1 | o2) +direct strategy might exist but was not found. +translating formula done in X seconds +automaton has 2 states and 0 colors +LAR construction done in X seconds +DPA has 2 states, 0 colors +split inputs and outputs done in X seconds +automaton has 4 states +solving game with acceptance: all +game solved in X seconds +simplification took X seconds +working on subformula G(!i1 -> (o3 | !o4)) & G(!i2 -> X(!o3 | o4)) +the following signals can be temporarily removed: + i1 := 0 + i2 := 0 +new formula: G(o3 | !o4) & GX(!o3 | o4) +trying to create strategy directly for G(o3 | !o4) & GX(!o3 | o4) +direct strategy might exist but was not found. +translating formula done in X seconds +automaton has 2 states and 0 colors +LAR construction done in X seconds +DPA has 2 states, 0 colors +split inputs and outputs done in X seconds +automaton has 4 states +solving game with acceptance: all +game solved in X seconds +simplification took X seconds +REALIZABLE +HOA: v1 +States: 1 +Start: 0 +AP: 6 "o1" "o2" "o3" "o4" "i1" "i2" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 0 1 2 3 +--BODY-- +State: 0 +[!0&!1&!2&!3 | !0&!1&2&3 | 0&1&!2&!3 | 0&1&2&3] 0 +--END-- +EOF +f1='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->X(!o1|o2)) & G(!i2->X(!o3|o4))' +ltlsynt -f "$f1" --verbose 2>out 1>&2 +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +gg='G(i2 -> (!o1 | o2)) & G(!i2 -> (!o3 | o4))' +cat >exp < (o1 | !o2)) & G(!i1 -> (o3 | !o4)) & $gg +there are 2 subformulas +working on subformula G(i1 -> (o1 | !o2)) & G(i2 -> (!o1 | o2)) +the following signals can be temporarily removed: + i1 := 1 + i2 := 1 +new formula: G(o1 | !o2) & G(!o1 | o2) + o2 := o1 +new formula: G(o1 | !o1) +trying to create strategy directly for G(o1 | !o1) +direct strategy was found. +direct strat has 1 states, 1 edges and 0 colors +simplification took X seconds +working on subformula G(!i1 -> (o3 | !o4)) & G(!i2 -> (!o3 | o4)) +the following signals can be temporarily removed: + i1 := 0 + i2 := 0 +new formula: G(o3 | !o4) & G(!o3 | o4) + o4 := o3 +new formula: G(o3 | !o3) +trying to create strategy directly for G(o3 | !o3) +direct strategy was found. +direct strat has 1 states, 1 edges and 0 colors +simplification took X seconds +REALIZABLE +HOA: v1 +States: 1 +Start: 0 +AP: 7 "o1" "o2" "o3" "o4" "o5" "i1" "i2" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +controllable-AP: 0 1 2 3 4 +--BODY-- +State: 0 +[!0&!1&!2&!3&4 | !0&!1&2&3&4 | 0&1&!2&!3&4 | 0&1&2&3&4] 0 +--END-- +EOF +f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5' +ltlsynt -f "$f2" --verbose 2>out 1>&2 +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + +gg='G(i2->(!o1 | o2)) & G(!i2->(!o3 | o4))' +hh='0&1&3&!5&6 | 0&!3&!4&!5&6 | !1&2&!3&5&6 | !1&!3&!4&!5&6 | ' +ii='1&!2&3&!5&6 | 1&!2&4&5&6 | !2&!3&!4&!5&6 | !2&!3&4&5&6' +cat >exp <(o1 | !o2)) & G(!i1->(o3 | !o4)) & $gg +there are 2 subformulas +working on subformula G(i1->(o1 | !o2)) & G(i2->(!o1 | o2)) +trying to create strategy directly for G(i1->(o1 | !o2)) & G(i2->(!o1 | o2)) +direct strategy was found. +direct strat has 1 states, 1 edges and 0 colors +simplification took X seconds +working on subformula G(!i1->(o3 | !o4)) & G(!i2->(!o3 | o4)) +trying to create strategy directly for G(!i1->(o3 | !o4)) & G(!i2->(!o3 | o4)) +direct strategy was found. +direct strat has 1 states, 1 edges and 0 colors +simplification took X seconds +REALIZABLE +HOA: v1 +States: 1 +Start: 0 +AP: 7 "o1" "o2" "i1" "i2" "o3" "o4" "o5" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +controllable-AP: 0 1 4 5 6 +--BODY-- +State: 0 +[!0&!1&2&5&6 | !0&!1&3&!5&6 | !0&!2&4&5&6 | 0&1&2&5&6 | $hh$ii] 0 +--END-- +EOF +f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5' +ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2 +sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx +diff outx exp