diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d575a6e5d..86a19e9c7 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -97,16 +97,17 @@ static const argp_option options[] = { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL, "randomize states and transitions (specify 's' or 't' to " "randomize only states or transitions)", 0 }, - { "instut", OPT_INSTUT, 0, 0, "allow more stuttering", 0 }, + { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL, + "allow more stuttering (two possible algorithms)", 0 }, { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filters:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, "keep automata that are isomorphic to the automaton in FILENAME", 0 }, + { "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 }, { "unique", 'u', 0, 0, "do not output the same automaton twice (same in the sense that they "\ "are isomorphic)", 0 }, - { "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 }, { "is-complete", OPT_IS_COMPLETE, 0, 0, "the automaton is complete", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0, @@ -160,7 +161,7 @@ static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; static int opt_max_count = -1; static bool opt_destut = false; -static bool opt_instut = false; +static char opt_instut = 0; static bool opt_is_empty = false; static std::unique_ptr opt_uniq = nullptr; @@ -235,7 +236,12 @@ parse_opt(int key, char* arg, struct argp_state*) opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_INSTUT: - opt_instut = true; + if (!arg || (arg[0] == '1' && arg[1] == 0)) + opt_instut = 1; + else if (arg[0] == '2' && arg[1] == 0) + opt_instut = 2; + else + error(2, 0, "unknown argument for --instut: %s", arg); break; case OPT_DESTUT: opt_destut = true; @@ -375,8 +381,10 @@ namespace if (opt_destut) aut = spot::closure(std::move(aut)); - if (opt_instut) + if (opt_instut == 1) aut = spot::sl(std::move(aut)); + else if (opt_instut == 2) + aut = spot::sl2(std::move(aut)); if (opt_product) aut = spot::product(std::move(aut), opt_product); diff --git a/src/tgbaalgos/closure.cc b/src/tgbaalgos/closure.cc index 22d992b16..da0ca9f06 100644 --- a/src/tgbaalgos/closure.cc +++ b/src/tgbaalgos/closure.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2014 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc index b4a2a1712..7aee575ca 100644 --- a/src/tgbaalgos/stutterize.cc +++ b/src/tgbaalgos/stutterize.cc @@ -1,9 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche +// Copyright (C) 2014, 2015 Laboratoire de Recherche // et Développement de l'Epita (LRDE). -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -152,34 +149,37 @@ namespace spot atomic_propositions = get_all_ap(a); unsigned num_states = a->num_states(); unsigned num_transitions = a->num_transitions(); - for (unsigned state = 0; state < num_states; ++state) + for (unsigned src = 0; src < num_states; ++src) { - auto trans = a->out(state); + auto trans = a->out(src); for (auto it = trans.begin(); it != trans.end() && it.trans() <= num_transitions; ++it) - { - if (it->dst != state) - { - bdd all = it->cond; - while (all != bddfalse) - { - unsigned dst = it->dst; - bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - unsigned tmp = a->new_state(); - unsigned i = a->new_transition(state, tmp, one, - it->acc); - assert(i > num_transitions); - i = a->new_transition(tmp, tmp, one, 0U); - assert(i > num_transitions); - i = a->new_transition(tmp, dst, one, - it->acc); - assert(i > num_transitions); - all -= one; - } - } - } + if (it->dst != src) + { + bdd all = it->cond; + while (all != bddfalse) + { + unsigned dst = it->dst; + bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); + unsigned tmp = a->new_state(); + unsigned i = a->new_transition(src, tmp, one, it->acc); + assert(i > num_transitions); + i = a->new_transition(tmp, tmp, one, 0U); + assert(i > num_transitions); + // No acceptance here to preserve the state-based property. + i = a->new_transition(tmp, dst, one, 0U); + assert(i > num_transitions); + all -= one; + } + } } + if (num_states != a->num_states()) + a->prop_keep({true, // state_based + true, // single_acc + false, // inherently_weak + false, // deterministic + }); a->merge_transitions(); return a; } diff --git a/src/tgbatest/stutter.test b/src/tgbatest/stutter.test index 7a32e69f6..ed0aac383 100755 --- a/src/tgbatest/stutter.test +++ b/src/tgbatest/stutter.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -36,3 +36,13 @@ $ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa $autfilt pos.hoa --product neg.hoa -H > prod.hoa $autfilt --is-empty prod.hoa -q && exit 1 $autfilt --states=12 prod.hoa -q + + +# Check for issue #7. +# +# We just run those without checking the output, it is enough to +# trigger assertions in the HOA output routines. +run 0 ../../bin/ltl2tgba -H 'X(a U b)' > det.hoa +run 0 ../../bin/autfilt --destut det.hoa -H +run 0 ../../bin/autfilt --instut=1 det.hoa -H +run 0 ../../bin/autfilt --instut=2 det.hoa -H