diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 3d9f46900..0e5d765a1 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -44,6 +44,7 @@ enum { OPT_ALGO = 256, + OPT_BYPASS, OPT_CSV, OPT_DECOMPOSE, OPT_INPUT, @@ -81,6 +82,9 @@ static const argp_option options[] = " \"acd\": translate to a deterministic automaton with arbitrary" " acceptance condition, then use ACD to turn to parity," " then split.\n", 0 }, + { "bypass", OPT_BYPASS, "yes|no", 0, + "whether to try to avoid to construct a parity game " + "(enabled by default)", 0}, { "decompose", OPT_DECOMPOSE, "yes|no", 0, "whether to decompose the specification as multiple output-disjoint " "problems to solve independently (enabled by default)", 0 }, @@ -182,6 +186,20 @@ static spot::synthesis_info::algo const algo_types[] = }; ARGMATCH_VERIFY(algo_args, algo_types); +static const char* const bypass_args[] = + { + "yes", "true", "enabled", "1", + "no", "false", "disabled", "0", + nullptr + }; +static bool bypass_values[] = + { + true, true, true, true, + false, false, false, false, + }; +ARGMATCH_VERIFY(bypass_args, bypass_values); +bool opt_bypass = true; + static const char* const decompose_args[] = { "yes", "true", "enabled", "1", @@ -374,7 +392,7 @@ namespace }; // If we want to print a game, // we never use the direct approach - if (!want_game) + if (!want_game && opt_bypass) m_like = spot::try_create_direct_strategy(*sub_f, *sub_o, *gi, !opt_real); @@ -638,6 +656,9 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_ALGO: gi->s = XARGMATCH("--algo", arg, algo_args, algo_types); break; + case OPT_BYPASS: + opt_bypass = XARGMATCH("--bypass", arg, bypass_args, bypass_values); + break; case OPT_CSV: opt_csv = arg ? arg : "-"; if (not gi->bv) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index f0cda98af..60b96bb46 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -566,7 +566,7 @@ 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 +# 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)" @@ -594,7 +594,7 @@ ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\ 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 +# # ltlsynt should be able to create a strategy when the last G # is input-complete. cat >exp < GFa) & G((a & c) | (!a & !c)) @@ -796,3 +796,37 @@ LTL='(((((G (((((((g_0) && (G (! (r_0)))) -> (F (! (g_0)))) && (((g_0) && OUT='g_0, g_1' ltlsynt --outs="$OUT" -f "$LTL" --aiger=both --algo=acd | grep "aag 8 2 2 2 4" ltlsynt --outs="$OUT" -f "$LTL" --aiger=both --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 +cat >exp < GFb +direct strategy was found. +EOF +diff out exp + +ltlsynt -f 'G(c) & (G(a) <-> GFb)' --outs=b,c --decompose=yes\ + --verbose --realizability --bypass=no 2> out +cat >exp < outx +diff outx exp