diff --git a/NEWS b/NEWS index 8de6a1918..a6cbba013 100644 --- a/NEWS +++ b/NEWS @@ -53,6 +53,9 @@ New in spot 1.1.4a (not relased) This makes it more homogeneous with the --stats option of the new dstar2tgba command. + Additionally, the %p escape can now be used to show whether the + output automaton is complete. + * All the parsers implemented in Spot now use the same type to store locations. diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 683b4c749..21d2d29d6 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -100,6 +100,8 @@ static const argp_option options[] = "number of nondeterministic states in output", 0 }, { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "1 if the output is deterministic, 0 otherwise", 0 }, + { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the output is complete, 0 otherwise", 0 }, { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, /**************************************************/ diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index d137d455f..5b87b22f8 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -91,6 +91,8 @@ static const argp_option options[] = "number of nondeterministic states", 0 }, { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "1 if the automaton is deterministic, 0 otherwise", 0 }, + { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the automaton is complete, 0 otherwise", 0 }, { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, /**************************************************/ diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc index 367f1e1f0..447e33f82 100644 --- a/src/tgbaalgos/isdet.cc +++ b/src/tgbaalgos/isdet.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -30,10 +30,9 @@ namespace spot count_nondet_states_aux(const tgba* aut, bool count = true) { unsigned res = 0; - typedef std::set seen_set; typedef std::deque todo_list; - seen_set seen; + state_set seen; todo_list todo; { const state* s = aut->get_init_state(); @@ -46,9 +45,8 @@ namespace spot todo.pop_front(); tgba_succ_iterator* i = aut->succ_iter(src); - tgba_succ_iterator* j = aut->succ_iter(src); - unsigned in = 0; bool nondeterministic = false; + bdd available = bddtrue; for (i->first(); !i->done(); i->next()) { // If we know the state is nondeterministic, just skip the @@ -57,22 +55,11 @@ namespace spot // destination states. if (!nondeterministic) { - ++in; - // Move j to the transition that follows i. - j->first(); - for (unsigned jn = 0; jn < in; ++jn) - j->next(); - // Make sure transitions after i are not conflicting. - while (!j->done()) - { - if ((i->current_condition() & j->current_condition()) - != bddfalse) - { - nondeterministic = true; - break; - } - j->next(); - } + bdd label = i->current_condition(); + if (!bdd_implies(label, available)) + nondeterministic = true; + else + available -= label; } const state* dst = i->current_state(); if (seen.insert(dst).second) @@ -80,13 +67,12 @@ namespace spot else dst->destroy(); } - delete j; delete i; res += nondeterministic; if (!count && nondeterministic) break; } - for (seen_set::const_iterator i = seen.begin(); i != seen.end();) + for (state_set::const_iterator i = seen.begin(); i != seen.end();) { const state* s = *i++; s->destroy(); @@ -106,4 +92,47 @@ namespace spot { return !count_nondet_states_aux(aut, false); } + + bool + is_complete(const tgba* aut) + { + state_set seen; + typedef std::deque todo_list; + todo_list todo; + bool complete = true; + { + const state* s = aut->get_init_state(); + seen.insert(s); + todo.push_back(s); + } + while (!todo.empty()) + { + const state* src = todo.front(); + todo.pop_front(); + + tgba_succ_iterator* i = aut->succ_iter(src); + bdd available = bddtrue; + for (i->first(); !i->done(); i->next()) + { + available -= i->current_condition(); + const state* dst = i->current_state(); + if (seen.insert(dst).second) + todo.push_back(dst); + else + dst->destroy(); + } + delete i; + if (available != bddfalse) + { + complete = false; + break; + } + } + for (state_set::const_iterator i = seen.begin(); i != seen.end();) + { + const state* s = *i++; + s->destroy(); + } + return complete; + } } diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index 19e3b4f36..294bab1bf 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.hh @@ -43,6 +43,13 @@ namespace spot SPOT_API bool is_deterministic(const tgba* aut); + /// \Brief Return true iff \a aut is complete. + /// + /// An automaton is complete if its translation relation is total, + /// i.e., each state as a successor for any possible configuration. + SPOT_API bool + is_complete(const tgba* aut); + /// @} } diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index cd7d99534..a71726449 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -147,6 +147,7 @@ namespace spot declare('e', &edges_); declare('f', &form_); declare('n', &nondetstates_); + declare('p', &complete_); declare('s', &states_); declare('S', &scc_); // Historical. Deprecated. Use %c instead. declare('t', &trans_); @@ -195,6 +196,11 @@ namespace spot deterministic_ = is_deterministic(aut); } + if (has('p')) + { + complete_ = is_complete(aut); + } + return format(format_); } diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 1b7140d7c..a8a58c4b8 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -98,6 +98,7 @@ namespace spot printable_value scc_; printable_value nondetstates_; printable_value deterministic_; + printable_value complete_; }; /// @} diff --git a/src/tgbatest/nondet.test b/src/tgbatest/nondet.test index ae4e4c53f..fa868824f 100755 --- a/src/tgbatest/nondet.test +++ b/src/tgbatest/nondet.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,13 +21,17 @@ . ./defs set -e -../../bin/ltl2tgba FGa GFa --stats='%f %d' >out.1 cat >expected.1<out.1 + +diff out.1 expected.1 ../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s' >out.2 cat >expected.2<