From 98de84f3de5544b81c9116446c1731d4c4d6a712 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Mar 2013 11:53:42 +0100 Subject: [PATCH] Add an is_unambiguous() function, use it in ltlcross and autfilt * src/twaalgos/isunamb.hh, src/twaalgos/isunamb.cc: New files. * src/twaalgos/Makefile.am: Add them. * src/tests/unambig.test: New file. * src/tests/Makefile.am: Add it. * src/bin/ltlcross.cc: Record whether each produced automaton is ambiguous. * src/bin/autfilt.cc: Add a --is-unambiguous option. * NEWS: Mention it. --- NEWS | 2 +- src/bin/autfilt.cc | 12 ++++++ src/bin/ltlcross.cc | 11 ++++-- src/tests/Makefile.am | 1 + src/tests/unambig.test | 84 ++++++++++++++++++++++++++++++++++++++++ src/twaalgos/Makefile.am | 2 + src/twaalgos/isunamb.cc | 40 +++++++++++++++++++ src/twaalgos/isunamb.hh | 44 +++++++++++++++++++++ 8 files changed, 192 insertions(+), 4 deletions(-) create mode 100755 src/tests/unambig.test create mode 100644 src/twaalgos/isunamb.cc create mode 100644 src/twaalgos/isunamb.hh diff --git a/NEWS b/NEWS index 23e73a6d2..298cecb14 100644 --- a/NEWS +++ b/NEWS @@ -225,7 +225,7 @@ New in spot 1.99b (not yet released) new options to produce unambiguous TGBA, i.e., TGBAs in which every word is accepted by at most one path. The ltl2tgba command line has a new option, --unambigous (or -U) to produce - these automata. + these automata, and autfilt has a --is-unambiguous filter. * Noteworthy code changes diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 0b16eeffc..33a3065a4 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -39,6 +39,7 @@ #include "twaalgos/product.hh" #include "twaalgos/isdet.hh" #include "twaalgos/stutter.hh" +#include "twaalgos/isunamb.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" #include "misc/random.hh" @@ -80,6 +81,7 @@ enum { OPT_IS_COMPLETE, OPT_IS_DETERMINISTIC, OPT_IS_EMPTY, + OPT_IS_UNAMBIGUOUS, OPT_KEEP_STATES, OPT_MASK_ACC, OPT_MERGE, @@ -179,6 +181,8 @@ static const argp_option options[] = "keep deterministic automata", 0 }, { "is-empty", OPT_IS_EMPTY, 0, 0, "keep automata with an empty language", 0 }, + { "is-unambiguous", OPT_IS_UNAMBIGUOUS, 0, 0, + "keep only unambiguous automata", 0 }, { "intersect", OPT_INTERSECT, "FILENAME", 0, "keep automata whose languages have an non-empty intersection with" " the automaton from FILENAME", 0 }, @@ -234,6 +238,7 @@ static struct opt_t static bool opt_merge = false; static bool opt_is_complete = false; static bool opt_is_deterministic = false; +static bool opt_is_unambiguous = false; static bool opt_invert = false; static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; @@ -344,6 +349,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_IS_EMPTY: opt_is_empty = true; break; + case OPT_IS_UNAMBIGUOUS: + opt_is_unambiguous = true; + break; case OPT_MERGE: opt_merge = true; break; @@ -522,6 +530,10 @@ namespace matched &= is_complete(aut); if (opt_is_deterministic) matched &= is_deterministic(aut); + if (opt_is_deterministic) + matched &= is_deterministic(aut); + else if (opt_is_unambiguous) + matched &= is_unambiguous(aut); if (opt->are_isomorphic) matched &= opt->isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index cfa584fd3..fb3ee6047 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -59,6 +59,7 @@ #include "misc/formater.hh" #include "twaalgos/stats.hh" #include "twaalgos/isdet.hh" +#include "twaalgos/isunamb.hh" #include "misc/escape.hh" #include "misc/hash.hh" #include "misc/random.hh" @@ -293,6 +294,7 @@ struct statistics std::vector product_states; std::vector product_transitions; std::vector product_scc; + bool ambiguous; static void fields(std::ostream& os, bool show_exit, bool show_sr) @@ -316,7 +318,8 @@ struct statistics "\"nondet_aut\"," "\"terminal_aut\"," "\"weak_aut\"," - "\"strong_aut\""); + "\"strong_aut\"," + "\"ambiguous_aut\""); size_t m = products_avg ? 1U : products; for (size_t i = 0; i < m; ++i) os << ",\"product_states\",\"product_transitions\",\"product_scc\""; @@ -353,7 +356,8 @@ struct statistics << nondeterministic << ',' << terminal_aut << ',' << weak_aut << ',' - << strong_aut; + << strong_aut << ',' + << ambiguous; if (!products_avg) { for (size_t i = 0; i < products; ++i) @@ -381,7 +385,7 @@ struct statistics { size_t m = products_avg ? 1U : products; m *= 3; - m += 13 + show_sr * 6; + m += 14 + show_sr * 6; os << na; for (size_t i = 0; i < m; ++i) os << ',' << na; @@ -688,6 +692,7 @@ namespace st->weak_aut = true; else st->terminal_aut = true; + st->ambiguous = !spot::is_unambiguous(res); } } output.cleanup(); diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index a9081c58e..31527fffc 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -211,6 +211,7 @@ TESTS_twa = \ babiak.test \ monitor.test \ dra2dba.test \ + unambig.test \ ltlcross4.test \ ltl2dstar.test \ ltl2dstar2.test \ diff --git a/src/tests/unambig.test b/src/tests/unambig.test new file mode 100755 index 000000000..0ca222fe2 --- /dev/null +++ b/src/tests/unambig.test @@ -0,0 +1,84 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement +# de l'Epita +# +# 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 +autfilt=../../bin/autfilt + +for f in 'Ga' \ + 'Ga | Gb' \ + 'Ga | GFb' \ + 'Ga | FGb' \ + 'XFGa | GFb | Gc' \ + '(Ga -> Gb) W c' \ + 'F(a & !b & (!c W b))' +do + $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous + $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous +done + +for f in FGa +do + $ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous + $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous +done + +# All these should be detected as ambiguous automata +cat >input<. + +#include "isunamb.hh" +#include "twaalgos/product.hh" +#include "sccfilter.hh" +#include "stats.hh" +#include +#include + +namespace spot +{ + bool is_unambiguous(const const_twa_graph_ptr& aut) + { + if (aut->is_deterministic()) + return true; + auto clean_a = scc_filter_states(aut); + auto prod = product(clean_a, clean_a); + auto clean_p = scc_filter_states(prod); + tgba_statistics sa = stats_reachable(clean_a); + tgba_statistics sp = stats_reachable(clean_p); + return sa.states == sp.states && sa.transitions == sp.transitions; + } +} diff --git a/src/twaalgos/isunamb.hh b/src/twaalgos/isunamb.hh new file mode 100644 index 000000000..57f7c2a3f --- /dev/null +++ b/src/twaalgos/isunamb.hh @@ -0,0 +1,44 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement +// 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 . + +#pragma once + +#include "twa/twagraph.hh" + +namespace spot +{ + class tgba; + + /// \addtogroup tgba_misc + /// @{ + + /// \brief Whether the automaton \a aut is unambiguous. + /// + /// An automaton is unambiguous if each accepted word is + /// recognized by only one path. + /// + /// We check unambiguousity by synchronizing the automaton with + /// itself, and then making sure that the co-reachable part of the + /// squared automaton has the same size as the co-reachable part of + /// the original automaton. + SPOT_API bool + is_unambiguous(const const_twa_graph_ptr& aut); + + /// @} +}