diff --git a/NEWS b/NEWS index 70af4f913..cb130cf2c 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,9 @@ New in spot 0.9.2a: minimization it cases it would produce a deterministic automaton that is bigger than the original TGBA. So this effectively gives the choice between less states or more determinism. + * new functions is_deterministic() and count_nondet_states() + (The count of nondeterministic states is now displayed on + automata generated with the web interface.) * Useful command-line tools are now installed in addition to the library. Some of these tools were originally written for our test suite and had evolved organically into useful @@ -48,8 +51,9 @@ New in spot 0.9.2a: (e.g., match only safety formulas that are larger than some given size). Besides being used as a "grep" tool for formulas, this can also be used to convert - files of formulas between different syntaxes, and apply - some simplifications. + files of formulas between different syntaxes, apply + some simplifications, check whether to formulas are + equivalent, ... New in spot 0.9.2 (2012-07-02): diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 79016813a..15f665b09 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -40,6 +40,7 @@ tgbaalgos_HEADERS = \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ + isdet.hh \ lbtt.hh \ ltl2taa.hh \ ltl2tgba_fm.hh \ @@ -77,6 +78,7 @@ libtgbaalgos_la_SOURCES = \ eltl2tgba_lacim.cc \ emptiness.cc \ gv04.cc \ + isdet.cc \ lbtt.cc \ ltl2taa.cc \ ltl2tgba_fm.cc \ diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc new file mode 100644 index 000000000..be80419e6 --- /dev/null +++ b/src/tgbaalgos/isdet.cc @@ -0,0 +1,111 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "tgbaalgos/isdet.hh" +#include +#include + +namespace spot +{ + namespace + { + static + unsigned + 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; + todo_list todo; + { + 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); + tgba_succ_iterator* j = aut->succ_iter(src); + unsigned in = 0; + bool nondeterministic = false; + for (i->first(); !i->done(); i->next()) + { + // If we know the state is nondeterministic, just skip the + // test for the remaining transitions. But don't break + // the loop, because we still have to record the + // 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(); + } + } + const state* dst = i->current_state(); + if (seen.insert(dst).second) + todo.push_back(dst); + else + dst->destroy(); + } + delete j; + delete i; + res += nondeterministic; + if (!count && nondeterministic) + break; + } + for (seen_set::const_iterator i = seen.begin(); i != seen.end();) + { + const state* s = *i++; + s->destroy(); + } + return res; + } + } + + unsigned + count_nondet_states(const tgba* aut) + { + return count_nondet_states_aux(aut); + } + + bool + is_deterministic(const tgba* aut) + { + return !!count_nondet_states_aux(aut, false); + } +} diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh new file mode 100644 index 000000000..3a602d173 --- /dev/null +++ b/src/tgbaalgos/isdet.hh @@ -0,0 +1,49 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_ISDET_HH +# define SPOT_TGBAALGOS_ISDET_HH + +# include "tgba/tgba.hh" + +namespace spot +{ + /// \addtogroup tgba_misc + /// @{ + + /// \brief Count the number of non-deterministic states in \a aut. + /// + /// The automaton is deterministic if it has 0 nondeterministic states, + /// but it is more efficient to call is_deterministic() if you do not + /// care about the number of nondeterministic states. + unsigned count_nondet_states(const tgba* aut); + + /// \brief Return true iff \a aut is deterministic. + /// + /// This function is more efficient than count_nondet_states() when + /// the automaton is nondeterministic, because it can return before + /// the entire automaton has been explored. + bool is_deterministic(const tgba* aut); + + /// @} +} + +#endif // SPOT_TGBAALGOS_ISDET_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 53c3c7cee..ea1779899 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -63,6 +63,7 @@ #include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/scc.hh" +#include "tgbaalgos/isdet.hh" #include "kripkeparse/public.hh" #include "tgbaalgos/simulation.hh" @@ -1367,6 +1368,8 @@ main(int argc, char** argv) break; case 13: sub_stats_reachable(a).dump(std::cout); + std::cout << "nondeterministic states: " + << count_nondet_states(a) << std::endl; break; case 14: if (minimized == 0) diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 7499d6cf7..008c9cd79 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -300,11 +300,17 @@ def render_formula(f): spot.dotty(dotsrc, f) render_dot_maybe(dotsrc.str(), False) -def print_stats(automaton): +def print_stats(automaton, detinfo = False): stats = spot.stats_reachable(automaton) unbufprint("

%d state" % stats.states) if stats.states > 1: unbufprint("s") + if detinfo: + nondet = spot.count_nondet_states(automaton) + if nondet == 0: + unbufprint(" (deterministic)") + else: + unbufprint(" (%d nondeterministic)" % nondet) unbufprint(", %d transition" % stats.transitions) if stats.transitions > 1: unbufprint("s") @@ -314,8 +320,8 @@ def print_stats(automaton): unbufprint(", %d acceptance condition" % count) if count > 1: unbufprint("s") - acc = automaton.all_acceptance_conditions() - unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) + acc = automaton.all_acceptance_conditions() + unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) else: unbufprint(", no acceptance condition (all cycles are accepting)") unbufprint("

\n") @@ -674,7 +680,7 @@ if output_type == 'a': unbufprint('
%s
' % cgi.escape(s.str())) del s else: # 't' or 's' - dont_run_dot = print_stats(degen) + dont_run_dot = print_stats(degen, True) render_automaton(degen, dont_run_dot, issba) degen = 0 automaton = 0 diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 361cc2670..c450aa4d0 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -108,6 +108,7 @@ namespace std { #include "tgbaalgos/safety.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/stats.hh" +#include "tgbaalgos/isdet.hh" #include "tgbaalgos/simulation.hh" #include "tgbaparse/public.hh" @@ -272,6 +273,7 @@ using namespace spot; %include "tgbaalgos/safety.hh" %include "tgbaalgos/sccfilter.hh" %include "tgbaalgos/stats.hh" +%include "tgbaalgos/isdet.hh" %include "tgbaalgos/simulation.hh" %include "tgbaparse/public.hh"