* 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

@@ -1,17 +1,27 @@
+2010-03-20  Felix Abecassis  <abecassis@lrde.epita.fr>
+
+	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  <abecassis@lrde.epita.fr>
 
 	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
+	Added class tgba_explicit_number, a tgba_explicit where states are
-	by integers.
+	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.

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 \

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 <set>
+#include <algorithm>
+#include <vector>
+#include <map>
+#include <queue>
+#include "minimize.hh"
+#include "ltlast/allnodes.hh"
+#include "misc/hash.hh"
+#include "tgbaalgos/powerset.hh"
+
+namespace spot
+{
+  typedef Sgi::hash_set<const state*,
+                        state_ptr_hash, state_ptr_equal> hash_set;
+  typedef Sgi::hash_map<const state*, unsigned,
+                        state_ptr_hash, state_ptr_equal> 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<state*> 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<hash_set*>& 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<hash_set*>::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<const state*> acc_list;
+    std::queue<hash_set*> todo;
+    std::list<hash_set*> done;
+    tgba_explicit* det_a = tgba_powerset(a, &acc_list);
+    hash_set final;
+    hash_set non_final;
+    hash_map state_set_map;
+    std::list<const state*>::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<std::pair<bdd, hash_set*> > 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<bdd, hash_set*>(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;
+  }
+}

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 */