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

ltlsynt: add option to call to_parity_old

Browse source 
* bin/ltlsynt.cc: Add support for --algo=lar.old
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-20 14:48:23 +02:00
parent 192ca91087
commit a6da6ed95a
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -33,6 +33,9 @@ New in spot 2.8.7.dev (not yet released)
use cases are probably quite limited. We use that to generate use cases are probably quite limited. We use that to generate
benchmarks for our generic emptiness check procedure. benchmarks for our generic emptiness check procedure.
- ltlsynt --algo=lar uses the new version of to_parity() mentionned
below. The old version is available via --algo=lar.old
Library: Library:
- Historically, Spot only supports LTL with infinite semantics - Historically, Spot only supports LTL with infinite semantics

14
bin/ltlsynt.cc
View file

@ -71,13 +71,14 @@ static const argp_option options[] =
" propositions", 0}, " propositions", 0},
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "ds|sd|lar", 0, { "algo", OPT_ALGO, "ds|sd|lar|lar.old", 0,
"choose the algorithm for synthesis:\n" "choose the algorithm for synthesis:\n"
" - sd: split then determinize with Safra (default)\n" " - sd: split then determinize with Safra (default)\n"
" - ds: determinize (Safra) then split\n" " - ds: determinize (Safra) then split\n"
" - lar: translate to a deterministic automaton with arbitrary" " - lar: translate to a deterministic automaton with arbitrary"
" acceptance condition, then use LAR to turn to parity," " acceptance condition, then use LAR to turn to parity,"
" then split", 0 }, " then split\n"
" - lar.old: old version of LAR, for benchmarking.\n", 0 },
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Output options:", 20 }, { nullptr, 0, nullptr, 0, "Output options:", 20 },
{ "print-pg", OPT_PRINT, nullptr, 0, { "print-pg", OPT_PRINT, nullptr, 0,
@ -121,6 +122,7 @@ enum solver
DET_SPLIT, DET_SPLIT,
SPLIT_DET, SPLIT_DET,
LAR, LAR,
LAR_OLD,
}; };
static char const *const solver_args[] = static char const *const solver_args[] =
@ -128,6 +130,7 @@ static char const *const solver_args[] =
"detsplit", "ds", "detsplit", "ds",
"splitdet", "sd", "splitdet", "sd",
"lar", "lar",
"lar.old",
nullptr nullptr
}; };
static solver const solver_types[] = static solver const solver_types[] =
@ -135,6 +138,7 @@ static solver const solver_types[] =
DET_SPLIT, DET_SPLIT, DET_SPLIT, DET_SPLIT,
SPLIT_DET, SPLIT_DET, SPLIT_DET, SPLIT_DET,
LAR, LAR,
LAR_OLD,
}; };
ARGMATCH_VERIFY(solver_args, solver_types); ARGMATCH_VERIFY(solver_args, solver_types);
@ -349,13 +353,17 @@ namespace
break; break;
} }
case LAR: case LAR:
case LAR_OLD:
{ {
dpa = split_2step(aut, all_inputs); dpa = split_2step(aut, all_inputs);
dpa->merge_states(); dpa->merge_states();
if (verbose) if (verbose)
std::cerr << "split inputs and outputs done\nautomaton has " std::cerr << "split inputs and outputs done\nautomaton has "
<< dpa->num_states() << " states\n"; << dpa->num_states() << " states\n";
dpa = spot::to_parity(dpa); if (opt_solver == LAR)
dpa = spot::to_parity(dpa);
else
dpa = spot::to_parity_old(dpa);
spot::colorize_parity_here(dpa, true); spot::colorize_parity_here(dpa, true);
spot::change_parity_here(dpa, spot::parity_kind_max, spot::change_parity_here(dpa, spot::parity_kind_max,
spot::parity_style_odd); spot::parity_style_odd);