alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: create a "bypass" option

Browse source 
* bin/ltlsynt.cc: here.
* tests/core/ltlsynt.test: add tests
This commit is contained in:
Florian Renkin 2022-03-22 15:08:40 +01:00
parent 328cf95816
commit 7abcf4e38b
2 changed files with 58 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

23
bin/ltlsynt.cc
View file

@ -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)

38
tests/core/ltlsynt.test
View file

@ -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 <<EOF
trying to create strategy directly for (GFb <-> 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 <<EOF
trying to create strategy directly for Gc
direct strategy was found.
trying to create strategy directly for Ga <-> 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 <<EOF
translating formula done in X seconds
automaton has 1 states and 1 colors
LAR construction done in X seconds
DPA has 1 states, 0 colors
split inputs and outputs done in X seconds
automaton has 2 states
solving game with acceptance: Streett 1
game solved in X seconds
translating formula done in X seconds
automaton has 2 states and 2 colors
LAR construction done in X seconds
DPA has 2 states, 2 colors
split inputs and outputs done in X seconds
automaton has 5 states
solving game with acceptance: parity max odd 4
game solved in X seconds
EOF
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp