diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index cb376806308beed19b7e317b53e18d4387521726..18c3cdcdbb7dae3514d6eba2d7b19ee1b756d70a 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -26,6 +26,9 @@ #include #include "misc/optionmap.hh" #include "priv/countstates.hh" +#include "powerset.hh" +#include "isdet.hh" +#include "tgba/tgbatba.hh" namespace spot { @@ -33,7 +36,7 @@ namespace spot postprocessor::postprocessor(const option_map* opt) : type_(TGBA), pref_(Small), level_(High), degen_reset_(true), degen_order_(false), degen_cache_(true), - simul_(-1), scc_filter_(-1), ba_simul_(-1) + simul_(-1), scc_filter_(-1), ba_simul_(-1), tba_determinisation_(false) { if (opt) { @@ -44,6 +47,7 @@ namespace spot simul_limit_ = opt->get("simul-limit", -1); scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); + tba_determinisation_ = opt->get("tba-det", 0); } } @@ -210,6 +214,50 @@ namespace spot delete a; } + // If WDBA failed attempt tba-determinization if requested. + if (tba_determinisation_ && !wdba && !is_deterministic(sim)) + { + const tgba* tmpd = 0; + if (pref_ == Deterministic + && f + && f->is_syntactic_recurrence() + && sim->number_of_acceptance_conditions() > 1) + tmpd = new tgba_tba_proxy(sim); + + // This threshold is arbitrary. For producing Small automata, + // we assume that a deterministic automaton that is twice the + // size of the original will never get reduced to a smaller + // one. For Deterministic automata, we accept automata that + // are 4 times bigger. The larger the value, the more likely + // the cycle enumeration algorithm will encounter an automaton + // that takes *eons* to explore. + const tgba* in = tmpd ? tmpd : sim; + const tgba* tmp = + tba_determinize_check(in, (pref_ == Small) ? 2 : 4, f); + if (tmp != 0 && tmp != in) + { + // There is no point in running the reverse simulation on + // a deterministic automaton, since all prefixes are + // unique. + wdba = simulation(tmp); + delete tmp; + // Degeneralize the result (which is a TBA) if requested. + if (type_ == BA) + { + const tgba* d = degeneralize(wdba); + delete wdba; + wdba = d; + } + } + delete tmpd; + if (wdba && pref_ == Deterministic) + { + // disregard the result of the simulation. + delete sim; + sim = 0; + } + } + if (wdba && sim) { if (count_states(wdba) > count_states(sim)) diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index fee1a684e826d49db0980a76a65fe459a78b30a9..4e428bb2a7518df9eaceb02b96831c13c29f5fba 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -105,6 +105,7 @@ namespace spot int simul_limit_; int scc_filter_; int ba_simul_; + bool tba_determinisation_; }; /// @} } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index bf88f1052d3cf529be1f597abe4885ecf4e0c89f..75b3804a48d14b1219fafd7e96b939635ca81089 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -81,6 +81,7 @@ TESTS = \ tgbaread.test \ renault.test \ nondet.test \ + det.test \ neverclaimread.test \ dstar.test \ readsave.test \ diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test new file mode 100755 index 0000000000000000000000000000000000000000..1a25530a8568045619f9beb7d0cdddf57fe7e3fd --- /dev/null +++ b/src/tgbatest/det.test @@ -0,0 +1,88 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2013 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +ltl2tgba=../../bin/ltl2tgba + +cat >formulas <<'EOF' +1,14,X((a M F((!c & !b) | (c & b))) W (G!c U b)) +1,5,X(((a & b) R (!a U !c)) R b) +1,10,XXG(Fa U Xb) +1,5,(!a M !b) W F!c +1,3,(b & Fa & GFc) R a +1,2,(a R (b W a)) W G(!a M (c | b)) +1,11,(Fa W b) R (Fc | !a) +1,7,X(G(!a M !b) | G(a | G!a)) +1,2,Fa W Gb +1,3,Ga | GFb +1,9,G((G!a & ((!b & X!c) | (b & Xc))) | (Fa & ((!b & Xc) | (b & X!c)))) +1,5,a M G(F!b | X!a) +1,4,G!a R XFb +1,4,XF(!a | GFb) +1,6,G(F!a U !a) U Xa +1,5,(a | G(a M !b)) W Fc +1,6,Fa W Xb +1,10,X(a R ((!b & F!c) M X!a)) +1,2,XG!a R Fb +1,4,GFc | (a & Fb) +1,6,X(a R (Fb R F!b)) +1,2,G(Xa M Fa) +1,4,X(Gb | GFa) +1,9,X(Gc | XG((b & Ga) | (!b & F!a))) +1,2,Ga R Fb +1,3,G(a U (b | X((!c & !a) | (a & c)))) +1,5,XG((G!a & F!b) | (Fa & (a | Gb))) +1,10,(a U X!a) | XG(!b & XFc) +1,4,X(G!a | GFa) +1,4,G(G!a | F!c | G!b) +EOF + +cut -d, -f3 out +diff formulas out + +cat >in.tgba <<'EOF' +acc = "1"; +"1", "2", "a", "1"; +"1", "1", "!a",; +"2", "3", "a", "1"; +"2", "1", "!a",; +"3", "3", "a",; +"3", "1", "!a",; +EOF + +cat >ex.tgba <<'EOF' +acc = "1"; +"1", "2", "a",; +"1", "1", "!a",; +"1", "-1", "!a",; +"2", "3", "a",; +"2", "1", "!a",; +"-1", "-1", "!a", "1"; +"3", "3", "a",; +"3", "-3", "a",; +"3", "1", "!a",; +"-3", "-3", "a", "1"; +"-3", "-1", "!a", "1"; +EOF + +run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba +cmp out.tgba ex.tgba