From 03e6dc47697809d7cbd26fc9aacc14fb55e64cc7 Mon Sep 17 00:00:00 2001 From: Felix Abecassis Date: Sat, 20 Mar 2010 14:36:29 +0100 Subject: [PATCH] * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: New files. Algorithm to minimize an automaton using first the powerset construction to determinize the input automaton, the automaton is then minimized using the standard algorithm, using BDDs to check if states are equivalent. --- ChangeLog | 16 ++- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/minimize.cc | 224 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/minimize.hh | 32 ++++++ 4 files changed, 271 insertions(+), 3 deletions(-) create mode 100644 src/tgbaalgos/minimize.cc create mode 100644 src/tgbaalgos/minimize.hh diff --git a/ChangeLog b/ChangeLog index 24c667fd7..304b3033a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,17 +1,27 @@ +2010-03-20 Felix Abecassis + + Algorithm to minimize an automaton. + + * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: + New files. Minimize an automaton using first the powerset + construction to determinize the input automaton, the automaton is then + minimized using the standard algorithm, using BDDs to check if states + are equivalent. + 2010-03-20 Felix Abecassis Modify the powerset algorithm to keep track of accepting states from the initial automaton. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: - Added tgba_explicit_number, a tgba_explicit where states are labelled - by integers. + Added class tgba_explicit_number, a tgba_explicit where states are + labelled by integers. * src/tgbaalgos/powerset.hh, src/tgbaalgos/powerset.cc: When building the deterministic automaton, keep track of which states were created from an accepting state in the initial automaton. The states are added to the new optional parameter (if not 0), acc_list. - Now use tgba_explicit_number instead of tgba_explicit_string to build + Use tgba_explicit_number instead of tgba_explicit_string to build the result. * src/tgbaalgos/scc.cc (spot): Small fix. Print everything on std::cout. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index b4da88996..dc9bd7546 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -42,6 +42,7 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ + minimize.hh \ neverclaim.hh \ powerset.hh \ projrun.hh \ @@ -75,6 +76,7 @@ libtgbaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ + minimize.cc \ ndfs_result.hxx \ neverclaim.cc \ powerset.cc \ diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc new file mode 100644 index 000000000..236b2f57f --- /dev/null +++ b/src/tgbaalgos/minimize.cc @@ -0,0 +1,224 @@ +// Copyright (C) 2010 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 +#include +#include +#include +#include +#include "minimize.hh" +#include "ltlast/allnodes.hh" +#include "misc/hash.hh" +#include "tgbaalgos/powerset.hh" + +namespace spot +{ + typedef Sgi::hash_set hash_set; + typedef Sgi::hash_map hash_map; + + // Given an automaton a, find all states that are not in "final" and add + // them to the set "non_final". + // "state_set_map" gives corresponding set for each state. + void init_sets(const tgba_explicit* a, + hash_set& final, + hash_set& non_final, + hash_map& state_set_map) + { + hash_set seen; + std::queue tovisit; + // Perform breadth-first traversal. + state* init = a->get_init_state(); + tovisit.push(init); + seen.insert(init); + while (!tovisit.empty()) + { + state* src = tovisit.front(); + tovisit.pop(); + // Is the state final ? + if (final.find(src) == final.end()) + { + // No, add it to the set non_final + non_final.insert(src); + state_set_map[src] = 0; + } + else + state_set_map[src] = 1; + tgba_succ_iterator* sit = a->succ_iter(src); + for (sit->first(); !sit->done(); sit->next()) + { + state* dst = sit->current_state(); + // Is it a new state ? + if (seen.find(dst) == seen.end()) + { + // Register the successor for later processing. + tovisit.push(dst); + seen.insert(dst); + } + else + delete dst; + } + } + } + + // From the base automaton and the list of sets, build the minimal + // resulting automaton + tgba_explicit_number* build_result(const tgba* a, + std::list& sets, + hash_set* final) + { + // For each set, create a state in the resulting automaton. + // For a state s, state_num[s] is the number of the state in the minimal + // automaton. + hash_map state_num; + std::list::iterator sit; + unsigned num = 0; + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + for (hit = h->begin(); hit != h->end(); ++hit) + state_num[*hit] = num; + ++num; + } + typedef tgba_explicit_number::transition trs; + tgba_explicit_number* res = new tgba_explicit_number(a->get_dict()); + // For each transition in the initial automaton, add the corresponding + // transition in res. + res->declare_acceptance_condition(ltl::constant::true_instance()); + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + for (hit = h->begin(); hit != h->end(); ++hit) + { + const state* src = *hit; + unsigned src_num = state_num[src]; + tgba_succ_iterator* succit = a->succ_iter(src); + bool accepting = final->find(src) == final->end(); + for (succit->first(); !succit->done(); succit->next()) + { + state* dst = succit->current_state(); + unsigned dst_num = state_num[dst]; + trs* t = res->create_transition(src_num, dst_num); + res->add_conditions(t, succit->current_condition()); + if (accepting) + res->add_acceptance_condition(t, ltl::constant::true_instance()); + } + } + } + res->merge_transitions(); + const state* init_state = a->get_init_state(); + unsigned init_num = state_num[init_state]; + res->set_init_state(init_num); + return res; + } + + tgba_explicit* minimize(const tgba* a) + { + // The list of accepting states of a. + std::list acc_list; + std::queue todo; + std::list done; + tgba_explicit* det_a = tgba_powerset(a, &acc_list); + hash_set final; + hash_set non_final; + hash_map state_set_map; + std::list::iterator li; + for (li = acc_list.begin(); li != acc_list.end(); ++li) + final.insert(*li); + init_sets(det_a, final, non_final, state_set_map); + if (final.size() > 1) + todo.push(&final); + else if (final.size() != 0) + done.push_back(&final); + if (non_final.size() > 1) + todo.push(&non_final); + else if (non_final.size() != 0) + done.push_back(&non_final); + unsigned set_num = 1; + // A bdd_states_map is a list of formulae (in a BDD form) associated with a + // destination set of states. + typedef std::list > bdd_states_map; + // While we have unprocessed sets. + while (!todo.empty()) + { + // Get a set to process. + hash_set* cur = todo.front(); + todo.pop(); + hash_set::iterator hi; + bdd_states_map bdd_map; + for (hi = cur->begin(); hi != cur->end(); ++hi) + { + const state* src = *hi; + bdd f = bddfalse; + tgba_succ_iterator* si = a->succ_iter(src); + for (si->first(); !si->done(); si->next()) + { + const state* dst = si->current_state(); + unsigned dst_set = state_set_map[dst]; + f |= (bdd_ithvar(dst_set) & si->current_condition()); + } + bdd_states_map::iterator bsi; + // Have we already seen this formula ? + for (bsi = bdd_map.begin(); bsi != bdd_map.end() && bsi->first != f; + ++bsi) + continue; + if (bsi == bdd_map.end()) + { + // No, create a new set. + hash_set* new_set = new hash_set; + new_set->insert(src); + bdd_map.push_back(std::make_pair(f, new_set)); + } + else + { + // Yes, add the current state to the set. + hash_set* set = bsi->second; + set->insert(src); + } + } + bdd_states_map::iterator bsi = bdd_map.begin(); + // The set is minimal. + if (bdd_map.size() == 1) + done.push_back(bsi->second); + else + { + for (; bsi != bdd_map.end(); ++bsi) + { + hash_set* set = bsi->second; + // Give a new number for new states. + ++set_num; + hash_set::iterator hit; + for (hit = set->begin(); hit != set->end(); ++hit) + state_set_map[*hit] = set_num; + // Trivial sets can't be splitted any further. + if (set->size() == 1) + done.push_back(set); + else + todo.push(set); + } + } + } + tgba_explicit_number* res = build_result(det_a, done, &final); + return res; + } +} diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh new file mode 100644 index 000000000..a646e47bf --- /dev/null +++ b/src/tgbaalgos/minimize.hh @@ -0,0 +1,32 @@ +// Copyright (C) 2009, 2010 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_MINIMIZE_HH +# define SPOT_TGBAALGOS_MINIMIZE_HH + +# include "tgba/tgbaexplicit.hh" + +namespace spot +{ + tgba_explicit* minimize(const tgba* a); +} + + +#endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */