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

postproc: add support for -x dpa-simul and simul-trans-pruning

Browse source 
Also have simul-max default to 4096 instead of 512, because it's
really simul-trans-pruning that is very slow and need to be limited.

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh:
Implement the above options.
* bin/spot-x.cc, NEWS: Document them.
* tests/core/ltlsynt.test, tests/core/minusx.test,
tests/core/sim3.test: Add some test cases.
This commit is contained in:
Alexandre Duret-Lutz 2021-04-29 17:24:26 +02:00
parent fca6513604
commit d32f19f5d0
11 changed files with 210 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

42
NEWS
View file

@ -129,14 +129,12 @@ New in spot 2.9.6.dev (not yet released)
- print_dot() will display states from player 1 using a diamond
shape.
- spot::postproc has two extra configuration variables that are meant
to speedup the processing of large automata.
- spot::postproc has new configuration variables that define
thresholds to disable some costly operation in order to speedup
the processing of large automata. (Those variables are typically
modified using the -x option of command-line tools, and are all
documented in the spot-x(7) man page.)
simul-max Number of states above which simulation-based
reductions are skipped. Defaults to 512. Set to 0
to disable. This also applies to the
simulation-based optimization of the
determinization algorithm.
wdba-det-max Maximum number of additional states allowed in
intermediate steps of WDBA-minimization. If the
number of additional states reached in the
@ -146,19 +144,35 @@ New in spot 2.9.6.dev (not yet released)
is ignored when -D used or when det-max-states is
set.
The reason for disabling simulation-based reduction above 512
states is that the current implementation uses one BDD variable
per state, and makes a number of BDD operations that is quadratic
in the number of states. Similarly, WDBA-mininimization is used
with --small in the off chance that it might produce a smaller
automaton, but we should not waste too much space and time trying
that.
simul-max Number of states above which simulation-based
reductions are skipped. Defaults to 4096. Set
to 0 to disable. This also applies to the
simulation-based optimization of the
determinization algorithm.
simul-trans-pruning
For simulation-based reduction, this is the
number of equivalence classes above which
transition-pruning for non-deterministic automata
is disabled. Defaults to 512. Set to 0 to
disable. This applies to all simulation-based
reduction, as well as to the simulation-based
optimization of the determinization algorithm.
Simulation-based reduction perform a number of
BDD implication checks that is quadratic in the
number of classes to implement transition pruning.
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.
spot::translator additionally honor the following new variables:
tls-max-states Maximum number of states of automata involved in
automata-based implication checks for formula
simplifications. Defaults to 64.
exprop When set, this causes the core LTL translation to
explicitly iterate over all possible valuations of
atomic propositions when considering the successors

23
bin/spot-x.cc
View file

@ -123,9 +123,15 @@ 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.") },
the determinization algorithm. (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.)") },
{ 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 \
@ -156,9 +162,18 @@ 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.") },
{ DOC("simul-max", "Number of states above which simulation-based \
reductions are skipped. Defaults to 512. Set to 0 to disable. This also \
applies to the simulation-based optimization of the determinization \
algorithm.") },
reductions are skipped. Defaults to 4096. Set to 0 to disable. This \
applies to all simulation-based optimization, including thoses of the \
determinization algorithm.") },
{ DOC("simul-trans-pruning", "Number of equivalence classes above which \
simulation-based transition-pruning for non-deterministic automata is disabled \
automata. Defaults to 512. Set to 0 to disable. This applies to all \
simulation-based reduction, as well as to the simulation-based optimization of \
the determinization algorithm. Simulation-based reduction perform a number of \
BDD implication checks that is quadratic in the number of classes to implement \
transition pruning. The equivalence classes is equal to the number \
of output states of simulation-based reduction when transition-pruning is \
disabled, it is just an upper bound otherwise.") },
{ DOC("relabel-bool", "If set to a positive integer N, a formula \
with N atomic propositions or more will have its Boolean subformulas \
abstracted as atomic propositions during the translation to automaton. \

5
spot/twaalgos/determinize.cc
View file

@ -811,7 +811,8 @@ namespace spot
tgba_determinize(const const_twa_graph_ptr& a,
bool pretty_print, bool use_scc,
bool use_simulation, bool use_stutter,
const output_aborter* aborter)
const output_aborter* aborter,
int trans_pruning)
{
if (!a->is_existential())
throw std::runtime_error
@ -829,7 +830,7 @@ namespace spot
if (use_simulation)
{
aut_tmp = spot::scc_filter(aut_tmp);
auto aut2 = simulation(aut_tmp, &implications);
auto aut2 = simulation(aut_tmp, &implications, trans_pruning);
if (pretty_print)
aut2->copy_state_names_from(aut_tmp);
aut_tmp = aut2;

7
spot/twaalgos/determinize.hh
View file

@ -77,11 +77,16 @@ namespace spot
/// \param aborter abort the construction if the constructed
/// automaton would be too large. Return nullptr
/// in this case.
///
/// \param trans_pruning when \a use_simulation is true, \a trans_pruning
/// is passed to the simulation-based reduction to limit
/// the effect of transition pruning.
SPOT_API twa_graph_ptr
tgba_determinize(const const_twa_graph_ptr& aut,
bool pretty_print = false,
bool use_scc = true,
bool use_simulation = true,
bool use_stutter = true,
const output_aborter* aborter = nullptr);
const output_aborter* aborter = nullptr,
int trans_pruning = -1);
}

34
spot/twaalgos/postproc.cc
View file

@ -75,6 +75,7 @@ namespace spot
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);
scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
tba_determinisation_ = opt->get("tba-det", 0);
@ -86,8 +87,9 @@ namespace spot
state_based_ = opt->get("state-based", 0);
wdba_minimize_ = opt->get("wdba-minimize", -1);
gen_reduce_parity_ = opt->get("gen-reduce-parity", 1);
simul_max_ = opt->get("simul-max", 512);
simul_max_ = opt->get("simul-max", 4096);
wdba_det_max_ = opt->get("wdba-det-max", 4096);
simul_trans_pruning_ = opt->get("simul-trans-pruning", 512);
if (sat_acc_ && sat_minimize_ == 0)
sat_minimize_ = 1; // Dicho.
@ -113,11 +115,10 @@ namespace spot
twa_graph_ptr
postprocessor::do_simul(const twa_graph_ptr& a, int opt) const
{
if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states())
return a;
if (opt == 0)
return a;
if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states())
return a;
static unsigned sim = [&]()
{
@ -131,18 +132,18 @@ namespace spot
if (sim == 2)
opt += 3;
// FIXME: simulation-based reduction how have work-arounds for
// FIXME: simulation-based reduction now have work-arounds for
// non-separated sets, so we can probably try them.
if (!has_separate_sets(a))
return a;
switch (opt)
{
case 1:
return simulation(a);
return simulation(a, simul_trans_pruning_);
case 2:
return cosimulation(a);
return cosimulation(a, simul_trans_pruning_);
case 3:
return iterated_simulations(a);
return iterated_simulations(a, simul_trans_pruning_);
case 4:
return reduce_direct_sim(a);
case 5:
@ -150,7 +151,7 @@ namespace spot
case 6:
return reduce_iterated(a);
default:
return iterated_simulations(a);
return iterated_simulations(a, simul_trans_pruning_);
}
}
@ -166,12 +167,12 @@ namespace spot
case 0:
return a;
case 1:
return simulation_sba(a);
return simulation_sba(a, simul_trans_pruning_);
case 2:
return cosimulation_sba(a);
return cosimulation_sba(a, simul_trans_pruning_);
case 3:
default:
return iterated_simulations_sba(a);
return iterated_simulations_sba(a, simul_trans_pruning_);
}
}
@ -266,6 +267,8 @@ namespace spot
simul_ = (level_ == Low) ? 1 : 3;
if (ba_simul_ < 0)
ba_simul_ = (level_ == High) ? 3 : 0;
if (dpa_simul_ < 0)
dpa_simul_ = (level_ != Low) ? 1 : 0;
if (scc_filter_ < 0)
scc_filter_ = 1;
if (type_ == BA)
@ -551,14 +554,13 @@ namespace spot
det_simul = false;
dba = tgba_determinize(tba,
false, det_scc_, det_simul, det_stutter_,
aborter);
aborter, simul_trans_pruning_);
// Setting det-max-states or det-max-edges may cause tgba_determinize
// to fail.
if (dba)
{
dba = simplify_acc(dba);
if (level_ != Low)
dba = simulation(dba);
dba = do_simul(simplify_acc(dba), dpa_simul_);
sim = nullptr;
}
}

6
spot/twaalgos/postproc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -253,6 +253,8 @@ namespace spot
int det_max_edges_ = -1;
int simul_ = -1;
int simul_method_ = -1;
int simul_trans_pruning_ = 512;
int dpa_simul_ = -1;
int scc_filter_ = -1;
int ba_simul_ = -1;
bool tba_determinisation_ = false;
@ -264,7 +266,7 @@ namespace spot
int gen_reduce_parity_ = 1;
bool state_based_ = false;
int wdba_minimize_ = -1;
int simul_max_ = 512;
int simul_max_ = 4096;
int wdba_det_max_ = 4096;
};
/// @}

84
spot/twaalgos/simulation.cc
View file

@ -154,10 +154,12 @@ namespace spot
}
direct_simulation(const const_twa_graph_ptr& in,
int trans_pruning,
std::vector<bdd>* implications = nullptr)
: po_size_(0),
all_class_var_(bddtrue),
original_(in),
trans_pruning_(trans_pruning),
record_implications_(implications)
{
if (!has_separate_sets(in))
@ -467,13 +469,18 @@ namespace spot
}
// Update the partial order.
//
// Do not compute implication between classes if we have more
// classes than trans_pruning_, or if the automaton is
// deterministic (in which case want_implications_ was
// initialized to false). The number of classes should only
// augment, so if we exceed trans_pruning_, it's safe to
// disable want_implications_ for good.
// This loop follows the pattern given by the paper.
// foreach class do
// | foreach class do
// | | update po if needed
// | od
// od
if (want_implications_
&& trans_pruning_ >= 0
&& static_cast<unsigned>(trans_pruning_) < sz)
want_implications_ = false;
for (unsigned n = 0; n < sz; ++n)
{
@ -773,7 +780,7 @@ namespace spot
if (!need_another_pass)
return res;
direct_simulation<Cosimulation, Sba> sim(res);
direct_simulation<Cosimulation, Sba> sim(res, trans_pruning_);
return sim.run();
}
@ -861,16 +868,16 @@ namespace spot
automaton_size stat;
const const_twa_graph_ptr original_;
int trans_pruning_;
std::vector<bdd>* record_implications_;
};
template<typename Fun, typename Aut>
twa_graph_ptr
wrap_simul(Fun f, const Aut& a)
wrap_simul(Fun f, const Aut& a, int trans_pruning)
{
if (has_separate_sets(a))
return f(a);
return f(a, trans_pruning);
// If the input has acceptance sets common to Fin and Inf,
// separate them before doing the simulation, and merge them
// back afterwards. Doing will temporarily introduce more sets
@ -879,62 +886,63 @@ namespace spot
// automata sharing Fin/Inf sets.
auto b = make_twa_graph(a, twa::prop_set::all());
separate_sets_here(b);
return simplify_acceptance_here(f(b));
return simplify_acceptance_here(f(b, trans_pruning));
}
} // End namespace anonymous.
twa_graph_ptr
simulation(const const_twa_graph_ptr& t)
simulation(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul([](const const_twa_graph_ptr& t) {
direct_simulation<false, false> simul(t);
return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) {
direct_simulation<false, false> simul(t, trans_pruning);
return simul.run();
}, t);
}, t, trans_pruning);
}
twa_graph_ptr
simulation(const const_twa_graph_ptr& t,
std::vector<bdd>* implications)
std::vector<bdd>* implications, int trans_pruning)
{
return wrap_simul([implications](const const_twa_graph_ptr& t) {
direct_simulation<false, false> simul(t, implications);
return wrap_simul([implications](const const_twa_graph_ptr& t,
int trans_pruning) {
direct_simulation<false, false> simul(t, trans_pruning, implications);
return simul.run();
}, t);
}, t, trans_pruning);
}
twa_graph_ptr
simulation_sba(const const_twa_graph_ptr& t)
simulation_sba(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul([](const const_twa_graph_ptr& t) {
direct_simulation<false, true> simul(t);
return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) {
direct_simulation<false, true> simul(t, trans_pruning);
return simul.run();
}, t);
}, t, trans_pruning);
}
twa_graph_ptr
cosimulation(const const_twa_graph_ptr& t)
cosimulation(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul([](const const_twa_graph_ptr& t) {
direct_simulation<true, false> simul(t);
return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) {
direct_simulation<true, false> simul(t, trans_pruning);
return simul.run();
}, t);
}, t, trans_pruning);
}
twa_graph_ptr
cosimulation_sba(const const_twa_graph_ptr& t)
cosimulation_sba(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul([](const const_twa_graph_ptr& t) {
direct_simulation<true, true> simul(t);
return wrap_simul([](const const_twa_graph_ptr& t, int trans_pruning) {
direct_simulation<true, true> simul(t, trans_pruning);
return simul.run();
}, t);
}, t, trans_pruning);
}
template<bool Sba>
twa_graph_ptr
iterated_simulations_(const const_twa_graph_ptr& t)
iterated_simulations_(const const_twa_graph_ptr& t, int trans_pruning)
{
twa_graph_ptr res = nullptr;
automaton_size prev;
@ -943,12 +951,12 @@ namespace spot
do
{
prev = next;
direct_simulation<false, Sba> simul(res ? res : t);
direct_simulation<false, Sba> simul(res ? res : t, trans_pruning);
res = simul.run();
if (res->prop_universal())
break;
direct_simulation<true, Sba> cosimul(res);
direct_simulation<true, Sba> cosimul(res, trans_pruning);
res = cosimul.run();
if (Sba)
@ -963,15 +971,15 @@ namespace spot
}
twa_graph_ptr
iterated_simulations(const const_twa_graph_ptr& t)
iterated_simulations(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul(iterated_simulations_<false>, t);
return wrap_simul(iterated_simulations_<false>, t, trans_pruning);
}
twa_graph_ptr
iterated_simulations_sba(const const_twa_graph_ptr& t)
iterated_simulations_sba(const const_twa_graph_ptr& t, int trans_pruning)
{
return wrap_simul(iterated_simulations_<true>, t);
return wrap_simul(iterated_simulations_<true>, t, trans_pruning);
}
template <bool Cosimulation, bool Sba>

55
spot/twaalgos/simulation.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2015, 2017, 2019 Laboratoire de Recherche et
// Copyright (C) 2012-2015, 2017, 2019, 2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -36,7 +36,8 @@ namespace spot
/// described in \cite babiak.13.spin .
///
/// Our reconstruction of the quotient automaton based on this
/// suffix-inclusion relation will also improve determinism.
/// suffix-inclusion relation will also improve determinism thanks
/// to a kind of transition-pruning.
///
/// We recommend to call scc_filter() to first simplify the
/// automaton that should be reduced by simulation.
@ -47,22 +48,33 @@ namespace spot
/// acceptance conditions than necessary, and running scc_filter()
/// again afterwards will remove these superfluous conditions.
///
/// The resulting automaton has a named property "simulated-states", that is a
/// vector mapping each state of the input to a state of the output. Note that
/// some input states may be mapped to -1, as a by-product of improved
/// determinism. Typically, if the language of q1 is included in the language
/// of q2, only a transition to q2 will be built.
///
/// The resulting automaton has a named property "simulated-states",
/// that is a vector mapping each state of the input to a state of
/// the output. Note that some input states may be mapped to -1, as
/// a by-product of transition prunning.
///
/// \param automaton the automaton to simulate.
///
/// \param trans_pruning Transition pruning requires a quadratic
/// number of BDD implication checks between all equivalence
/// classes, so it can be costly on large automata. If \a
/// trans_pruning is set to a non-negative integer, only
/// (non-deterministic) automata with more states than trans_pruning
/// will be simplified.
///
/// \return a new automaton which is at worst a copy of the received
/// one
SPOT_API twa_graph_ptr
simulation(const const_twa_graph_ptr& automaton);
simulation(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
SPOT_API twa_graph_ptr
simulation(const const_twa_graph_ptr& automaton,
std::vector<bdd>* implications);
std::vector<bdd>* implications,
int trans_pruning = -1);
SPOT_API twa_graph_ptr
simulation_sba(const const_twa_graph_ptr& automaton);
simulation_sba(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
/// @}
/// @{
@ -73,7 +85,8 @@ namespace spot
/// state can be merged into the latter. \cite babiak.13.spin .
///
/// Our reconstruction of the quotient automaton based on this
/// prefix-inclusion relation will also improve codeterminism.
/// prefix-inclusion relation will also improve codeterminism
/// thanks to a kind of transition pruning.
///
/// We recommend to call scc_filter() to first simplify the
/// automaton that should be reduced by cosimulation.
@ -93,12 +106,22 @@ namespace spot
/// codeterminism.)
///
/// \param automaton the automaton to simulate.
///
/// \param trans_pruning Transition pruning requires a quadratic
/// number of BDD implication checks between all equivalence
/// classes, so it can be costly on large automata. If \a
/// trans_pruning is set to a non-negative integer, only
/// (non-deterministic) automata with more states than trans_pruning
/// will be simplified.
///
/// \return a new automaton which is at worst a copy of the received
/// one
SPOT_API twa_graph_ptr
cosimulation(const const_twa_graph_ptr& automaton);
cosimulation(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
SPOT_API twa_graph_ptr
cosimulation_sba(const const_twa_graph_ptr& automaton);
cosimulation_sba(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
/// @}
/// @{
@ -117,9 +140,11 @@ namespace spot
/// \return a new automaton which is at worst a copy of the received
/// one
SPOT_API twa_graph_ptr
iterated_simulations(const const_twa_graph_ptr& automaton);
iterated_simulations(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
SPOT_API twa_graph_ptr
iterated_simulations_sba(const const_twa_graph_ptr& automaton);
iterated_simulations_sba(const const_twa_graph_ptr& automaton,
int trans_pruning = -1);
/// @}
/// @{

2
tests/core/ltlsynt.test
View file

@ -377,5 +377,7 @@ diff out exp
f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))'
ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
grep 'DPA has 13 states' err
ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
grep 'DPA has 30 states' err
ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
grep 'DPA has 12 states' err

7
tests/core/minusx.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016, 2020 Laboratoire de Recherche et Développement de
# Copyright (C) 2016, 2020, 2021 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -39,3 +39,8 @@ grep "autfilt: option 'other' was not used" error
f='G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4)))) | G!p1)'
test 4,1 = `ltl2tgba --stats=%s,%d "$f"`
test 6,0 = `ltl2tgba -x wdba-det-max=4 --stats=%s,%d "$f"`
# Make sure simul-max has an effect
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"`

32
tests/core/sim3.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2018, 2019, 2020 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2018-2021 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -150,3 +150,33 @@ State: 6
EOF
autfilt --small --low input > output
diff expect output
cat >input <<EOF
HOA: v1
States: 4
Start: 0
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 0 t
--BODY--
State: 0
[0] 1
[0&1] 2
[2] 3
State: 1
[0] 1
State: 2
[0&1] 2
State: 3
[0] 3
--END--
EOF
cmd="autfilt --small input --stats=%s,%t"
test 2,5 = `$cmd -x simul=0`
test 2,5 = `$cmd -x wdba-minimize=0`
test 4,20 = `$cmd -x simul=0,wdba-minimize=0`
test 3,14 = `$cmd -x simul-trans-pruning=0,wdba-minimize=0`
test 3,14 = `$cmd -x simul-trans-pruning=2,wdba-minimize=0`
# Three "equivalence classes" are needed even if the output has two states.
test 2,5 = `$cmd -x simul-trans-pruning=3,wdba-minimize=0`