degen.cc 16.6 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
75
	bool has_acc_self_loop = false;
	for (auto& t: a_->out(s))
76
          {
77
	    // Ignore transitions that leave the SCC of s.
78
79
	    unsigned d = t.dst;
	    unsigned s2 = sm_ ? sm_->scc_of(d) : 0;
80
81
82
	    if (s2 != s1)
	      continue;

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

	    // an accepting self-loop?
	    has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
88
          }
89
        cache_[s] = std::make_tuple(common, union_, has_acc_self_loop);
90
      }
91

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

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

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

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

123
124
125
    // Order of accepting sets (for one SCC)
    class acc_order
    {
126
127
      std::vector<unsigned> order_;
      acc_cond::mark_t found_;
128
129
130

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

        unsigned next = slevel;
141
        while (next < order_.size() && set.has(order_[next]))
142
143
144
145
146
	  {
	    ++next;
	    if (!skip_levels)
	      break;
	  }
147
148
149
150
        return next;
      }

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

    // Accepting order for each SCC
    class scc_orders
    {
      std::map<int, acc_order> orders_;
164
      bool skip_levels_;
165
166

    public:
167
168
      scc_orders(bool skip_levels):
	skip_levels_(skip_levels)
169
170
171
172
      {
      }

      unsigned
173
      next_level(int scc, int slevel, acc_cond::mark_t set)
174
      {
175
        return orders_[scc].next_level(slevel, set, skip_levels_);
176
177
178
      }

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

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

197
198
      bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;

199
      bdd_dict_ptr dict = a->get_dict();
200
201

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

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

230
      // Initialize scc_orders
231
      scc_orders orders(skip_levels);
232
233
234
235
236
237
238
239
240
241
242
243

      // 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;

244
245
246
247
248
249
      // 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());
250
251

      // Compute SCCs in order to use any optimization.
252
      scc_info* m = nullptr;
253
      if (use_scc)
254
	m = new scc_info(a);
255
256

      // Cache for common outgoing acceptances.
257
      outgoing_acc outgoing(a, m);
258
259
260
261
262
263

      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.
264
      if (want_sba && outgoing.has_acc_selfloop(s.first))
265
266
267
268
269
270
	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)
	{
271
	  auto set = outgoing.common_acc(s.first);
272
	  if (use_cust_acc_orders)
273
	    s.second = orders.next_level(m->initial(), s.second, set);
274
	  else
275
276
	    while (s.second < order.size()
		   && set.has(order[s.second]))
277
	      {
278
279
280
		++s.second;
		if (!skip_levels)
		  break;
281
	      }
282
283
284
285
286
287
288
289
290
291
292
293
294
295
	  // 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)
296
	lvl_cache[s.first] = std::make_pair(s.second, true);
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313

      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)
314
	    s_scc = m->scc_of(s.first);
315

316
	  for (auto& i: a->out(s.first))
317
	    {
318
	      degen_state d(i.dst, 0);
319
320
321
322
323
324

	      // Check whether the target SCC is accepting
	      bool is_scc_acc;
	      int scc;
	      if (use_scc)
		{
325
326
		  scc = m->scc_of(d.first);
		  is_scc_acc = m->is_accepting_scc(scc);
327
328
329
330
331
332
333
334
335
336
		}
	      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?
337
	      auto acc = i.acc;
338
	      auto otheracc = outgoing.common_acc(d.first);
339
340
341
342

	      if (want_sba && is_acc)
		{
		  // Ignore the last expected acceptance set (the value of
343
		  // prev below) if it is common to all other outgoing
344
345
346
347
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
		  // 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;
379
380
		      auto common = outgoing.common_acc(s.first);
		      if (common.has(order[prev]))
381
			{
382
383
384
			  auto u = outgoing.union_acc(d.first);
			  if (!u.has(order[prev]))
			    acc -= a->acc().mark(order[prev]);
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
			}
		    }
		}
	      // 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
410
		      && lvl_cache[d.first].second)
411
		    {
412
		      d.second = lvl_cache[d.first].first;
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
		    }
		  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.
441
442
			  if (s_scc != scc
			      && outgoing.has_acc_selfloop(d.first))
443
444
445
446
447
448
449
450
451
452
453
454
455
			    {
			      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()
456
				       && acc.has(order[next]))
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
				  {
				    ++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.
478
		      if (!a->acc().accepting(acc) && !skip_levels)
479
480
481
482
483
484
485
486
			{
			  if (use_cust_acc_orders)
			    {
			      d.second = orders.next_level(scc, d.second, acc);
			    }
			  else
			    {
			      while (d.second < order.size() &&
487
				     acc.has(order[d.second]))
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
				++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)
		    {
510
511
		      auto lvl = d.second;
		      if (lvl_cache[d.first].second)
512
513
			{
			  if (use_lvl_cache == 3)
514
			    lvl = std::max(lvl_cache[d.first].first, lvl);
515
			  else if (use_lvl_cache == 2)
516
			    lvl = std::min(lvl_cache[d.first].first, lvl);
517
			}
518
		      lvl_cache[d.first] = std::make_pair(lvl, true);
519
520
521
522
523
		    }
		}

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

524
	      if (t == 0)	// Create transition.
525
		t = res->new_acc_transition(src, dest, i.cond, is_acc);
526
	      else		// Update existing transition.
527
		res->trans_data(t).cond |= i.cond;
528
529
530
	    }
	  tr_cache.clear();
	}
531
532

#ifdef DEGEN_DEBUG
533
      std::cout << "Orig. order:  \t";
534
      for (auto i: order)
535
	{
536
	  std::cout << i << ", ";
537
	}
538
539
      std::cout << '\n';
      orders.print();
540
541
#endif

542
543
      delete m;

544
545
546
547
548
      res->merge_transitions();
      return res;
    }
  }

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

559
560
561
562
    return degeneralize_aux<true>(a, use_z_lvl, use_cust_acc_orders,
				  use_lvl_cache, skip_levels);
  }

563
  tgba_digraph_ptr
564
  degeneralize_tba(const const_tgba_digraph_ptr& a,
565
		   bool use_z_lvl, bool use_cust_acc_orders,
566
567
		   int use_lvl_cache, bool skip_levels)
  {
568
569
    // If this already a degeneralized digraph, there is nothing we
    // can improve.
570
    if (a->has_single_acc_set())
571
      return std::const_pointer_cast<tgba_digraph>(a);
572

573
574
    return degeneralize_aux<false>(a, use_z_lvl, use_cust_acc_orders,
				   use_lvl_cache, skip_levels);
575
576
  }
}