degen.cc 16.8 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// 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


#include "degen.hh"
22
#include "tgba/tgbagraph.hh"
23
24
25
26
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include <deque>
#include <vector>
27
#include <algorithm>
28
#include <iterator>
29
#include "tgbaalgos/sccinfo.hh"
30
31
32
#include "tgba/bddprint.hh"

//#define DEGEN_DEBUG
33
34
35
36
37
38
39
40

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.
41
    typedef std::pair<unsigned, unsigned> degen_state;
42
43
44
45
46
47

    struct degen_state_hash
    {
      size_t
      operator()(const degen_state& s) const
      {
48
        return wang32_hash(s.first ^ wang32_hash(s.second));
49
50
51
52
      }
    };

    // Associate the degeneralized state to its number.
53
    typedef std::unordered_map<degen_state, int, degen_state_hash> ds2num_map;
54
55
56
57

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

58
59
    // Acceptance set common to all outgoing transitions (of the same
    // SCC -- we do not care about the other) of some state.
60
61
    class outgoing_acc
    {
62
63
64
65
66
67
68
69
      const_tgba_digraph_ptr a_;
      typedef std::tuple<acc_cond::mark_t,
			 acc_cond::mark_t,
			 bool> cache_entry;
      std::vector<cache_entry> cache_;
      const scc_info* sm_;

      void fill_cache(unsigned s)
70
      {
71
	unsigned s1 = sm_ ? sm_->scc_of(s) : 0;
72
73
	acc_cond::mark_t common = a_->acc().all_sets();
        acc_cond::mark_t union_ = 0U;
74
	bool has_acc_self_loop = false;
75
	bool seen = false;
76
	for (auto& t: a_->out(s))
77
          {
78
	    // Ignore transitions that leave the SCC of s.
79
80
	    unsigned d = t.dst;
	    unsigned s2 = sm_ ? sm_->scc_of(d) : 0;
81
82
83
	    if (s2 != s1)
	      continue;

84
85
86
87
88
            common &= t.acc;
            union_ |= t.acc;

	    // an accepting self-loop?
	    has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
89
	    seen = true;
90
          }
91
92
	if (!seen)
	  common = 0U;
93
        cache_[s] = std::make_tuple(common, union_, has_acc_self_loop);
94
      }
95

96
97
98
    public:
      outgoing_acc(const const_tgba_digraph_ptr& a, const scc_info* sm):
	a_(a), cache_(a->num_states()), sm_(sm)
99
      {
100
101
102
	unsigned n = a->num_states();
	for (unsigned s = 0; s < n; ++s)
	  fill_cache(s);
103
104
      }

105
106
      // Intersection of all outgoing acceptance sets
      acc_cond::mark_t common_acc(unsigned s)
107
      {
108
109
	assert(s < cache_.size());
	return std::get<0>(cache_[s]);
110
111
      }

112
113
      // Union of all outgoing acceptance sets
      acc_cond::mark_t union_acc(unsigned s)
114
      {
115
116
	assert(s < cache_.size());
	return std::get<1>(cache_[s]);
117
118
      }

119
120
      // Has an accepting self-loop
      bool has_acc_selfloop(unsigned s)
121
      {
122
123
	assert(s < cache_.size());
	return std::get<2>(cache_[s]);
124
125
126
      }
    };

127
128
129
    // Order of accepting sets (for one SCC)
    class acc_order
    {
130
131
      std::vector<unsigned> order_;
      acc_cond::mark_t found_;
132
133
134

    public:
      unsigned
135
      next_level(int slevel, acc_cond::mark_t set, bool skip_levels)
136
      {
137
138
139
	// Update the order with any new set we discover
	if (auto newsets = set - found_)
	  {
140
	    newsets.fill(std::back_inserter(order_));
141
142
	    found_ |= newsets;
	  }
143
144

        unsigned next = slevel;
145
        while (next < order_.size() && set.has(order_[next]))
146
147
148
149
150
	  {
	    ++next;
	    if (!skip_levels)
	      break;
	  }
151
152
153
154
        return next;
      }

      void
155
      print(int scc)
156
157
      {
        std::cout << "Order_" << scc << ":\t";
158
159
160
        for (auto i: order_)
	  std::cout << i << ", ";
        std::cout << '\n';
161
162
163
164
165
166
167
      }
    };

    // Accepting order for each SCC
    class scc_orders
    {
      std::map<int, acc_order> orders_;
168
      bool skip_levels_;
169
170

    public:
171
172
      scc_orders(bool skip_levels):
	skip_levels_(skip_levels)
173
174
175
176
      {
      }

      unsigned
177
      next_level(int scc, int slevel, acc_cond::mark_t set)
178
      {
179
        return orders_[scc].next_level(slevel, set, skip_levels_);
180
181
182
      }

      void
183
      print()
184
185
186
      {
        std::map<int, acc_order>::iterator i;
        for (i = orders_.begin(); i != orders_.end(); i++)
187
          i->second.print(i->first);
188
189
190
      }
    };

191
    template<bool want_sba>
192
    tgba_digraph_ptr
193
    degeneralize_aux(const const_tgba_digraph_ptr& a, bool use_z_lvl,
194
		     bool use_cust_acc_orders, int use_lvl_cache,
195
		     bool skip_levels, bool ignaccsl)
196
    {
197
198
199
200
      if (!a->acc().is_generalized_buchi())
	throw std::runtime_error
	  ("degeneralize() can only work with generalized Büchi acceptance");

201
202
      bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;

203
      bdd_dict_ptr dict = a->get_dict();
204
205

      // The result automaton is an SBA.
206
      auto res = make_tgba_digraph(dict);
207
      res->copy_ap_of(a);
208
      res->set_buchi();
209
      if (want_sba)
210
	res->prop_state_based_acc();
211
      // Preserve determinism, weakness, and stutter-invariance
212
      res->prop_copy(a, { false, true, true, true });
213
214
215
216
217
218

      // 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.
219
      std::vector<unsigned> order;
220
      {
221
222
	// FIXME: revisit this comment once everything compiles again.
	//
223
224
225
226
227
228
	// 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.)
229
230
231
	unsigned n = a->acc().num_sets();
	for (unsigned i = n; i > 0; --i)
	  order.push_back(i - 1);
232
      }
233

234
      // Initialize scc_orders
235
      scc_orders orders(skip_levels);
236
237
238
239
240
241
242
243
244
245
246
247

      // and vice-versa.
      ds2num_map ds2num;

      // 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, unsigned> tr_cache_t;
      tr_cache_t tr_cache;

248
249
250
251
252
253
      // Read this early, because it might create a state if the
      // automaton is empty.
      degen_state s(a->get_init_state_number(), 0);

      // State->level cache
      std::vector<std::pair<unsigned, bool>> lvl_cache(a->num_states());
254
255

      // Compute SCCs in order to use any optimization.
256
      scc_info* m = nullptr;
257
      if (use_scc)
258
	m = new scc_info(a);
259
260

      // Cache for common outgoing acceptances.
261
      outgoing_acc outgoing(a, m);
262
263
264
265
266
267

      queue_t todo;

      // As a heuristic for building SBA, if the initial state has at
      // least one accepting self-loop, start the degeneralization on
      // the accepting level.
268
      if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first))
269
270
271
272
273
274
	s.second = order.size();
      // 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)
	{
275
	  auto set = outgoing.common_acc(s.first);
276
	  if (use_cust_acc_orders)
277
	    s.second = orders.next_level(m->initial(), s.second, set);
278
	  else
279
280
	    while (s.second < order.size()
		   && set.has(order[s.second]))
281
	      {
282
283
284
		++s.second;
		if (!skip_levels)
		  break;
285
	      }
286
287
288
289
290
291
292
293
294
295
296
297
298
299
	  // There is not accepting level for TBA, let reuse level 0.
	  if (!want_sba && s.second == order.size())
	    s.second = 0;
	}

      ds2num[s] = res->new_state();
      todo.push_back(s);

      // If use_lvl_cache is on insert initial state to level cache
      // Level cache stores first encountered level for each state.
      // 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)
300
	lvl_cache[s.first] = std::make_pair(s.second, true);
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317

      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 (want_sba && is_acc)
	    slevel = 0;

	  // Check SCC for state s
	  int s_scc = -1;
	  if (use_scc)
318
	    s_scc = m->scc_of(s.first);
319

320
	  for (auto& i: a->out(s.first))
321
	    {
322
	      degen_state d(i.dst, 0);
323
324
325
326
327
328

	      // Check whether the target SCC is accepting
	      bool is_scc_acc;
	      int scc;
	      if (use_scc)
		{
329
330
		  scc = m->scc_of(d.first);
		  is_scc_acc = m->is_accepting_scc(scc);
331
332
333
334
335
336
337
338
339
340
		}
	      else
		{
		  // If we have no SCC information, treat all SCCs as
		  // accepting.
		  scc = -1;
		  is_scc_acc = true;
		}

	      // The old level is slevel.  What should be the new one?
341
	      auto acc = i.acc;
342
	      auto otheracc = outgoing.common_acc(d.first);
343
344
345
346

	      if (want_sba && is_acc)
		{
		  // Ignore the last expected acceptance set (the value of
347
		  // prev below) if it is common to all other outgoing
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
		  // 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 state
		  //    2, depending on whether we reach it using 1=>2
		  //    or from 2->2.  If this example was not clear,
		  //    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;
383
384
		      auto common = outgoing.common_acc(s.first);
		      if (common.has(order[prev]))
385
			{
386
387
388
			  auto u = outgoing.union_acc(d.first);
			  if (!u.has(order[prev]))
			    acc -= a->acc().mark(order[prev]);
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
			}
		    }
		}
	      // 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)
		{
		  // If lvl_cache is used and switching SCCs, use level
		  // from cache
		  if (use_lvl_cache && s_scc != scc
414
		      && lvl_cache[d.first].second)
415
		    {
416
		      d.second = lvl_cache[d.first].first;
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
		    }
		  else
		    {
		      // 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;

		      // 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
			{
			  // 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.
445
			  if (s_scc != scc
446
			      && !ignaccsl
447
			      && outgoing.has_acc_selfloop(d.first))
448
449
450
451
452
453
454
455
456
457
458
459
460
			    {
			      d.second = order.size();
			    }
			  else
			    {
			      // Consider both the current acceptance
			      // sets, and the acceptance sets common to
			      // the outgoing transitions of the
			      // destination state.  But don't do
			      // that if the state is accepting and we
			      // are not skipping levels.
			      if (skip_levels || !is_acc)
				while (next < order.size()
461
				       && acc.has(order[next]))
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
				  {
				    ++next;
				    if (!skip_levels)
				      break;
				  }
			      d.second = next;
			    }
			}
		    }
		}

	      // In case we are building a TBA is_acc has to be
	      // set differently for each transition, and
	      // we do not need to stay use final level.
	      if (!want_sba)
		{
		  is_acc = d.second == order.size();
		  if (is_acc)	// The transition is accepting
		    {
		      d.second = 0; // Make it go to the first level.
		      // Skip levels as much as possible.
483
		      if (!a->acc().accepting(acc) && !skip_levels)
484
485
486
487
488
489
490
491
			{
			  if (use_cust_acc_orders)
			    {
			      d.second = orders.next_level(scc, d.second, acc);
			    }
			  else
			    {
			      while (d.second < order.size() &&
492
				     acc.has(order[d.second]))
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
				++d.second;
			    }
			}
		    }
		}

	      // 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 = res->new_state();
		  ds2num[d] = dest;
		  todo.push_back(d);
		  // Insert new state to cache

		  if (use_lvl_cache)
		    {
515
516
		      auto lvl = d.second;
		      if (lvl_cache[d.first].second)
517
518
			{
			  if (use_lvl_cache == 3)
519
			    lvl = std::max(lvl_cache[d.first].first, lvl);
520
			  else if (use_lvl_cache == 2)
521
			    lvl = std::min(lvl_cache[d.first].first, lvl);
522
			}
523
		      lvl_cache[d.first] = std::make_pair(lvl, true);
524
525
526
527
528
		    }
		}

	      unsigned& t = tr_cache[dest * 2 + is_acc];

529
	      if (t == 0)	// Create transition.
530
		t = res->new_acc_transition(src, dest, i.cond, is_acc);
531
	      else		// Update existing transition.
532
		res->trans_data(t).cond |= i.cond;
533
534
535
	    }
	  tr_cache.clear();
	}
536
537

#ifdef DEGEN_DEBUG
538
      std::cout << "Orig. order:  \t";
539
      for (auto i: order)
540
	{
541
	  std::cout << i << ", ";
542
	}
543
544
      std::cout << '\n';
      orders.print();
545
546
#endif

547
548
      delete m;

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

554
  tgba_digraph_ptr
555
  degeneralize(const const_tgba_digraph_ptr& a,
556
	       bool use_z_lvl, bool use_cust_acc_orders,
557
               int use_lvl_cache, bool skip_levels, bool ignaccsl)
558
  {
559
560
    // If this already a degeneralized digraph, there is nothing we
    // can improve.
561
    if (a->is_sba())
562
      return std::const_pointer_cast<tgba_digraph>(a);
563

564
    return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
565
				  use_lvl_cache, skip_levels, ignaccsl);
566
567
  }

568
  tgba_digraph_ptr
569
  degeneralize_tba(const const_tgba_digraph_ptr& a,
570
		   bool use_z_lvl, bool use_cust_acc_orders,
571
		   int use_lvl_cache, bool skip_levels, bool ignaccsl)
572
  {
573
574
    // If this already a degeneralized digraph, there is nothing we
    // can improve.
575
    if (a->acc().is_buchi())
576
      return std::const_pointer_cast<tgba_digraph>(a);
577

578
    return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
579
				   use_lvl_cache, skip_levels, ignaccsl);
580
581
  }
}