postproc: Add the new simulation in do_simul()

* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add the new simulation
  in do_simul().
* bin/man/spot-x.x, bin/spot-x.cc: Add documentation for
  SPOT_SIMULATION_REDUCTION environnement variable and the simul-method
  fine tunning option.
* NEWS: Mention the changes.
This commit is contained in:
Jerome Dubois 2021-02-19 17:09:22 +01:00 committed by Alexandre Duret-Lutz
parent fb066ada0a
commit b082df201f
5 changed files with 44 additions and 3 deletions

View file

@ -74,6 +74,7 @@ namespace spot
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);
scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
tba_determinisation_ = opt->get("tba-det", 0);
@ -115,19 +116,39 @@ namespace spot
if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states())
return a;
if (opt == 0)
return a;
static unsigned sim = [&]()
{
if (simul_method_ != -1)
return simul_method_;
char* s = getenv("SPOT_SIMULATION_REDUCTION");
return s ? *s - '0' : 0;
}();
if (sim == 2)
opt += 3;
// FIXME: simulation-based reduction how have work-arounds for
// non-separated sets, so we can probably try them.
if (!has_separate_sets(a))
return a;
switch (opt)
{
case 0:
return a;
case 1:
return simulation(a);
case 2:
return cosimulation(a);
case 3:
return iterated_simulations(a);
case 4:
return reduce_direct_sim(a);
case 5:
return reduce_direct_cosim(a);
case 6:
return reduce_iterated(a);
default:
return iterated_simulations(a);
}

View file

@ -252,6 +252,7 @@ namespace spot
int det_max_states_ = -1;
int det_max_edges_ = -1;
int simul_ = -1;
int simul_method_ = -1;
int scc_filter_ = -1;
int ba_simul_ = -1;
bool tba_determinisation_ = false;