diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am index f82b98c42..918b82a1a 100644 --- a/src/taalgos/Makefile.am +++ b/src/taalgos/Makefile.am @@ -28,13 +28,19 @@ taalgos_HEADERS = \ sba2ta.hh \ dotty.hh \ reachiter.hh \ - stats.hh \ + stats.hh \ + statessetbuilder.hh \ + minimize.hh \ emptinessta.hh + noinst_LTLIBRARIES = libtaalgos.la libtaalgos_la_SOURCES = \ sba2ta.cc \ dotty.cc \ reachiter.cc \ stats.cc \ + statessetbuilder.cc \ + minimize.cc \ emptinessta.cc + diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc new file mode 100644 index 000000000..a5be1a7bf --- /dev/null +++ b/src/taalgos/minimize.cc @@ -0,0 +1,444 @@ +// Copyright (C) 2010, 2011 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. + + +//#define TRACE + +#ifdef TRACE +# define trace std::cerr +#else +# define trace while (0) std::cerr +#endif + +#include +#include +#include +#include "minimize.hh" +#include "ltlast/allnodes.hh" +#include "misc/hash.hh" +#include "misc/bddlt.hh" +#include "ta/taproduct.hh" +#include "taalgos/statessetbuilder.hh" +#include "tgba/tgbaexplicit.hh" + +namespace spot +{ + typedef Sgi::hash_set hash_set; + typedef Sgi::hash_map + hash_map; + + namespace + { + static std::ostream& + dump_hash_set(const hash_set* hs, const ta* aut, std::ostream& out) + { + out << "{"; + const char* sep = ""; + for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i) + { + out << sep << aut->format_state(*i); + sep = ", "; + } + out << "}"; + return out; + } + + static std::string + format_hash_set(const hash_set* hs, const ta* aut) + { + std::ostringstream s; + dump_hash_set(hs, aut, s); + return s.str(); + } + } + + // From the base automaton and the list of sets, build the minimal + // tgbaulting automaton + ta* + build_result(const ta* a, std::list& sets) + { + tgba_explicit_number* tgba = new tgba_explicit_number(a->get_dict()); + ta_explicit* ta = new ta_explicit(tgba); + + // For each set, create a state in the tgbaulting 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; + } + + // For each transition in the initial automaton, add the corresponding + // transition in ta. + + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + hit = h->begin(); + const state* src = *hit; + unsigned src_num = state_num[src]; + + state* tgba_state = new state_explicit(tgba->add_state(src_num)); + bdd tgba_condition = bddtrue; + bool is_initial_state = a->is_initial_state(src); + if (is_initial_state) + tgba_condition = a->get_state_condition(src); + bool is_accepting_state = a->is_accepting_state(src); + bool is_livelock_accepting_state = a->is_livelock_accepting_state(src); + + state_ta_explicit* new_src = new state_ta_explicit(tgba_state, + tgba_condition, is_initial_state, is_accepting_state, + is_livelock_accepting_state); + + state_ta_explicit* ta_src = ta->add_state(new_src); + + if (ta_src != new_src) + { + delete new_src; + delete tgba_state; + } + else if (is_initial_state) + ta->add_to_initial_states_set(new_src); + + ta_succ_iterator* succit = a->succ_iter(src); + + for (succit->first(); !succit->done(); succit->next()) + { + const state* dst = succit->current_state(); + hash_map::const_iterator i = state_num.find(dst); + + if (i == state_num.end()) // Ignore useless destinations. + continue; + + state* tgba_state = new state_explicit(tgba->add_state(i->second)); + bdd tgba_condition = bddtrue; + is_initial_state = a->is_initial_state(dst); + if (is_initial_state) + tgba_condition = a->get_state_condition(dst); + bool is_accepting_state = a->is_accepting_state(dst); + bool is_livelock_accepting_state = a->is_livelock_accepting_state( + dst); + + state_ta_explicit* new_dst = new state_ta_explicit(tgba_state, + tgba_condition, is_initial_state, is_accepting_state, + is_livelock_accepting_state); + + state_ta_explicit* ta_dst = ta->add_state(new_dst); + + if (ta_dst != new_dst) { + delete new_dst; + delete tgba_state; + } + else if (is_initial_state) + ta->add_to_initial_states_set(new_dst); + + ta->create_transition(ta_src, succit->current_condition(), ta_dst); + + } + delete succit; + } + + return ta; + } + + ta* + minimize_ta(const ta* ta_) + { + + typedef std::list partition_t; + partition_t cur_run; + partition_t next_run; + + // The list of equivalent states. + partition_t done; + + std::set states_set = get_states_set(ta_); + + // livelock acceptance states + hash_set* G = new hash_set; + + // Buchi acceptance states + hash_set* F = new hash_set; + + // Buchi and livelock acceptance states + hash_set* G_F = new hash_set; + + // the other states (non initial and not in G, F and G_F) + hash_set* S = new hash_set; + + std::set::iterator it; + + for (it = states_set.begin(); it != states_set.end(); it++) + { + const state* s = (*it); + + if (ta_->is_initial_state(s)) + { + hash_set* i = new hash_set; + i->insert(s); + done.push_back(i); + } + else if (ta_->is_livelock_accepting_state(s) + && ta_->is_accepting_state(s)) + { + G_F->insert(s); + } + else if (ta_->is_accepting_state(s)) + { + F->insert(s); + } + + else if (ta_->is_livelock_accepting_state(s)) + { + G->insert(s); + } + else + { + S->insert(s); + } + + } + + hash_map state_set_map; + + // Size of ta_ + unsigned size = states_set.size(); + // Use bdd variables to number sets. set_num is the first variable + // available. + unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_); + + std::set free_var; + for (unsigned i = set_num; i < set_num + size; ++i) + free_var.insert(i); + std::map used_var; + + if (!G->empty()) + { + unsigned s = G->size(); + used_var[set_num] = s; + free_var.erase(set_num); + if (s > 1) + cur_run.push_back(G); + else + done.push_back(G); + for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i) + state_set_map[*i] = set_num; + + } + else + delete G; + + if (!F->empty()) + { + unsigned s = F->size(); + unsigned num = set_num + 1; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(F); + else + done.push_back(F); + for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i) + state_set_map[*i] = num; + } + else + delete F; + + if (!G_F->empty()) + { + unsigned s = G_F->size(); + unsigned num = set_num + 2; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(G_F); + else + done.push_back(G_F); + for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i) + state_set_map[*i] = num; + } + else + delete G_F; + + if (!S->empty()) + { + unsigned s = S->size(); + unsigned num = set_num + 3; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(S); + else + done.push_back(S); + for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i) + state_set_map[*i] = num; + } + else + delete S; + + // A bdd_states_map is a list of formulae (in a BDD form) associated with a + // destination set of states. + typedef std::map bdd_states_map; + + bool did_split = true; + + while (did_split) + { + did_split = false; + while (!cur_run.empty()) + { + // Get a set to process. + hash_set* cur = cur_run.front(); + cur_run.pop_front(); + + trace + << "processing " << format_hash_set(cur, ta_) << std::endl; + + hash_set::iterator hi; + bdd_states_map bdd_map; + for (hi = cur->begin(); hi != cur->end(); ++hi) + { + const state* src = *hi; + bdd f = bddfalse; + ta_succ_iterator* si = ta_->succ_iter(src); + for (si->first(); !si->done(); si->next()) + { + const state* dst = si->current_state(); + hash_map::const_iterator i = state_set_map.find(dst); + + if (i == state_set_map.end()) + // The destination state is not in our + // partition. This can happen if the initial + // FINAL and NON_FINAL supplied to the algorithm + // do not cover the whole automaton (because we + // want to ignore some useless states). Simply + // ignore these states here. + continue; + f |= (bdd_ithvar(i->second) & si->current_condition()); + } + delete si; + + // Have we already seen this formula ? + bdd_states_map::iterator bsi = bdd_map.find(f); + if (bsi == bdd_map.end()) + { + // No, create a new set. + hash_set* new_set = new hash_set; + new_set->insert(src); + bdd_map[f] = new_set; + } + else + { + // Yes, add the current state to the set. + bsi->second->insert(src); + } + } + + bdd_states_map::iterator bsi = bdd_map.begin(); + if (bdd_map.size() == 1) + { + // The set was not split. + trace + << "set " << format_hash_set(bsi->second, ta_) + << " was not split" << std::endl; + next_run.push_back(bsi->second); + } + else + { + for (; bsi != bdd_map.end(); ++bsi) + { + hash_set* set = bsi->second; + // Free the number associated to these states. + unsigned num = state_set_map[*set->begin()]; + assert(used_var.find(num) != used_var.end()); + unsigned left = (used_var[num] -= set->size()); + // Make sure LEFT does not become negative (hence bigger + // than SIZE when read as unsigned) + assert(left < size); + if (left == 0) + { + used_var.erase(num); + free_var.insert(num); + } + // Pick a free number + assert(!free_var.empty()); + num = *free_var.begin(); + free_var.erase(free_var.begin()); + used_var[num] = set->size(); + for (hash_set::iterator hit = set->begin(); hit + != set->end(); ++hit) + state_set_map[*hit] = num; + // Trivial sets can't be splitted any further. + if (set->size() == 1) + { + trace + << "set " << format_hash_set(set, ta_) + << " is minimal" << std::endl; + done.push_back(set); + } + else + { + did_split = true; + trace + << "set " << format_hash_set(set, ta_) + << " should be processed further" << std::endl; + next_run.push_back(set); + } + } + } + delete cur; + } + if (did_split) + trace + << "splitting did occur during this pass." << std::endl; + //elsetrace << "splitting did not occur during this pass." << std::endl; + std::swap(cur_run, next_run); + } + + done.splice(done.end(), cur_run); + +#ifdef TRACE + trace << "Final partition: "; + for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) + trace << format_hash_set(*i, ta_) << " "; + trace << std::endl; +#endif + + // Build the tgbault. + ta* res = build_result(ta_, done); + + // Free all the allocated memory. + std::list::iterator itdone; + for (itdone = done.begin(); itdone != done.end(); ++itdone) + delete *itdone; + delete ta_; + + return res; + } + +} diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh new file mode 100644 index 000000000..367f4ae8e --- /dev/null +++ b/src/taalgos/minimize.hh @@ -0,0 +1,36 @@ +// Copyright (C) 2009, 2010, 2011 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_TAALGOS_MINIMIZE_HH +# define SPOT_TAALGOS_MINIMIZE_HH + +# include "ta/ta.hh" +# include "ta/taexplicit.hh" + +namespace spot +{ + + ta* + minimize_ta(const ta* ta_); + +/// @} +} + +#endif /* !SPOT_TAALGOS_MINIMIZE_HH */ diff --git a/src/taalgos/statessetbuilder.cc b/src/taalgos/statessetbuilder.cc new file mode 100644 index 000000000..2b1cfbdd6 --- /dev/null +++ b/src/taalgos/statessetbuilder.cc @@ -0,0 +1,69 @@ +// 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 "ta/ta.hh" +#include "statessetbuilder.hh" +#include "reachiter.hh" + +namespace spot +{ + namespace + { + class states_set_builder_bfs : public ta_reachable_iterator_breadth_first + { + public: + states_set_builder_bfs(const ta* a) : + ta_reachable_iterator_breadth_first(a) + { + } + + void + process_state(const state* s, int) + { + states_set_.insert(s); + } + + void + process_link(int, int, const ta_succ_iterator*) + { + } + + std::set + get_states_set() + { + return states_set_; + } + + private: + std::set states_set_; + }; + } // anonymous + + + + std::set + get_states_set(const ta* t) + { + states_set_builder_bfs d(t); + d.run(); + return d.get_states_set(); + } +} diff --git a/src/taalgos/statessetbuilder.hh b/src/taalgos/statessetbuilder.hh new file mode 100644 index 000000000..2745c7b16 --- /dev/null +++ b/src/taalgos/statessetbuilder.hh @@ -0,0 +1,35 @@ +// 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. + +#ifndef SPOT_TAALGOS_STATESSETBUILDER_HH +# define SPOT_TAALGOS_STATESSETBUILDER_HH + +#include "ta/ta.hh" + +namespace spot +{ + + /// \brief Compute states set for an automaton. + std::set get_states_set(const ta* t); + + /// @} +} + +#endif // SPOT_TAALGOS_STATESSETBUILDER_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3d0a074d5..abaca0e40 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -49,6 +49,7 @@ #include "neverparse/public.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/minimize.hh" +#include "taalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" @@ -281,7 +282,11 @@ syntax(char* prog) << "Options for Testing Automata:" << std::endl << " -TA Translate an LTL formula into a Testing automata" - << std::endl; + << std::endl + << std::endl + << " -TM Translate an LTL formula into a minimal Testing automata" + << std::endl; + exit(2); } @@ -343,6 +348,7 @@ main(int argc, char** argv) spot::tgba* temp_dir_sim = 0; bool ta_opt = false; + for (;;) { if (argc < formula_index + 2) @@ -673,6 +679,11 @@ main(int argc, char** argv) { ta_opt = true; } + else if (!strcmp(argv[formula_index], "-TM")) + { + ta_opt = true; + opt_minimize = true; + } else if (!strcmp(argv[formula_index], "-taa")) { translation = TransTAA; @@ -1084,9 +1095,10 @@ main(int argc, char** argv) delete aps; spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd); + if (opt_minimize) testing_automata = minimize_ta(testing_automata); spot::dotty_reachable(std::cout, testing_automata); delete testing_automata; - delete degeneralized_new; + output = -1; }