diff --git a/NEWS b/NEWS index 33a95163c..dd6e6071f 100644 --- a/NEWS +++ b/NEWS @@ -51,6 +51,11 @@ New in spot 2.7.3.dev (not yet released) - separate_sets_here() (and therefore autfilt --separate-sets) could loop infinitely on some inputs. + - In some situation, ltl2tgba -G could abort with + "direct_simulation() requires separate Inf and Fin sets". This + was fixed by teaching simulation-based reductions how to deal + with such cases. + New in spot 2.7.3 (2019-04-19) Bugs fixed: diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index afbae6420..889736fcd 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -30,7 +30,7 @@ #include #include #include -#include +#include // Simulation-based reduction, implemented using bdd-based signatures. // @@ -803,43 +803,70 @@ namespace spot std::vector* record_implications_; }; + template + twa_graph_ptr + wrap_simul(Fun f, const Aut& a) + { + if (has_separate_sets(a)) + return f(a); + // 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 + // and may exceed the number of sets we support. But it's + // better than refusing to apply simulation-based reductions to + // 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)); + } + } // End namespace anonymous. twa_graph_ptr simulation(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr simulation(const const_twa_graph_ptr& t, std::vector* implications) { - direct_simulation simul(t, implications); - return simul.run(); + return wrap_simul([implications](const const_twa_graph_ptr& t) { + direct_simulation simul(t, implications); + return simul.run(); + }, t); } twa_graph_ptr simulation_sba(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr cosimulation(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } twa_graph_ptr cosimulation_sba(const const_twa_graph_ptr& t) { - direct_simulation simul(t); - return simul.run(); + return wrap_simul([](const const_twa_graph_ptr& t) { + direct_simulation simul(t); + return simul.run(); + }, t); } @@ -876,13 +903,13 @@ namespace spot twa_graph_ptr iterated_simulations(const const_twa_graph_ptr& t) { - return iterated_simulations_(t); + return wrap_simul(iterated_simulations_, t); } twa_graph_ptr iterated_simulations_sba(const const_twa_graph_ptr& t) { - return iterated_simulations_(t); + return wrap_simul(iterated_simulations_, t); } } // End namespace spot. diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 11b022023..9c9e695bf 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -409,3 +409,16 @@ f='(a R !b) & (c R !d) & G((!b | !d) & (!a | Fb) & (!c | Fd) ' f=$f'& (!b | X(b | (a R !b))) & (!d | X(d | (c R !d))) & F(a | !b) & F(c | !d))' test '8,1' = `ltl2tgba "$f" --stats=%s,%d` test '8,1' = `ltl2tgba -GD "$f" --stats=%s,%d` + + +# Two formulas for which ltl2tgba 2.7.3 was raising an error with -GDS +# Reported by David Müller. +cat >in <out +cat >expected <