minimize.cc 9.14 KB
Newer Older
1
// Copyright (C) 2010 Laboratoire de Recherche et Développement
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
// 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 <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".
  void init_sets(const tgba_explicit* a,
                 hash_set& final,
38
                 hash_set& non_final)
39
40
  {
    hash_set seen;
Felix Abecassis's avatar
Felix Abecassis committed
41
    std::queue<const state*> tovisit;
42
    // Perform breadth-first traversal.
Felix Abecassis's avatar
Felix Abecassis committed
43
    const state* init = a->get_init_state();
44
45
46
47
    tovisit.push(init);
    seen.insert(init);
    while (!tovisit.empty())
    {
Felix Abecassis's avatar
Felix Abecassis committed
48
      const state* src = tovisit.front();
49
50
51
      tovisit.pop();
      // Is the state final ?
      if (final.find(src) == final.end())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
52
53
	// No, add it to the set non_final
	non_final.insert(src->clone());
54
55
56
      tgba_succ_iterator* sit = a->succ_iter(src);
      for (sit->first(); !sit->done(); sit->next())
      {
Felix Abecassis's avatar
Felix Abecassis committed
57
        const state* dst = sit->current_state();
58
59
60
61
62
63
64
65
66
67
        // 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;
      }
Felix Abecassis's avatar
Felix Abecassis committed
68
      delete sit;
69
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
70
71
72
73
74
75
76
77
78

    while (!seen.empty())
      {
	hash_set::iterator i = seen.begin();
	const state* s = *i;
	seen.erase(i);
	delete s;
      }

79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
  }

  // 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.
105
106
    if (!final->empty())
      res->declare_acceptance_condition(ltl::constant::true_instance());
107
108
109
110
111
112
113
114
115
    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);
Felix Abecassis's avatar
Felix Abecassis committed
116
        bool accepting = (final->find(src) != final->end());
117
118
        for (succit->first(); !succit->done(); succit->next())
        {
Felix Abecassis's avatar
Felix Abecassis committed
119
          const state* dst = succit->current_state();
120
          unsigned dst_num = state_num[dst];
Felix Abecassis's avatar
Felix Abecassis committed
121
          delete dst;
122
123
124
125
126
          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());
        }
Felix Abecassis's avatar
Felix Abecassis committed
127
        delete succit;
128
129
130
131
132
      }
    }
    res->merge_transitions();
    const state* init_state = a->get_init_state();
    unsigned init_num = state_num[init_state];
Felix Abecassis's avatar
Felix Abecassis committed
133
    delete init_state;
134
135
136
137
138
139
140
141
142
    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;
Felix Abecassis's avatar
Felix Abecassis committed
143
    // The list of equivalent states.
144
145
    std::list<hash_set*> done;
    tgba_explicit* det_a = tgba_powerset(a, &acc_list);
Felix Abecassis's avatar
Felix Abecassis committed
146
147
    hash_set* final = new hash_set;
    hash_set* non_final = new hash_set;
148
    hash_map state_set_map;
149
    bdd_dict* dict = det_a->get_dict();
150
151
    std::list<const state*>::iterator li;
    for (li = acc_list.begin(); li != acc_list.end(); ++li)
Felix Abecassis's avatar
Felix Abecassis committed
152
      final->insert(*li);
153
154

    init_sets(det_a, *final, *non_final);
155
156
    // Size of det_a
    unsigned size = final->size() + non_final->size();
157
158
159
160
161
162
163
164
165
    // Use bdd variables to number sets.  set_num is the first variable
    // available.
    unsigned set_num = dict->register_anonymous_variables(size, det_a);

    std::set<int> free_var;
    for (unsigned i = set_num; i < set_num + size; ++i)
      free_var.insert(i);
    std::map<int, int> used_var;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
166
167
    hash_set* final_copy;

168
169
170
171
172
173
174
175
176
177
178
179
    if (!final->empty())
      {
	unsigned s = final->size();
	used_var[set_num] = s;
	free_var.erase(set_num);
	if (s > 1)
	  todo.push(final);
	else
	  done.push_back(final);
	for (hash_set::const_iterator i = final->begin();
	     i != final->end(); ++i)
	  state_set_map[*i] = set_num;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
180
181

	final_copy = new hash_set(*final);
182
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
183
184
185
186
187
    else
      {
	final_copy = final;
      }

188
189
190
191
192
193
194
195
196
197
198
199
200
201
    if (!non_final->empty())
      {
	unsigned s = non_final->size();
	unsigned num = set_num + 1;
	used_var[num] = s;
	free_var.erase(num);
	if (s > 1)
	  todo.push(non_final);
	else
	  done.push_back(non_final);
	for (hash_set::const_iterator i = non_final->begin();
	     i != non_final->end(); ++i)
	  state_set_map[*i] = num;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202
203
204
205
    else
      {
	delete non_final;
      }
206

207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
    // 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;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
222
        tgba_succ_iterator* si = det_a->succ_iter(src);
223
224
225
226
        for (si->first(); !si->done(); si->next())
        {
          const state* dst = si->current_state();
          unsigned dst_set = state_set_map[dst];
Felix Abecassis's avatar
Felix Abecassis committed
227
          delete dst;
228
          f |= (bdd_ithvar(dst_set) & si->current_condition());
229
        }
Felix Abecassis's avatar
Felix Abecassis committed
230
        delete si;
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
        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;
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
          // 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;
278
279
280
281
282
283
284
          // Trivial sets can't be splitted any further.
          if (set->size() == 1)
            done.push_back(set);
          else
            todo.push(set);
        }
      }
Felix Abecassis's avatar
Felix Abecassis committed
285
      delete cur;
286
    }
Felix Abecassis's avatar
Felix Abecassis committed
287
288
289
290
291
292
293
294
295
296
297
298
299
300

    // Build the result.
    tgba_explicit_number* res = build_result(det_a, done, final_copy);

    // Free all the allocated memory.
    delete final_copy;
    hash_map::iterator hit;
    for (hit = state_set_map.begin(); hit != state_set_map.end(); ++hit)
      delete hit->first;
    std::list<hash_set*>::iterator it;
    for (it = done.begin(); it != done.end(); ++it)
      delete *it;
    delete det_a;

301
302
303
    return res;
  }
}