ltlsynt: new algorithm, based on LAR
* bin/ltlsynt.cc: here * tests/core/ltlsynt.test: test it * NEWS: document it
This commit is contained in:
Maximilien Colange
parent
bd75ab5b39
commit
8d5d453efa
3 changed files with 88 additions and 45 deletions
13
NEWS
13
NEWS
|
|
@ -34,13 +34,16 @@ New in spot 2.6.0.dev (not yet released)
|
|||
- "ltlfilt --suspendable" is now a synonym for
|
||||
"ltlfilt --universal --eventual".
|
||||
|
||||
- ltlsynt now has two algorithms for synthesis:
|
||||
- ltlsynt now has three algorithms for synthesis:
|
||||
--algo=sd is the historical one. The automaton of the formula
|
||||
is split to separate inputs and outputs, then
|
||||
determinized.
|
||||
--algo=ds the automaton of the formula is determinized, then
|
||||
split to separate inputs and outputs.
|
||||
In both cases, the obtained parity game is solved using
|
||||
determinized (with Safra construction).
|
||||
--algo=ds the automaton of the formula is determinized (Safra),
|
||||
then split to separate inputs and outputs.
|
||||
--alog=lar translate the formula to a deterministic automaton
|
||||
with an arbitrary acceptance condition, then turn it
|
||||
into a parity automaton using LAR, and split it.
|
||||
In all three cases, the obtained parity game is solved using
|
||||
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
|
||||
been dropped as it was not used.
|
||||
|
||||
|
|
|
|||
116
bin/ltlsynt.cc
116
bin/ltlsynt.cc
|
|
@ -46,6 +46,7 @@
|
|||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/simulation.hh>
|
||||
#include <spot/twaalgos/split.hh>
|
||||
#include <spot/twaalgos/toparity.hh>
|
||||
|
||||
enum
|
||||
{
|
||||
|
|
@ -72,8 +73,11 @@ static const argp_option options[] =
|
|||
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
|
||||
{ "algo", OPT_ALGO, "ds|sd", 0,
|
||||
"choose the algorithm for synthesis:\n"
|
||||
" - sd: split then determinize (default)\n"
|
||||
" - ds: determinize then split", 0 },
|
||||
" - sd: split then determinize with Safra (default)\n"
|
||||
" - ds: determinize (Safra) then split\n"
|
||||
" - lar: translate to a deterministic automaton with arbitrary"
|
||||
" acceptance condition, then use LAR to turn to parity,"
|
||||
" then split", 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
|
||||
{ "print-pg", OPT_PRINT, nullptr, 0,
|
||||
|
|
@ -115,19 +119,22 @@ bool opt_print_aiger(false);
|
|||
enum solver
|
||||
{
|
||||
DET_SPLIT,
|
||||
SPLIT_DET
|
||||
SPLIT_DET,
|
||||
LAR,
|
||||
};
|
||||
|
||||
static char const *const solver_args[] =
|
||||
{
|
||||
"detsplit", "ds",
|
||||
"splitdet", "sd",
|
||||
"lar",
|
||||
nullptr
|
||||
};
|
||||
static solver const solver_types[] =
|
||||
{
|
||||
DET_SPLIT, DET_SPLIT,
|
||||
SPLIT_DET, SPLIT_DET
|
||||
SPLIT_DET, SPLIT_DET,
|
||||
LAR,
|
||||
};
|
||||
ARGMATCH_VERIFY(solver_args, solver_types);
|
||||
|
||||
|
|
@ -194,9 +201,13 @@ namespace
|
|||
spot::colorize_parity_here(dpa, true);
|
||||
spot::change_parity_here(dpa, spot::parity_kind_max,
|
||||
spot::parity_style_odd);
|
||||
bool max, odd;
|
||||
dpa->acc().is_parity(max, odd);
|
||||
assert(max && odd);
|
||||
assert((
|
||||
[&dpa]() -> bool
|
||||
{
|
||||
bool max, odd;
|
||||
dpa->acc().is_parity(max, odd);
|
||||
return max && odd;
|
||||
}()));
|
||||
assert(spot::is_deterministic(dpa));
|
||||
return dpa;
|
||||
}
|
||||
|
|
@ -271,6 +282,12 @@ namespace
|
|||
spot::process_timer timer;
|
||||
timer.start();
|
||||
|
||||
if (opt_solver == LAR)
|
||||
{
|
||||
trans_.set_type(spot::postprocessor::Generic);
|
||||
trans_.set_pref(spot::postprocessor::Deterministic);
|
||||
}
|
||||
|
||||
auto aut = trans_.run(&f);
|
||||
if (verbose)
|
||||
std::cerr << "translating formula done" << std::endl;
|
||||
|
|
@ -294,38 +311,61 @@ namespace
|
|||
}
|
||||
|
||||
spot::twa_graph_ptr dpa = nullptr;
|
||||
if (opt_solver == DET_SPLIT)
|
||||
switch (opt_solver)
|
||||
{
|
||||
auto tmp = to_dpa(aut);
|
||||
if (verbose)
|
||||
std::cerr << "determinization done\n"
|
||||
<< "dpa has " << tmp->num_states() << " states" << std::endl;
|
||||
tmp->merge_states();
|
||||
if (verbose)
|
||||
std::cerr << "simulation done\n"
|
||||
<< "dpa has " << tmp->num_states() << " states" << std::endl;
|
||||
dpa = split_2step(tmp, all_inputs);
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done\n"
|
||||
<< "automaton has " << dpa->num_states() << " states"
|
||||
<< std::endl;
|
||||
spot::colorize_parity_here(dpa, true);
|
||||
}
|
||||
else
|
||||
{
|
||||
auto split = split_2step(aut, all_inputs);
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done\n"
|
||||
<< "automaton has " << split->num_states() << " states"
|
||||
<< std::endl;
|
||||
dpa = to_dpa(split);
|
||||
if (verbose)
|
||||
std::cerr << "determinization done\n"
|
||||
<< "dpa has " << dpa->num_states() << " states" << std::endl;
|
||||
dpa->merge_states();
|
||||
if (verbose)
|
||||
std::cerr << "simulation done\n"
|
||||
<< "dpa has " << dpa->num_states() << " states" << std::endl;
|
||||
case DET_SPLIT:
|
||||
{
|
||||
auto tmp = to_dpa(aut);
|
||||
if (verbose)
|
||||
std::cerr << "determinization done\n"
|
||||
<< "dpa has " << tmp->num_states() << " states" << std::endl;
|
||||
tmp->merge_states();
|
||||
if (verbose)
|
||||
std::cerr << "simulation done\n"
|
||||
<< "dpa has " << tmp->num_states() << " states" << std::endl;
|
||||
dpa = split_2step(tmp, all_inputs);
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done\n"
|
||||
<< "automaton has " << dpa->num_states() << " states"
|
||||
<< std::endl;
|
||||
spot::colorize_parity_here(dpa, true);
|
||||
break;
|
||||
}
|
||||
case SPLIT_DET:
|
||||
{
|
||||
auto split = split_2step(aut, all_inputs);
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done\n"
|
||||
<< "automaton has " << split->num_states() << " states"
|
||||
<< std::endl;
|
||||
dpa = to_dpa(split);
|
||||
if (verbose)
|
||||
std::cerr << "determinization done\n"
|
||||
<< "dpa has " << dpa->num_states() << " states" << std::endl;
|
||||
dpa->merge_states();
|
||||
if (verbose)
|
||||
std::cerr << "simulation done\n"
|
||||
<< "dpa has " << dpa->num_states() << " states" << std::endl;
|
||||
break;
|
||||
}
|
||||
case LAR:
|
||||
{
|
||||
dpa = split_2step(aut, all_inputs);
|
||||
dpa->merge_states();
|
||||
if (verbose)
|
||||
std::cerr << "split inputs and outputs done\n"
|
||||
<< "automaton has " << dpa->num_states() << " states"
|
||||
<< std::endl;
|
||||
dpa = spot::to_parity(dpa);
|
||||
spot::cleanup_parity_here(dpa);
|
||||
spot::change_parity_here(dpa, spot::parity_kind_max,
|
||||
spot::parity_style_odd);
|
||||
if (verbose)
|
||||
std::cerr << "LAR construction done\n"
|
||||
<< "dpa has " << dpa->num_states() << " states" << std::endl;
|
||||
spot::colorize_parity_here(dpa, true);
|
||||
break;
|
||||
}
|
||||
}
|
||||
auto owner = complete_env(dpa);
|
||||
auto pg = spot::parity_game(dpa, owner);
|
||||
|
|
|
|||
|
|
@ -184,7 +184,7 @@ for i in 0 1 7 8 9; do
|
|||
OUT=$(eval echo \$OUT$i)
|
||||
EXP=$(eval echo \$EXP$i)
|
||||
|
||||
for algo in sd ds; do
|
||||
for algo in sd ds lar; do
|
||||
test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \
|
||||
--algo=$algo)
|
||||
done
|
||||
|
|
@ -199,7 +199,7 @@ for i in 2 3 4 5 6 10; do
|
|||
ltl2tgba -f "!($F)" > negf_aut$i
|
||||
|
||||
# test ltlsynt
|
||||
for algo in sd ds; do
|
||||
for algo in sd ds lar; do
|
||||
ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
|
||||
REAL=`head -1 out$i`
|
||||
test $REAL = $EXP
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue