From 23323b743fd739121f092b55558858c099268446 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 May 2021 12:57:56 +0200 Subject: [PATCH] postproc: introduce dba-simul, and have simul=0 disable all *-simul * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement the dba-simul option, and disable ba-simul, dba-simul, dpa-simul, det-simul when simul=0. * bin/ltlsynt.cc: Adjust. * bin/spot-x.cc: Document dba-simul and adjust other variables. * tests/core/minusx.test: Add some test. --- NEWS | 19 ++++++++++++++++--- bin/ltlsynt.cc | 11 +++++------ bin/spot-x.cc | 15 ++++++++++----- spot/twaalgos/postproc.cc | 14 ++++++++++---- spot/twaalgos/postproc.hh | 3 ++- tests/core/minusx.test | 10 ++++++++++ 6 files changed, 53 insertions(+), 19 deletions(-) diff --git a/NEWS b/NEWS index 04d76a96e..ccb7a222f 100644 --- a/NEWS +++ b/NEWS @@ -164,8 +164,14 @@ New in spot 2.9.6.dev (not yet released) dpa-simul Set to 0/1 to disable/enable simulation-based reduction performed after running a Safra-like - determinization to optain a DPA. By default, it - is activated at all levels but --low. + determinization to optain a DPA. By default, it is + only disabled with --low or if simul=0. + + dba-simul Set to 0/1 to disable/enable simulation-based + reduction performed after running the + powerset-like construction (enabled by option + tba-det) to obtain a DBA. By default, it is + only disabled with --low or if simul=0. spot::translator additionally honor the following new variables: @@ -184,8 +190,15 @@ New in spot 2.9.6.dev (not yet released) cannot be disabled. (This feature is not new, but was not tunable before.) + - In addition the to above new variables, the default value for + ba-simul (controling how degeneralized automata are reduced) and + for det-simul (simulation-based optimization of the + determinization) is now equal to the default value of simul. This + changes allows "-x simul=0" to disable all of "ba-simul", + "dba-simul", "dpa-simul", and "det-simul" at once. + - tgba_powerset() now takes an extra optional argument to specify a - list of accepting sinks states if some are known. Doing so can + list of accepting sinks states if some arex known. Doing so can cut the size of the powerset automaton by 2^|sinks| in favorable cases. diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index a75b83790..7b332dc18 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -587,11 +587,10 @@ int main(int argc, char **argv) { return protected_main(argv, [&] { - extra_options.set("simul", 0); - extra_options.set("ba-simul", 0); - extra_options.set("det-simul", 0); - extra_options.set("tls-impl", 1); - extra_options.set("wdba-minimize", 2); + extra_options.set("simul", 0); // no simulation, except... + extra_options.set("dpa-simul", 1); // ... after determinization + extra_options.set("tls-impl", 1); // no automata-based implication check + extra_options.set("wdba-minimize", 2); // minimize only syntactic oblig const argp ap = { options, parse_opt, nullptr, argp_program_doc, children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 8b3f6ecca..56175862e 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -123,15 +123,16 @@ will be returned.")}, { DOC("det-scc", "Set to 0 to disable scc-based optimizations in \ the determinization algorithm.") }, { DOC("det-simul", "Set to 0 to disable simulation-based optimizations in \ -the determinization algorithm. (Do not confuse this with option dpa-simul, \ +the determinization algorithm. This is enabled by default, unless \"simul\" \ +is set to 0. (Do not confuse this with option \"dpa-simul\", \ which runs a simulation-based reduction after determinization.)") }, { DOC("det-stutter", "Set to 0 to disable optimizations based on \ the stutter-invariance in the determinization algorithm.") }, { DOC("dpa-simul", "Set to 1 to enable simulation-based reduction after \ running a Safra-like determinization to obtain a DPA, or 0 to disable. By \ -default is is enabled at all levels except low. (Do not confuse this with \ -option det-simul, which uses a simulation-based optimizations during \ -the determinization.)") }, +default this is disabled at low level or if parameter \"simul\" is set to 0. \ +(Do not confuse this with option det-simul, which uses a simulation-based \ +optimizations during the determinization.)") }, { DOC("gen-reduce-parity", "When the postprocessor routines are \ configured to output automata with any kind of acceptance condition, \ but they happen to process an automaton with parity acceptance, they \ @@ -160,7 +161,8 @@ only to Büchi automata for historical reasons; it really applies to any \ state-based acceptance nowadays. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ -The default is 3 in --high mode, and 0 otherwise.") }, +The default is the value of parameter \"simul\" in --high mode, and 0 \ +therwise.") }, { DOC("simul-max", "Number of states above which simulation-based \ reductions are skipped. Defaults to 4096. Set to 0 to disable. This \ applies to all simulation-based optimization, including thoses of the \ @@ -193,6 +195,9 @@ or when det-max-states is set.") }, { DOC("tba-det", "Set to 1 to attempt a powerset determinization \ if the TGBA is not already deterministic. Doing so will degeneralize \ the automaton. This is disabled by default, unless sat-minimize is set.") }, + { DOC("dba-simul", "Set to 1 to enable simulation-based reduction after \ +running the powerset determinization enabled by \"tba-det\". By default this \ +is disabled at low level or if parameter \"simul\" is set to 0.") }, { DOC("sat-minimize", "Set to a value between 1 and 4 to enable SAT-based minimization \ of deterministic ω-automata. If the input has n states, a SAT solver is \ diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 8011cf285..a44ac3d52 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -69,13 +69,14 @@ namespace spot degen_lowinit_ = opt->get("degen-lowinit", 0); degen_remscc_ = opt->get("degen-remscc", 1); det_scc_ = opt->get("det-scc", 1); - det_simul_ = opt->get("det-simul", 1); + det_simul_ = opt->get("det-simul", -1); det_stutter_ = opt->get("det-stutter", 1); det_max_states_ = opt->get("det-max-states", -1); det_max_edges_ = opt->get("det-max-edges", -1); simul_ = opt->get("simul", -1); simul_method_ = opt->get("simul-method", -1); dpa_simul_ = opt->get("dpa-simul", -1); + dba_simul_ = opt->get("dba-simul", -1); scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); tba_determinisation_ = opt->get("tba-det", 0); @@ -266,9 +267,14 @@ namespace spot if (simul_ < 0) simul_ = (level_ == Low) ? 1 : 3; if (ba_simul_ < 0) - ba_simul_ = (level_ == High) ? 3 : 0; + ba_simul_ = (level_ == High) ? simul_ : 0; + int detaut_simul_default = (level_ != Low && simul_ > 0) ? 1 : 0; if (dpa_simul_ < 0) - dpa_simul_ = (level_ != Low) ? 1 : 0; + dpa_simul_ = detaut_simul_default; + if (dba_simul_ < 0) + dba_simul_ = detaut_simul_default; + if (det_simul_ < 0) + det_simul_ = simul_ > 0; if (scc_filter_ < 0) scc_filter_ = 1; if (type_ == BA) @@ -530,7 +536,7 @@ namespace spot // There is no point in running the reverse simulation on // a deterministic automaton, since all prefixes are // unique. - dba = simulation(tmp); + dba = do_simul(tmp, dba_simul_); } if (dba && PREF_ == Deterministic) { diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index fc4ba9413..080cb831f 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -247,7 +247,7 @@ namespace spot bool degen_lowinit_ = false; bool degen_remscc_ = true; bool det_scc_ = true; - bool det_simul_ = true; + int det_simul_ = -1; bool det_stutter_ = true; int det_max_states_ = -1; int det_max_edges_ = -1; @@ -255,6 +255,7 @@ namespace spot int simul_method_ = -1; int simul_trans_pruning_ = 512; int dpa_simul_ = -1; + int dba_simul_ = -1; int scc_filter_ = -1; int ba_simul_ = -1; bool tba_determinisation_ = false; diff --git a/tests/core/minusx.test b/tests/core/minusx.test index d7be77ef1..9ed77cdad 100755 --- a/tests/core/minusx.test +++ b/tests/core/minusx.test @@ -44,3 +44,13 @@ test 6,0 = `ltl2tgba -x wdba-det-max=4 --stats=%s,%d "$f"` f=`genltl --ms-phi-s=2` test 484 -eq `ltl2tgba -P -D --stats=%s "$f"` test 484 -lt `ltl2tgba -P -D -x simul-max=512 --stats=%s "$f"` + +# Illustrate issue #455: the simulation-based reduction applied before +# tba-det can cause the creation of a DBA that is harder to reduce. +# Hopefully and improvement to the simulation-based reduction should +# reduce the third automaton in the same way as the fourth. +L=ltl2tgba +test 4,7 = `$L -xtba-det,simul=0 -D 'F(!p0 | GFp1)' --stats=%s,%e` +test 4,8 = `$L -xtba-det,simul=1,dba-simul=0 -D 'F(!p0 | GFp1)' --stats=%s,%e` +test 3,7 = `$L -xtba-det,simul=1 -D 'F(!p0 | GFp1)' --stats=%s,%e` +test 2,4 = `$L -xtba-det,simul=0,dba-simul=1 -D 'F(!p0 | GFp1)' --stats=%s,%e`