degen.cc 17.7 KB
Newer Older
1
2
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita.
3
4
5
6
7
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
// (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
17
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
19
20
21
22
23
24
25
26


#include "degen.hh"
#include "tgba/tgbaexplicit.hh"
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include "ltlast/constant.hh"
#include <deque>
#include <vector>
27
28
29
30
#include "tgbaalgos/scc.hh"
#include "tgba/bddprint.hh"

//#define DEGEN_DEBUG
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

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
      {
46
        return s.first->hash() & wang32_hash(s.second);
47
48
49
50
51
52
53
      }
    };

    struct degen_state_equal
    {
      bool
      operator()(const degen_state& left,
54
                 const degen_state& right) const
55
      {
56
57
58
        if (left.second != right.second)
          return false;
        return left.first->compare(right.first) == 0;
59
60
61
62
63
      }
    };

    // Associate the degeneralized state to its number.
    typedef Sgi::hash_map<degen_state, int,
64
                          degen_state_hash, degen_state_equal> ds2num_map;
65
66
67
68
69
70
71
72

    // 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*,
73
                            state_ptr_hash, state_ptr_equal> uniq_set;
74
75
76
77
      uniq_set m;
    public:
      const state* operator()(const state* s)
      {
78
79
80
81
82
83
84
85
86
87
88
        uniq_set::const_iterator i = m.find(s);
        if (i == m.end())
          {
            m.insert(s);
            return s;
          }
        else
          {
            s->destroy();
            return *i;
          }
89
90
91
92
      }

      ~unicity_table()
      {
93
94
95
96
97
98
99
	for (uniq_set::iterator i = m.begin(); i != m.end();)
	  {
	    // Advance the iterator before destroying its key.  This
	    // avoid issues with old g++ implementations.
	    uniq_set::iterator old = i++;
	    (*old)->destroy();
	  }
100
      }
101
102
103
104
105
106

      size_t
      size()
      {
        return m.size();
      }
107
108
109
110
111
112
    };

    // Acceptance set common to all outgoing transitions of some state.
    class outgoing_acc
    {
      const tgba* a_;
113
114
      typedef std::pair<bdd, bdd> cache_entry;
      typedef Sgi::hash_map<const state*, cache_entry,
115
                            state_ptr_hash, state_ptr_equal> cache_t;
116
      cache_t cache_;
117
118
119
120
121
122

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

123
      cache_t::const_iterator fill_cache(const state* s)
124
      {
125
126
127
128
129
130
131
132
133
134
135
136
        bdd common = a_->all_acceptance_conditions();
        bdd union_ = bddfalse;
        tgba_succ_iterator* it = a_->succ_iter(s);
        for (it->first(); !it->done(); it->next())
          {
            bdd set = it->current_acceptance_conditions();
            common &= set;
            union_ |= set;
          }
        delete it;
        cache_entry e(common, union_);
        return cache_.insert(std::make_pair(s, e)).first;
137
      }
138

139
140
141
      // Intersection of all outgoing acceptance sets
      bdd common_acc(const state* s)
      {
142
143
144
145
        cache_t::const_iterator i = cache_.find(s);
        if (i == cache_.end())
          i = fill_cache(s);
        return i->second.first;
146
147
      }

148
      // Union of all outgoing acceptance sets
149
150
      bdd union_acc(const state* s)
      {
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
        cache_t::const_iterator i = cache_.find(s);
        if (i == cache_.end())
          i = fill_cache(s);
        return i->second.second;
      }
    };

    // Order of accepting sets (for one SCC)
    class acc_order
    {
      std::vector<bdd> order_;
      bdd found_;

    public:
      unsigned
      next_level(bdd all, int slevel, bdd acc)
      {
        bdd temp = acc;
        if (all != found_)
          {
            // Check for new conditions in acc
            if ((acc & found_) != acc)
              {
                bdd acc_t = acc;
                while (acc_t != bddfalse)
                {
                  bdd next = bdd_satone(acc_t);
                  acc_t -= next;
                  // Add new condition
                  if ((next & found_) != next)
                    {
                      order_.push_back(next);
                      found_ |= next;
                    }
                }
              }
          }

        acc = temp;
        unsigned next = slevel;
        while (next < order_.size()
               && (acc & order_[next]) == order_[next])
          ++next;
        return next;
      }

      void
      print(int scc, const bdd_dict* dict)
      {
        std::vector<bdd>::iterator i;
        std::cout << "Order_" << scc << ":\t";
202
        for (i = order_.begin(); i != order_.end(); i++)
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
          {
            bdd_print_acc(std::cout, dict, *i);
            std::cout << ", ";
          }
        std::cout << std::endl;
      }
    };

    // Accepting order for each SCC
    class scc_orders
    {
      bdd all_;
      std::map<int, acc_order> orders_;

    public:
      scc_orders(bdd all): all_(all)
      {
      }

      unsigned
      next_level(int scc, int slevel, bdd acc)
      {
        return orders_[scc].next_level(all_, slevel, acc);
      }

      void
      print(const bdd_dict* dict)
      {
        std::map<int, acc_order>::iterator i;
        for (i = orders_.begin(); i != orders_.end(); i++)
          i->second.print(i->first, dict);
234
235
236
237
238
      }
    };
  }

  sba*
239
240
  degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
               bool use_lvl_cache)
241
  {
242
243
    bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;

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
    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)
272
273
274
275
276
        {
          bdd next = bdd_satone(all);
          all -= next;
          order.push_back(next);
        }
277
278
    }

279
280
281
    // Initialize scc_orders
    scc_orders orders(a->all_acceptance_conditions());

282
283
284
285
286
287
288
289
290
291
    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;

292
293
294
295
296
297
298
299
    // This map is used to find transitions that go to the same
    // destination with the same acceptance.  The integer key is
    // (dest*2+acc) where dest is the destination state number, and
    // acc is 1 iff the transition is accepting.  The source
    // is always that of the current iteration.
    typedef std::map<int, state_explicit_number::transition*> tr_cache_t;
    tr_cache_t tr_cache;

300
    // State level cache
301
302
303
    typedef std::map<const state*, int> lvl_cache_t;
    lvl_cache_t lvl_cache;

304
    // Compute SCCs in order to use any optimization.
305
    scc_map m(a);
306
    if (use_cust_acc_orders || use_lvl_cache || use_z_lvl)
307
308
      m.build_map();

309
310
311
312
313
314
315
316
317
318
319
    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())
320
321
322
323
324
325
326
327
328
329
330
331
332
        {
          // 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;
            }
        }
333
334
335
      delete it;
    }

336
337
338
339
#ifdef DEGEN_DEBUG
    std::map<const state*, int>names;
    names[s.first] = 1;

340
341
    ds2num[s] =
      10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first);
342
#else
343
    ds2num[s] = 0;
344
345
#endif

346
347
    todo.push_back(s);

348
349
    // If use_lvl_cache is on insert initial state to level cache
    // Level cache stores first encountered level for each state.
350
351
352
353
354
355
    // When entering an SCC first the lvl_cache is checked.
    // If such state exists level from chache is used.
    // If not, a new level (starting with 0) is computed.
    if (use_lvl_cache)
      lvl_cache[s.first] = s.second;

356
357
    while (!todo.empty())
      {
358
359
360
361
362
363
364
365
366
367
368
369
370
        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;

        // Check SCC for state s
        int s_scc = -1;
371
        if (use_scc)
372
373
374
375
376
377
378
379
380
381
382
383
384
385
          s_scc = m.scc_of_state(s.first);

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

#ifdef DEGEN_DEBUG
            if (names.find(d.first) == names.end())
              names[d.first] = uniq.size();
#endif

            // Check whether the target's SCC is accepting
            bool is_scc_acc = false;
386
387
            int scc = use_scc ? m.scc_of_state(i->current_state()) : -1;
            if (!use_scc || m.accepting(scc))
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
              is_scc_acc = true;

            // 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
418
                //    example was not clear, uncomment the following
419
420
421
422
423
424
425
426
427
428
429
430
                //    "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.
431
432
433
434
                if (!order.empty())
                  {
                    unsigned prev = order.size() - 1;
                    bdd common = outgoing.common_acc(s.first);
435
                    if (bdd_implies(order[prev], common))
436
437
                      {
                        bdd u = outgoing.union_acc(d.first);
438
                        if (!bdd_implies(order[prev], u))
439
440
441
                          acc -= order[prev];
                      }
                  }
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
              }
            // 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}
            // }
            if (is_scc_acc)
              {
                acc |= otheracc;
463
464
                // If use_z_lvl is on, start with level zero 0 when
                // swhitching SCCs
465
                unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0;
466

467
                // If lvl_cache is used and switching SCCs, use level from cache
468
                if (use_lvl_cache && s_scc != scc
469
		    && lvl_cache.find(d.first) != lvl_cache.end())
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
                  {
                    d.second = lvl_cache[d.first];
                  }
                else
                  {
                  // If using custom acc orders, get next level for this scc
                    if (use_cust_acc_orders)
                      d.second = orders.next_level(scc, next, acc);
                    // Else compute level according the global acc order
                    else
                      {
                        // Consider both the current acceptance sets, and the
                        // acceptance sets common to the outgoing transitions of
                        // the destination state.
                        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
              {
#ifdef DEGEN_DEBUG
503
                dest = 10000 * names[d.first] + 100 * d.second + scc;
504
505
506
507
508
#else
                dest = ds2num.size();
#endif
                ds2num[d] = dest;
                todo.push_back(d);
509
                // Insert new state to cache
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
                if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end())
                  lvl_cache[d.first] = d.second;
              }

            state_explicit_number::transition*& t =
              tr_cache[dest * 2 + is_acc];

            if (t == 0)
              {
                // Actually create the 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.)
526
527
		if (is_acc)
		  t->acceptance_conditions = degen_acc;
528
529
530
531
532
533
534
535
              }
            else
              {
                t->condition |= i->current_condition();
              }
          }
        delete i;
        tr_cache.clear();
536
      }
537
538
539
540

#ifdef DEGEN_DEBUG
        std::vector<bdd>::iterator i;
        std::cout << "Orig. order:  \t";
541
        for (i = order.begin(); i != order.end(); i++)
542
543
544
545
546
547
548
549
550
          {
            bdd_print_acc(std::cout, dict, *i);
            std::cout << ", ";
          }
        std::cout << std::endl;
        orders.print(dict);
#endif

    res->merge_transitions();
551
552
553
    return res;
  }
}