degen.cc 10.6 KB
Newer Older
1
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
// Copyright (C) 2012 Laboratoire de Recherche et
// Développement de l'Epita.
//
// 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 "degen.hh"
#include "tgba/tgbaexplicit.hh"
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include "ltlast/constant.hh"
#include <deque>
#include <vector>

namespace spot
{
  namespace
  {
    // A state in the degenalized automaton corresponds to a state in
    // the TGBA associated to a level.  The level is just an index in
    // the list of acceptance sets.
    typedef std::pair<const state*, unsigned> degen_state;

    struct degen_state_hash
    {
      size_t
      operator()(const degen_state& s) const
      {
	return s.first->hash() & wang32_hash(s.second);
      }
    };

    struct degen_state_equal
    {
      bool
      operator()(const degen_state& left,
		 const degen_state& right) const
      {
	if (left.second != right.second)
	  return false;
	return left.first->compare(right.first) == 0;
      }
    };

    // Associate the degeneralized state to its number.
    typedef Sgi::hash_map<degen_state, int,
			  degen_state_hash, degen_state_equal> ds2num_map;

    // Queue of state to be processed.
    typedef std::deque<degen_state> queue_t;

    // Memory management for the input states.
    class unicity_table
    {
      typedef Sgi::hash_set<const state*,
			    state_ptr_hash, state_ptr_equal> uniq_set;
      uniq_set m;
    public:
      const state* operator()(const state* s)
      {
	uniq_set::const_iterator i = m.find(s);
	if (i == m.end())
	  {
	    m.insert(s);
	    return s;
	  }
	else
	  {
	    s->destroy();
	    return *i;
	  }
      }

      ~unicity_table()
      {
	for (uniq_set::iterator i = m.begin(); i != m.end(); ++i)
	  (*i)->destroy();
      }
    };

    // Acceptance set common to all outgoing transitions of some state.
    class outgoing_acc
    {
      const tgba* a_;
100
101
102
103
      typedef std::pair<bdd, bdd> cache_entry;
      typedef Sgi::hash_map<const state*, cache_entry,
			    state_ptr_hash, state_ptr_equal> cache_t;
      cache_t cache_;
104
105
106
107
108
109

    public:
      outgoing_acc(const tgba* a): a_(a)
      {
      }

110
      cache_t::const_iterator fill_cache(const state* s)
111
112
      {
	bdd common = a_->all_acceptance_conditions();
113
	bdd union_ = bddfalse;
114
	tgba_succ_iterator* it = a_->succ_iter(s);
115
116
117
118
119
120
	for (it->first(); !it->done(); it->next())
	  {
	    bdd set = it->current_acceptance_conditions();
	    common &= set;
	    union_ |= set;
	  }
121
	delete it;
122
123
124
	cache_entry e(common, union_);
	return cache_.insert(std::make_pair(s, e)).first;
      }
125

126
127
128
129
130
131
132
      // Intersection of all outgoing acceptance sets
      bdd common_acc(const state* s)
      {
	cache_t::const_iterator i = cache_.find(s);
	if (i == cache_.end())
	  i = fill_cache(s);
	return i->second.first;
133
134
      }

135
      // Union of all outgoing acceptance sets
136
137
      bdd union_acc(const state* s)
      {
138
139
140
141
	cache_t::const_iterator i = cache_.find(s);
	if (i == cache_.end())
	  i = fill_cache(s);
	return i->second.second;
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
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
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
      }
    };
  }

  sba*
  degeneralize(const tgba* a)
  {
    bdd_dict* dict = a->get_dict();

    // The result (degeneralized) automaton uses numbered state.
    sba_explicit_number* res = new sba_explicit_number(dict);
    dict->register_all_variables_of(a, res);
    // FIXME: unregister acceptance conditions.

    // Invent a new acceptance set for the degeneralized automaton.
    int accvar =
      dict->register_acceptance_variable(ltl::constant::true_instance(), res);
    bdd degen_acc = bdd_ithvar(accvar);
    res->set_acceptance_conditions(degen_acc);

    // Create an order of acceptance conditions.  Each entry in this
    // vector correspond to an acceptance set.  Each index can
    // be used as a level in degen_state to indicate the next expected
    // acceptance set.  Level order.size() is a special level used to
    // denote accepting states.
    std::vector<bdd> order;
    {
      // The order is arbitrary, but it turns out that using push_back
      // instead of push_front often gives better results because
      // acceptance sets at the beginning if the cycle are more often
      // used in the automaton.  (This surprising fact is probably
      // related to the order in which we declare the BDD variables
      // during the translation.)
      bdd all = a->all_acceptance_conditions();
      while (all != bddfalse)
	{
	  bdd next = bdd_satone(all);
	  all -= next;
	  order.push_back(next);
	}
    }

    outgoing_acc outgoing(a);

    // Make sure we always use the same pointer for identical states
    // from the input automaton.
    unicity_table uniq;

    // These maps make it possible to convert degen_state to number
    // and vice-versa.
    ds2num_map ds2num;

    queue_t todo;

    const state* s0 = uniq(a->get_init_state());
    degen_state s(s0, 0);

    // As an heuristic, if the initial state has accepting self-loops,
    // start the degeneralization on the accepting level.
    {
      bdd all = a->all_acceptance_conditions();
      tgba_succ_iterator* it = a->succ_iter(s0);
      for (it->first(); !it->done(); it->next())
	{
	  // Look only for transitions that are accepting.
	  if (all != it->current_acceptance_conditions())
	    continue;
	  // Look only for self-loops.
	  const state* dest = uniq(it->current_state());
	  if (dest == s0)
	    {
	      // The initial state has an accepting self-loop.
	      s.second = order.size();
	      break;
	    }
	}
      delete it;
    }

    ds2num[s] = 0;
    todo.push_back(s);

    while (!todo.empty())
      {
	s = todo.front();
	todo.pop_front();
	int src = ds2num[s];
	unsigned slevel = s.second;

	// If we have a state on the last level, it should be accepting.
	bool is_acc = slevel == order.size();
	// On the accepting level, start again from level 0.
	if (is_acc)
	  slevel = 0;

	tgba_succ_iterator* i = a->succ_iter(s.first);
	for (i->first(); !i->done(); i->next())
	  {
	    degen_state d(uniq(i->current_state()), 0);

	    // The old level is slevel.  What should be the new one?
	    bdd acc = i->current_acceptance_conditions();
	    bdd otheracc = outgoing.common_acc(d.first);

	    if (is_acc)
	      {
		// Ignore the last expected acceptance set (the value of
		// *prev below) if it is common to all other outgoing
		// transitions (of the current state) AND if it is not
		// used by any outgoing transition of the destination
		// state.
		//
		// 1) It's correct to do that, because this acceptance
		//    set is common to other outgoing transitions.
		//    Therefore if we make a cycle to this state we
		//    will eventually see that acceptance set thanks
		//    to the "pulling" of the common acceptance sets
		//    of the destination state (d.first).
		//
		// 2) It's also desirable because it makes the
		//    degeneralization idempotent (up to a renaming of
		//    states).  Consider the following automaton where
		//    1 is initial and => marks accepting transitions:
		//    1=>1, 1=>2, 2->2, 2->1 This is already an SBA,
		//    with 1 as accepting state.  However if you try
		//    degeralize it without ignoring *prev, you'll get
		//    two copies of states 2, depending on whether we
		//    reach it using 1=>2 or from 2->2.  If this
		//    example was not clear, uncomment this following
		//    "if" block, and play with the "degenid.test"
		//    test case.
		//
		// 3) Ignoring all common acceptance sets would also
		//    be correct, but it would make the
		//    degeneralization produce larger automata in some
		//    cases.  The current condition to ignore only one
		//    acceptance set if is this not used by the next
		//    state is a heuristic that is compatible with
		//    point 2) above while not causing more states to
		//    be generated in our benchmark of 188 formulae
		//    from the literature.
                if (!order.empty())
                  {
                    unsigned prev = order.size() - 1;
                    bdd common = outgoing.common_acc(s.first);
                    if ((common & order[prev]) == order[prev])
                      {
                        bdd u = outgoing.union_acc(d.first);
                        if ((u & order[prev]) != order[prev])
                          acc -= order[prev];
                      }
                  }
	      }
	    // A transition in the SLEVEL acceptance set should
	    // be directed to the next acceptance set.  If the
	    // current transition is also in the next acceptance
	    // set, then go to the one after, etc.
	    //
	    // See Denis Oddoux's PhD thesis for a nice
	    // explanation (in French).
	    // @PhDThesis{    oddoux.03.phd,
	    //   author     = {Denis Oddoux},
	    //   title      = {Utilisation des automates alternants pour un
	    //                model-checking efficace des logiques
	    //                temporelles lin{\'e}aires.},
	    //   school     = {Universit{\'e}e Paris 7},
	    //   year       = {2003},
	    //   address= {Paris, France},
	    //   month      = {December}
	    // }
	    unsigned next = slevel;
	    // Consider both the current acceptance sets, and the
	    // acceptance sets common to the outgoing transitions of
	    // the destination state.
	    acc |= otheracc;
	    while (next < order.size()
		   && (acc & order[next]) == order[next])
	      ++next;

	    d.second = next;

	    // Have we already seen this destination?
	    int dest;
	    ds2num_map::const_iterator di = ds2num.find(d);
	    if (di != ds2num.end())
	      {
		dest = di->second;
	      }
	    else
	      {
		dest = ds2num.size();
		ds2num[d] = dest;
		todo.push_back(d);
	      }

	    // Actually create the transition.
	    state_explicit_number::transition* t
	      = res->create_transition(src, dest);
	    t->condition = i->current_condition();
	    // If the source state is accepting, we have to put
	    // degen_acc on all outgoing transitions.  (We are still
	    // building a TGBA; we only assure that it can be used as
	    // an SBA.)
	    t->acceptance_conditions = is_acc ? degen_acc : bddfalse;
	  }
	delete i;
      }

    res->merge_transitions();
    return res;
  }
}