From 6f7f9ef8bcf7172c6badf178d72603e6e0ccb8e0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 11 Jan 2015 13:58:52 +0100 Subject: [PATCH] isdet: rewrite using the tgba_digraph interface * src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: Rewrite using the tgba_digraph interface. * src/tgbatest/ltl2tgba.cc: Adjust call. --- src/tgbaalgos/isdet.cc | 110 +++++++++++---------------------------- src/tgbaalgos/isdet.hh | 10 ++-- src/tgbatest/ltl2tgba.cc | 2 +- 3 files changed, 36 insertions(+), 86 deletions(-) diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc index 2c33082e9..9d9ae40ea 100644 --- a/src/tgbaalgos/isdet.cc +++ b/src/tgbaalgos/isdet.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,66 +28,40 @@ namespace spot template static unsigned - count_nondet_states_aux(const const_tgba_ptr& aut) + count_nondet_states_aux(const const_tgba_digraph_ptr& aut) { - unsigned res = 0; - typedef std::deque todo_list; - - state_set seen; - todo_list todo; - { - const state* s = aut->get_init_state(); - seen.insert(s); - todo.push_back(s); - } - while (!todo.empty()) + unsigned nondet_states = 0; + unsigned ns = aut->num_states(); + for (unsigned src = 0; src < ns; ++src) { - const state* src = todo.front(); - todo.pop_front(); - - bool nondeterministic = false; bdd available = bddtrue; - for (auto i: aut->succ(src)) - { - // 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) - { - 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) - todo.push_back(dst); - else - dst->destroy(); - } - res += nondeterministic; - if (!count && nondeterministic) + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + { + ++nondet_states; + break; + } + else + { + available -= t.cond; + } + // If we are not counting non-deterministic states, abort as + // soon as possible. + if (!count && nondet_states) break; } - for (state_set::const_iterator i = seen.begin(); i != seen.end();) - { - const state* s = *i++; - s->destroy(); - } - return res; + return nondet_states; } } unsigned - count_nondet_states(const const_tgba_ptr& aut) + count_nondet_states(const const_tgba_digraph_ptr& aut) { return count_nondet_states_aux(aut); } bool - is_deterministic(const const_tgba_ptr& aut) + is_deterministic(const const_tgba_digraph_ptr& aut) { if (aut->is_deterministic()) return true; @@ -95,43 +69,19 @@ namespace spot } bool - is_complete(const const_tgba_ptr& aut) + is_complete(const const_tgba_digraph_ptr& 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()) + unsigned ns = aut->num_states(); + for (unsigned src = 0; src < ns; ++src) { - const state* src = todo.front(); - todo.pop_front(); - bdd available = bddtrue; - for (auto i: aut->succ(src)) - { - available -= i->current_condition(); - const state* dst = i->current_state(); - if (seen.insert(dst).second) - todo.push_back(dst); - else - dst->destroy(); - } + for (auto& t: aut->out(src)) + available -= t.cond; if (available != bddfalse) - { - complete = false; - break; - } + return false; } - for (state_set::const_iterator i = seen.begin(); i != seen.end();) - { - const state* s = *i++; - s->destroy(); - } - return complete; + // The empty automaton is not complete since it does not have an + // initial state. + return ns > 0; } } diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index 54989e8bd..a43f464c1 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,7 +20,7 @@ #ifndef SPOT_TGBAALGOS_ISDET_HH # define SPOT_TGBAALGOS_ISDET_HH -# include "tgba/tgba.hh" +# include "tgba/tgbagraph.hh" namespace spot { @@ -33,7 +33,7 @@ namespace spot /// but it is more efficient to call is_deterministic() if you do not /// care about the number of nondeterministic states. SPOT_API unsigned - count_nondet_states(const const_tgba_ptr& aut); + count_nondet_states(const const_tgba_digraph_ptr& aut); /// \brief Return true iff \a aut is deterministic. /// @@ -41,14 +41,14 @@ namespace spot /// the automaton is nondeterministic, because it can return before /// the entire automaton has been explored. SPOT_API bool - is_deterministic(const const_tgba_ptr& aut); + is_deterministic(const const_tgba_digraph_ptr& 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 const_tgba_ptr& aut); + is_complete(const const_tgba_digraph_ptr& aut); /// @} } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7bf35f956..6b5c65512 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1638,7 +1638,7 @@ checked_main(int argc, char** argv) case 13: sub_stats_reachable(a).dump(std::cout); std::cout << "nondeterministic states: " - << count_nondet_states(a) << std::endl; + << count_nondet_states(ensure_digraph(a)) << std::endl; break; case 14: if (!wdba_minimization_is_success)