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


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

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

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

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

    // Associate the degeneralized state to its number.
64
65
    typedef std::unordered_map<degen_state, int,
			       degen_state_hash, degen_state_equal> ds2num_map;
66
67
68
69

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

70
71
    // Acceptance set common to all outgoing transitions (of the same
    // SCC -- we do not care about the other) of some state.
72
73
74
    class outgoing_acc
    {
      const tgba* a_;
75
      typedef std::pair<bdd, bdd> cache_entry;
76
77
      typedef std::unordered_map<const state*, cache_entry,
				 state_ptr_hash, state_ptr_equal> cache_t;
78
      cache_t cache_;
79
      const scc_map* sm_;
80
81

    public:
82
      outgoing_acc(const tgba* a, const scc_map* sm): a_(a), sm_(sm)
83
84
85
      {
      }

86
      cache_t::const_iterator fill_cache(const state* s)
87
      {
88
	unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0;
89
90
        bdd common = a_->all_acceptance_conditions();
        bdd union_ = bddfalse;
91
	for (auto it: a_->succ(s))
92
          {
93
94
95
96
97
98
99
	    // Ignore transitions that leave the SCC of s.
	    const state* d = it->current_state();
	    unsigned s2 = sm_ ? sm_->scc_of_state(d) : 0;
	    d->destroy();
	    if (s2 != s1)
	      continue;

100
101
102
103
104
105
            bdd set = it->current_acceptance_conditions();
            common &= set;
            union_ |= set;
          }
        cache_entry e(common, union_);
        return cache_.insert(std::make_pair(s, e)).first;
106
      }
107

108
109
110
      // Intersection of all outgoing acceptance sets
      bdd common_acc(const state* s)
      {
111
112
113
114
        cache_t::const_iterator i = cache_.find(s);
        if (i == cache_.end())
          i = fill_cache(s);
        return i->second.first;
115
116
      }

117
      // Union of all outgoing acceptance sets
118
119
      bdd union_acc(const state* s)
      {
120
121
122
123
124
125
126
        cache_t::const_iterator i = cache_.find(s);
        if (i == cache_.end())
          i = fill_cache(s);
        return i->second.second;
      }
    };

127
128
129
130
131

    // Check whether a state has an accepting self-loop, with a catch.
    class has_acc_loop
    {
      const tgba* a_;
132
133
      typedef std::unordered_map<const state*, bool,
				 state_ptr_hash, state_ptr_equal> cache_t;
134
      cache_t cache_;
135
      state_unicity_table& uniq_;
136
137

    public:
138
      has_acc_loop(const tgba* a, state_unicity_table& uniq):
139
140
141
142
143
144
145
146
147
148
149
150
	a_(a),
	uniq_(uniq)
      {
      }

      bool check(const state* s)
      {
	std::pair<cache_t::iterator, bool> p =
	  cache_.insert(std::make_pair(s, false));
	if (p.second)
	  {
	    bdd all = a_->all_acceptance_conditions();
151
	    for (auto it: a_->succ(s))
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
	      {
		// 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 == s)
		  {
		    p.first->second = true;
		    break;
		  }
	      }
	  }
        return p.first->second;
      }
    };

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
    // 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;
202
        while (next < order_.size() && bdd_implies(order_[next], acc))
203
204
205
206
207
208
209
210
211
          ++next;
        return next;
      }

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

  sba*
249
250
  degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
               bool use_lvl_cache)
251
  {
252
253
    bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;

254
255
    bdd_dict* dict = a->get_dict();

256
    // The result (degeneralized) automaton uses numbered states.
257
    sba_explicit_number* res = new sba_explicit_number(dict);
258
259
260

    // We use the same BDD variables as the input, except for the
    // acceptance.
261
    dict->register_all_variables_of(a, res);
262
    dict->unregister_all_typed_variables(bdd_dict::acc, res);
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284

    // 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)
285
286
287
288
289
        {
          bdd next = bdd_satone(all);
          all -= next;
          order.push_back(next);
        }
290
291
    }

292
293
294
    // Initialize scc_orders
    scc_orders orders(a->all_acceptance_conditions());

295
296
    // Make sure we always use the same pointer for identical states
    // from the input automaton.
297
    state_unicity_table uniq;
298

299
300
301
    // Accepting loop checker, for some heuristics.
    has_acc_loop acc_loop(a, uniq);

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

306
307
308
309
310
311
312
313
    // 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;

314
    // State level cache
315
316
317
    typedef std::map<const state*, int> lvl_cache_t;
    lvl_cache_t lvl_cache;

318
    // Compute SCCs in order to use any optimization.
319
    scc_map m(a);
320
    if (use_scc)
321
322
      m.build_map();

323
324
325
    // Cache for common outgoing acceptances.
    outgoing_acc outgoing(a, use_scc ? &m : 0);

326
327
328
329
330
    queue_t todo;

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

331
332
    // As an heuristic, if the initial state at least one accepting
    // self-loop, start the degeneralization on the accepting level.
333
334
    if (acc_loop.check(s0))
      s.second = order.size();
335
336
337
338
339
340
341
342
343
344
345
346
    // Otherwise, check for acceptance conditions common to all
    // outgoing transitions, and assume we have already seen these and
    // start on the associated level.
    if (s.second == 0)
      {
	bdd acc = outgoing.common_acc(s.first);
	if (use_cust_acc_orders)
	  s.second = orders.next_level(m.initial(), s.second, acc);
	else
	  while (s.second < order.size() && bdd_implies(order[s.second], acc))
	    ++s.second;
      }
347

348
349
350
351
#ifdef DEGEN_DEBUG
    std::map<const state*, int>names;
    names[s.first] = 1;

352
353
    ds2num[s] =
      10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first);
354
#else
355
    ds2num[s] = 0;
356
357
#endif

358
359
    todo.push_back(s);

360
361
    // If use_lvl_cache is on insert initial state to level cache
    // Level cache stores first encountered level for each state.
362
363
364
365
366
367
    // 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;

368
369
    while (!todo.empty())
      {
370
371
372
373
374
375
376
377
378
379
380
381
382
        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;
383
        if (use_scc)
384
385
          s_scc = m.scc_of_state(s.first);

386
	for (auto i: a->succ(s.first))
387
388
389
390
391
392
393
          {
            degen_state d(uniq(i->current_state()), 0);

#ifdef DEGEN_DEBUG
            if (names.find(d.first) == names.end())
              names[d.first] = uniq.size();
#endif
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
            // Check whether the target SCC is accepting
            bool is_scc_acc;
            int scc;
	    if (use_scc)
	      {
		scc = m.scc_of_state(d.first);
		is_scc_acc = m.accepting(scc);
	      }
	    else
	      {
		// If we have no SCC information, treat all SCCs as
		// accepting.
		scc = -1;
		is_scc_acc = true;
	      }
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435

            // 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
436
                //    two copies of state 2, depending on whether we
437
                //    reach it using 1=>2 or from 2->2.  If this
438
                //    example was not clear, uncomment the following
439
440
441
442
443
444
445
446
447
448
449
450
                //    "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.
451
452
453
454
                if (!order.empty())
                  {
                    unsigned prev = order.size() - 1;
                    bdd common = outgoing.common_acc(s.first);
455
                    if (bdd_implies(order[prev], common))
456
457
                      {
                        bdd u = outgoing.union_acc(d.first);
458
                        if (!bdd_implies(order[prev], u))
459
460
461
                          acc -= order[prev];
                      }
                  }
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
              }
            // 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)
              {
482
                // If lvl_cache is used and switching SCCs, use level from cache
483
                if (use_lvl_cache && s_scc != scc
484
		    && lvl_cache.find(d.first) != lvl_cache.end())
485
486
487
488
489
                  {
                    d.second = lvl_cache[d.first];
                  }
                else
                  {
490
491
492
493
494
495
496
497
498
499
500
501
		    // Complete (or replace) the acceptance sets of
		    // this link with the acceptance sets common to
		    // all transitions leaving the destination state.
		    if (s_scc == scc)
		      acc |= otheracc;
		    else
		      acc = otheracc;

		    // If use_z_lvl is on, start with level zero 0 when
		    // swhitching SCCs
		    unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0;

502
		    // If using custom acc orders, get next level for this scc
503
                    if (use_cust_acc_orders)
504
505
506
		      {
			d.second = orders.next_level(scc, next, acc);
		      }
507
508
509
                    // Else compute level according the global acc order
                    else
                      {
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
			// As a heuristic, if we enter the SCC on a
			// state that has at least one accepting
			// self-loop, start the degeneralization on
			// the accepting level.
			if (s_scc != scc && acc_loop.check(d.first))
			  {
			    d.second = order.size();
			  }
			else
			  {
			    // Consider both the current acceptance
			    // sets, and the acceptance sets common to
			    // the outgoing transitions of the
			    // destination state.
			    while (next < order.size()
				   && bdd_implies(order[next], acc))
			      ++next;
			    d.second = next;
			  }
529
530
531
532
533
534
535
536
537
538
539
540
541
542
                      }
                  }
              }

            // 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
543
                dest = 10000 * names[d.first] + 100 * d.second + scc;
544
545
546
547
548
#else
                dest = ds2num.size();
#endif
                ds2num[d] = dest;
                todo.push_back(d);
549
                // Insert new state to cache
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
                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.)
566
567
		if (is_acc)
		  t->acceptance_conditions = degen_acc;
568
569
570
571
572
573
574
              }
            else
              {
                t->condition |= i->current_condition();
              }
          }
        tr_cache.clear();
575
      }
576
577
578
579

#ifdef DEGEN_DEBUG
        std::vector<bdd>::iterator i;
        std::cout << "Orig. order:  \t";
580
        for (i = order.begin(); i != order.end(); i++)
581
582
583
584
585
586
587
588
589
          {
            bdd_print_acc(std::cout, dict, *i);
            std::cout << ", ";
          }
        std::cout << std::endl;
        orders.print(dict);
#endif

    res->merge_transitions();
590
591
592
    return res;
  }
}