Commit 16540869 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlsynt: add --algo=ps

* bin/ltlsynt.cc: Implement this.
* tests/core/ltlsynt.test: Add a test case.
* NEWS: Mention it.
parent b434ac7f
......@@ -18,6 +18,9 @@ New in spot 2.9.0.dev (not yet released)
The default is 1 in "--high" mode, 2 in "--medium" mode or in
"--deterministic --low" mode, and 0 in other "--low" modes.
- ltlsynt learned --algo=ps to use the default conversion to
deterministic parity automata (the same as ltl2tgba -DP'max odd').
Library:
- product_xor() and product_xnor() are two new versions of the
......
......@@ -74,10 +74,11 @@ static const argp_option options[] =
" propositions", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "ds|sd|lar|lar.old", 0,
{ "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0,
"choose the algorithm for synthesis:\n"
" - sd: split then determinize with Safra (default)\n"
" - ds: determinize (Safra) then split\n"
" - sd: translate to tgba, split, then determinize (default)\n"
" - ds: translate to tgba, determinize, then split\n"
" - ps: translate to dpa, then split\n"
" - lar: translate to a deterministic automaton with arbitrary"
" acceptance condition, then use LAR to turn to parity,"
" then split\n"
......@@ -136,6 +137,7 @@ enum solver
{
DET_SPLIT,
SPLIT_DET,
DPA_SPLIT,
LAR,
LAR_OLD,
};
......@@ -144,6 +146,7 @@ static char const *const solver_names[] =
{
"ds",
"sd",
"ps",
"lar",
"lar.old"
};
......@@ -152,6 +155,7 @@ static char const *const solver_args[] =
{
"detsplit", "ds",
"splitdet", "sd",
"dpasplit", "ps",
"lar",
"lar.old",
nullptr
......@@ -160,6 +164,7 @@ static solver const solver_types[] =
{
DET_SPLIT, DET_SPLIT,
SPLIT_DET, SPLIT_DET,
DPA_SPLIT, DPA_SPLIT,
LAR,
LAR_OLD,
};
......@@ -354,10 +359,21 @@ namespace
spot::stopwatch sw;
bool want_time = verbose || opt_csv;
if (opt_solver == LAR || opt_solver == LAR_OLD)
switch (opt_solver)
{
case LAR:
case LAR_OLD:
trans_.set_type(spot::postprocessor::Generic);
trans_.set_pref(spot::postprocessor::Deterministic);
break;
case DPA_SPLIT:
trans_.set_type(spot::postprocessor::ParityMaxOdd);
trans_.set_pref(spot::postprocessor::Deterministic
| spot::postprocessor::Colored);
break;
case DET_SPLIT:
case SPLIT_DET:
break;
}
if (want_time)
......@@ -423,6 +439,29 @@ namespace
<< tmp->num_states() << " states\n";
break;
}
case DPA_SPLIT:
{
if (want_time)
sw.start();
aut->merge_states();
if (want_time)
paritize_time = sw.stop();
if (verbose)
std::cerr << "simplification done in " << paritize_time
<< " seconds\nDPA has " << aut->num_states()
<< " states\n";
if (want_time)
sw.start();
dpa = split_2step(aut, all_inputs);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
if (verbose)
std::cerr << "split inputs and outputs done in " << split_time
<< " seconds\nautomaton has "
<< dpa->num_states() << " states\n";
break;
}
case SPLIT_DET:
{
if (want_time)
......
......@@ -118,6 +118,20 @@ ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp
cat >exp <<EOF
translating formula done in X seconds
automaton has 3 states and 4 colors
simplification done in X seconds
DPA has 3 states
split inputs and outputs done in X seconds
automaton has 9 states
parity game built in X seconds
parity game solved in X seconds
EOF
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp
cat >exp <<EOF
translating formula done in X seconds
automaton has 16 states and 2 colors
......@@ -137,9 +151,10 @@ for r in '' '--real'; do
opts="$r --ins=a --outs=b -f"
ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
ltlsynt --algo=lar $opts 'FGc <-> GF(!b&XXb)' --csv='>>FILE' || :
ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || :
test 5 = `wc -l < FILE`
test 6 = `wc -l < FILE`
# Make sure all lines in FILE have the same number of comas
sed 's/[^,]//g' < FILE |
( read first
......@@ -242,7 +257,7 @@ for i in 2 3 4 5 6 10; do
ltl2tgba -f "!($F)" > negf_aut$i
# test ltlsynt
for algo in sd ds lar lar.old; do
for algo in sd ds ps lar lar.old; do
ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
REAL=`head -1 out$i`
test $REAL = $EXP
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment