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

ltlsynt: add --algo=acd

Browse source 
* bin/ltlsynt.cc: Add "acd" to the list of possible paritization
		  algorithms used by ltlsynt
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Add
	ACD as paritisation algorithm
* tests/core/ltlsynt.test: add tests
This commit is contained in:
Florian Renkin 2022-03-21 15:58:58 +01:00
parent dd58747659
commit 8d9597d80d
4 changed files with 33 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
bin/ltlsynt.cc
View file

@ -69,7 +69,7 @@ static const argp_option options[] =
" propositions", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0,
{ "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
"choose the algorithm for synthesis:"
" \"sd\": translate to tgba, split, then determinize;"
" \"ds\": translate to tgba, determinize, then split;"
@ -77,7 +77,10 @@ static const argp_option options[] =
" \"lar\": translate to a deterministic automaton with arbitrary"
" acceptance condition, then use LAR to turn to parity,"
" then split (default);"
" \"lar.old\": old version of LAR, for benchmarking.\n", 0 },
" \"lar.old\": old version of LAR, for benchmarking;"
" \"acd\": translate to a deterministic automaton with arbitrary"
" acceptance condition, then use ACD to turn to parity,"
" then split.\n", 0 },
{ "decompose", OPT_DECOMPOSE, "yes|no", 0,
"whether to decompose the specification as multiple output-disjoint "
"problems to solve independently (enabled by default)", 0 },
@ -154,7 +157,8 @@ static char const *const algo_names[] =
"sd",
"ps",
"lar",
"lar.old"
"lar.old",
"acd",
};
static char const *const algo_args[] =
@ -164,6 +168,7 @@ static char const *const algo_args[] =
"dpasplit", "ps",
"lar",
"lar.old",
"acd",
nullptr
};
static spot::synthesis_info::algo const algo_types[] =
@ -173,6 +178,7 @@ static spot::synthesis_info::algo const algo_types[] =
spot::synthesis_info::algo::DPA_SPLIT, spot::synthesis_info::algo::DPA_SPLIT,
spot::synthesis_info::algo::LAR,
spot::synthesis_info::algo::LAR_OLD,
spot::synthesis_info::algo::ACD,
};
ARGMATCH_VERIFY(algo_args, algo_types);

14
spot/twaalgos/synthesis.cc
View file

@ -29,6 +29,7 @@
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/zlktree.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/toparity.hh>
@ -741,6 +742,9 @@ namespace spot
case (algo::LAR_OLD):
name = "lar.old";
break;
case (algo::ACD):
name = "acd";
break;
}
return os << name;
}
@ -775,6 +779,8 @@ namespace spot
translator trans(dict, &extra_options);
switch (sol)
{
case algo::ACD:
SPOT_FALLTHROUGH;
case algo::LAR:
SPOT_FALLTHROUGH;
case algo::LAR_OLD:
@ -965,6 +971,8 @@ namespace spot
alternate_players(dpa);
break;
}
case algo::ACD:
SPOT_FALLTHROUGH;
case algo::LAR:
SPOT_FALLTHROUGH;
case algo::LAR_OLD:
@ -976,11 +984,13 @@ namespace spot
dpa = to_parity(aut);
// reduce_parity is called by to_parity()
}
else
else if (gi.s == algo::LAR_OLD)
{
dpa = to_parity_old(aut);
dpa = reduce_parity_here(dpa, true);
reduce_parity_here(dpa, true);
}
else
dpa = acd_transform(aut);
if (bv)
bv->paritize_time += sw.stop();
if (vs)

1
spot/twaalgos/synthesis.hh
View file

@ -86,6 +86,7 @@ namespace spot
DPA_SPLIT,
LAR,
LAR_OLD,
ACD,
};
struct bench_var

12
tests/core/ltlsynt.test
View file

@ -836,4 +836,14 @@ ltlsynt --outs="" -f "GFb" | grep "UNREALIZABLE"
ltlsynt --outs="" -f "1"
ltlsynt --outs="" --ins="" -f "GFa" 2>&1 | \
grep "both --ins and --outs are specified"
grep "both --ins and --outs are specified"
LTL='(((((G (((((((g_0) && (G (! (r_0)))) -> (F (! (g_0)))) && (((g_0) &&
(X ((! (r_0)) && (! (g_0))))) -> (X ((r_0) R (! (g_0)))))) && (((g_1) &&
(G (! (r_1)))) -> (F (! (g_1))))) && (((g_1) && (X ((! (r_1)) && (! (g_1))))) ->
(X ((r_1) R (! (g_1)))))) && (((! (g_0)) && (true)) || ((true) && (! (g_1))))))
&& ((r_0) R (! (g_0)))) && (G ((r_0) -> (F (g_0))))) && ((r_1) R (! (g_1)))) &&
(G ((r_1) -> (F (g_1)))))'
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"