minimize.cc 18.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
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
28

//#define TRACE

#ifdef TRACE
#  define trace std::cerr
#else
#  define trace while (0) std::cerr
#endif

29
#include <queue>
30
31
32
#include <deque>
#include <set>
#include <list>
33
#include <vector>
34
#include <sstream>
35
36
37
38
39
40
41
42
43
44
45
46
47
48
#include <spot/twaalgos/minimize.hh>
#include <spot/misc/hash.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/remfin.hh>
49
50
51

namespace spot
{
52
53
  // FIXME: do we really want to use unordered_set instead of set here?
  // This calls for benchmarking.
54
55
56
57
  typedef std::unordered_set<const state*,
			     state_ptr_hash, state_ptr_equal> hash_set;
  typedef std::unordered_map<const state*, unsigned,
			     state_ptr_hash, state_ptr_equal> hash_map;
58

59
60
61
  namespace
  {
    static std::ostream&
62
    dump_hash_set(const hash_set* hs,
63
		  const const_twa_ptr& aut,
64
		  std::ostream& out)
65
    {
66
      out << '{';
67
68
69
70
71
72
      const char* sep = "";
      for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i)
	{
	  out << sep << aut->format_state(*i);
	  sep = ", ";
	}
73
      out << '}';
74
75
76
77
      return out;
    }

    static std::string
78
    format_hash_set(const hash_set* hs, const_twa_ptr aut)
79
80
81
82
83
84
    {
      std::ostringstream s;
      dump_hash_set(hs, aut, s);
      return s.str();
    }

85
86
87
88
89
90
91
92
93
94
95
96
97
    // Find all states of an automaton.
    static void
    build_state_set(const const_twa_ptr& a, hash_set* seen)
    {
      std::queue<const state*> tovisit;
      // Perform breadth-first traversal.
      const state* init = a->get_init_state();
      tovisit.push(init);
      seen->insert(init);
      while (!tovisit.empty())
	{
	  const state* src = tovisit.front();
	  tovisit.pop();
98

99
100
	  for (auto sit: a->succ(src))
	    {
101
	      const state* dst = sit->dst();
102
103
104
105
106
107
108
109
110
111
112
113
	      // Is it a new state ?
	      if (seen->find(dst) == seen->end())
		{
		  // Register the successor for later processing.
		  tovisit.push(dst);
		  seen->insert(dst);
		}
	      else
		dst->destroy();
	    }
	}
    }
114

115
116
117
118
119
120
121
122
123
124
    // From the base automaton and the list of sets, build the minimal
    // resulting automaton
    static twa_graph_ptr
    build_result(const const_twa_ptr& a,
		 std::list<hash_set*>& sets,
		 hash_set* final)
    {
      auto dict = a->get_dict();
      auto res = make_twa_graph(dict);
      res->copy_ap_of(a);
125
      res->prop_state_acc(true);
126
127
128
129
130
131
132
133
134
135
136
137
138
139

      // For each set, create a state in the resulting automaton.
      // For a state s, state_num[s] is the number of the state in the minimal
      // automaton.
      hash_map state_num;
      std::list<hash_set*>::iterator sit;
      for (sit = sets.begin(); sit != sets.end(); ++sit)
	{
	  hash_set::iterator hit;
	  hash_set* h = *sit;
	  unsigned num = res->new_state();
	  for (hit = h->begin(); hit != h->end(); ++hit)
	    state_num[*hit] = num;
	}
140

141
142
      // For each transition in the initial automaton, add the corresponding
      // transition in res.
143

144
145
      if (!final->empty())
	res->set_buchi();
146

147
148
149
      for (sit = sets.begin(); sit != sets.end(); ++sit)
	{
	  hash_set* h = *sit;
150

151
152
153
154
155
156
157
158
	  // Pick one state.
	  const state* src = *h->begin();
	  unsigned src_num = state_num[src];
	  bool accepting = (final->find(src) != final->end());

	  // Connect it to all destinations.
	  for (auto succit: a->succ(src))
	    {
159
	      const state* dst = succit->dst();
160
161
162
163
164
	      hash_map::const_iterator i = state_num.find(dst);
	      dst->destroy();
	      if (i == state_num.end()) // Ignore useless destinations.
		continue;
	      res->new_acc_edge(src_num, i->second,
165
				succit->cond(), accepting);
166
167
168
169
170
171
172
173
174
175
176
177
	    }
	}
      res->merge_edges();
      if (res->num_states() > 0)
	{
	  const state* init_state = a->get_init_state();
	  unsigned init_num = state_num[init_state];
	  init_state->destroy();
	  res->set_init_state(init_num);
	}
      return res;
    }
178
179
180

    struct wdba_search_acc_loop : public bfs_steps
    {
181
      wdba_search_acc_loop(const const_twa_ptr& det_a,
182
			   unsigned scc_n, scc_info& sm,
183
184
185
			   power_map& pm, const state* dest)
	: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
      {
186
	seen(dest);
187
188
189
190
191
      }

      virtual const state*
      filter(const state* s)
      {
192
	s = seen(s);
193
	if (sm.scc_of(std::static_pointer_cast<const twa_graph>(a_)
194
		      ->state_number(s)) != scc_n)
195
	  return nullptr;
196
197
198
199
	return s;
      }

      virtual bool
200
      match(twa_run::step&, const state* to)
201
202
203
204
205
      {
	return to == dest;
      }

      unsigned scc_n;
206
      scc_info& sm;
207
208
      power_map& pm;
      const state* dest;
209
      state_unicity_table seen;
210
211
212
213
    };


    bool
214
215
    wdba_scc_is_accepting(const const_twa_graph_ptr& det_a, unsigned scc_n,
			  const const_twa_graph_ptr& orig_a, scc_info& sm,
216
			  power_map& pm)
217
218
    {
      // Get some state from the SCC #n.
219
      const state* start = det_a->state_from_number(sm.one_state_of(scc_n));
220
221
222

      // Find a loop around START in SCC #n.
      wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start);
223
      twa_run::steps loop;
224
225
226
227
228
      const state* reached = wsal.search(start, loop);
      assert(reached == start);
      (void)reached;

      // Build an automaton representing this loop.
229
      auto loop_a = make_twa_graph(det_a->get_dict());
230
      twa_run::steps::const_iterator i;
231
      int loop_size = loop.size();
232
      loop_a->new_states(loop_size);
233
234
235
      int n;
      for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
	{
236
	  loop_a->new_edge(n - 1, n, i->label);
237
	  i->s->destroy();
238
239
	}
      assert(i != loop.end());
240
      loop_a->new_edge(n - 1, 0, i->label);
241
      i->s->destroy();
242
243
      assert(++i == loop.end());

244
      loop_a->set_init_state(0U);
245
246
247
248
249

      // Check if the loop is accepting in the original automaton.
      bool accepting = false;

      // Iterate on each original state corresponding to start.
250
251
      const power_map::power_state& ps =
	pm.states_of(det_a->state_number(start));
252
      for (auto& s: ps)
253
	{
254
	  // Construct a product between LOOP_A and ORIG_A starting in
255
256
	  // S.  FIXME: This could be sped up a lot!
	  if (!product(loop_a, orig_a, 0U, s)->is_empty())
257
258
259
260
	    {
	      accepting = true;
	      break;
	    }
261
262
263
264
265
	}

      return accepting;
    }

266
267
268
269
270
271
    static twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a,
				      hash_set* final, hash_set* non_final)
    {
      typedef std::list<hash_set*> partition_t;
      partition_t cur_run;
      partition_t next_run;
272

273
274
      // The list of equivalent states.
      partition_t done;
275

276
      hash_map state_set_map;
277

278
279
280
281
282
283
      // Size of det_a
      unsigned size = final->size() + non_final->size();
      // Use bdd variables to number sets.  set_num is the first variable
      // available.
      unsigned set_num =
	det_a->get_dict()->register_anonymous_variables(size, det_a);
284

285
286
287
288
      std::set<int> free_var;
      for (unsigned i = set_num; i < set_num + size; ++i)
	free_var.insert(i);
      std::map<int, int> used_var;
289

290
      hash_set* final_copy;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
291

292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
      if (!final->empty())
	{
	  unsigned s = final->size();
	  used_var[set_num] = s;
	  free_var.erase(set_num);
	  if (s > 1)
	    cur_run.push_back(final);
	  else
	    done.push_back(final);
	  for (hash_set::const_iterator i = final->begin();
	       i != final->end(); ++i)
	    state_set_map[*i] = set_num;

	  final_copy = new hash_set(*final);
	}
      else
	{
	  final_copy = final;
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
311

312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
      if (!non_final->empty())
	{
	  unsigned s = non_final->size();
	  unsigned num = set_num + 1;
	  used_var[num] = s;
	  free_var.erase(num);
	  if (s > 1)
	    cur_run.push_back(non_final);
	  else
	    done.push_back(non_final);
	  for (hash_set::const_iterator i = non_final->begin();
	       i != non_final->end(); ++i)
	    state_set_map[*i] = num;
	}
      else
	{
	  delete non_final;
	}
330

331
332
333
      // A bdd_states_map is a list of formulae (in a BDD form)
      // associated with a destination set of states.
      typedef std::map<bdd, hash_set*, bdd_less_than> bdd_states_map;
334

335
      bool did_split = true;
336

337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
      while (did_split)
	{
	  did_split = false;
	  while (!cur_run.empty())
	    {
	      // Get a set to process.
	      hash_set* cur = cur_run.front();
	      cur_run.pop_front();

	      trace << "processing " << format_hash_set(cur, det_a)
		    << std::endl;

	      hash_set::iterator hi;
	      bdd_states_map bdd_map;
	      for (hi = cur->begin(); hi != cur->end(); ++hi)
		{
		  const state* src = *hi;
		  bdd f = bddfalse;
		  for (auto si: det_a->succ(src))
		    {
357
		      const state* dst = si->dst();
358
359
360
361
362
363
364
365
366
367
		      hash_map::const_iterator i = state_set_map.find(dst);
		      dst->destroy();
		      if (i == state_set_map.end())
			// The destination state is not in our
			// partition.  This can happen if the initial
			// FINAL and NON_FINAL supplied to the algorithm
			// do not cover the whole automaton (because we
			// want to ignore some useless states).  Simply
			// ignore these states here.
			continue;
368
		      f |= (bdd_ithvar(i->second) & si->cond());
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
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
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
436
437
438
439
440
441
442
443
		    }

		  // Have we already seen this formula ?
		  bdd_states_map::iterator bsi = bdd_map.find(f);
		  if (bsi == bdd_map.end())
		    {
		      // No, create a new set.
		      hash_set* new_set = new hash_set;
		      new_set->insert(src);
		      bdd_map[f] = new_set;
		    }
		  else
		    {
		      // Yes, add the current state to the set.
		      bsi->second->insert(src);
		    }
		}

	      bdd_states_map::iterator bsi = bdd_map.begin();
	      if (bdd_map.size() == 1)
		{
		  // The set was not split.
		  trace << "set " << format_hash_set(bsi->second, det_a)
			<< " was not split" << std::endl;
		  next_run.push_back(bsi->second);
		}
	      else
		{
		  did_split = true;
		  for (; bsi != bdd_map.end(); ++bsi)
		    {
		      hash_set* set = bsi->second;
		      // Free the number associated to these states.
		      unsigned num = state_set_map[*set->begin()];
		      assert(used_var.find(num) != used_var.end());
		      unsigned left = (used_var[num] -= set->size());
		      // Make sure LEFT does not become negative (hence bigger
		      // than SIZE when read as unsigned)
		      assert(left < size);
		      if (left == 0)
			{
			  used_var.erase(num);
			  free_var.insert(num);
			}
		      // Pick a free number
		      assert(!free_var.empty());
		      num = *free_var.begin();
		      free_var.erase(free_var.begin());
		      used_var[num] = set->size();
		      for (hash_set::iterator hit = set->begin();
			   hit != set->end(); ++hit)
			state_set_map[*hit] = num;
		      // Trivial sets can't be splitted any further.
		      if (set->size() == 1)
			{
			  trace << "set " << format_hash_set(set, det_a)
				<< " is minimal" << std::endl;
			  done.push_back(set);
			}
		      else
			{
			  trace << "set " << format_hash_set(set, det_a)
				<< " should be processed further" << std::endl;
			  next_run.push_back(set);
			}
		    }
		}
	      delete cur;
	    }
	  if (did_split)
	    trace << "splitting did occur during this pass." << std::endl;
	  else
	    trace << "splitting did not occur during this pass." << std::endl;
	  std::swap(cur_run, next_run);
	}
444

445
      done.splice(done.end(), cur_run);
446
447

#ifdef TRACE
448
449
450
451
      trace << "Final partition: ";
      for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
	trace << format_hash_set(*i, det_a) << ' ';
      trace << std::endl;
452
#endif
Felix Abecassis's avatar
Felix Abecassis committed
453

454
455
      // Build the result.
      auto res = build_result(det_a, done, final_copy);
Felix Abecassis's avatar
Felix Abecassis committed
456

457
458
459
460
461
462
463
464
465
466
467
      // Free all the allocated memory.
      delete final_copy;
      hash_map::iterator hit;
      for (hit = state_set_map.begin(); hit != state_set_map.end();)
	{
	  hash_map::iterator old = hit++;
	  old->first->destroy();
	}
      std::list<hash_set*>::iterator it;
      for (it = done.begin(); it != done.end(); ++it)
	delete *it;
Felix Abecassis's avatar
Felix Abecassis committed
468

469
470
      return res;
    }
471
  }
472

473
  twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a)
474
475
  {
    hash_set* final = new hash_set;
476
    hash_set* non_final = new hash_set;
477
    twa_graph_ptr det_a = tgba_powerset(a);
478
479

    // non_final contain all states.
480
    // final is empty: there is no acceptance condition
481
    build_state_set(det_a, non_final);
482
    auto res = minimize_dfa(det_a, final, non_final);
483
    res->prop_copy(a, { false, false, false, true });
484
    res->prop_deterministic(true);
485
    res->prop_weak(true);
486
    res->prop_state_acc(true);
487
    return res;
488
489
  }

490
  twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a)
491
492
  {
    hash_set* final = new hash_set;
493
494
    hash_set* non_final = new hash_set;

495
    twa_graph_ptr det_a;
496
497
498
499
500

    {
      power_map pm;
      det_a = tgba_powerset(a, pm);

501
502
503
504
505
      // For each SCC of the deterministic automaton, determine if it
      // is accepting or not.

      // This corresponds to the algorithm in Fig. 1 of "Efficient
      // minimization of deterministic weak omega-automata" written by
506
      // Christof Löding and published in Information Processing
507
508
509
510
511
      // Letters 79 (2001) pp 105--109.

      // We also keep track of whether an SCC is useless
      // (i.e., it is not the start of any accepting word).

512
      scc_info sm(det_a);
513
      sm.determine_unknown_acceptance();
514
      unsigned scc_count = sm.scc_count();
515
516
      // SCC that have been marked as useless.
      std::vector<bool> useless(scc_count);
517
518
519
520
521
522
523
      // The "color".  Even number correspond to
      // accepting SCCs.
      std::vector<unsigned> d(scc_count);

      // An even number larger than scc_count.
      unsigned k = (scc_count | 1) + 1;

524
      // SCC are numbered in topological order
525
      // (but in the reverse order as Löding's)
526
      for (unsigned m = 0; m < scc_count; ++m)
527
	{
528
	  bool is_useless = true;
529
530
	  bool transient = sm.is_trivial(m);
	  auto& succ = sm.succ(m);
531

532
	  if (transient && succ.empty())
533
	    {
534
535
536
537
538
539
540
541
542
543
	      // A trivial SCC without successor is useless.
	      useless[m] = true;
	      d[m] = k - 1;
	      continue;
	    }

	  // Compute the minimum color l of the successors.
	  // Also SCCs are useless if all their successor are
	  // useless.
	  unsigned l = k;
544
	  for (unsigned j: succ)
545
	    {
546
547
	      is_useless &= useless[j];
	      unsigned dj = d[j];
548
549
550
551
552
553
554
	      if (dj < l)
		l = dj;
	    }

	  if (transient)
	    {
	      d[m] = l;
555
556
557
558
	    }
	  else
	    {
	      // Regular SCCs are accepting if any of their loop
559
560
	      // corresponds to an accepted word in the original
	      // automaton.
561
	      if (wdba_scc_is_accepting(det_a, m, a, sm, pm))
562
563
		{
		  is_useless = false;
564
		  d[m] = l & ~1; // largest even number inferior or equal
565
566
567
		}
	      else
		{
568
		  d[m] = (l - 1) | 1; // largest odd number inferior or equal
569
		}
570
	    }
571

572
	  useless[m] = is_useless;
573

574
575
	  if (!is_useless)
	    {
576
	      hash_set* dest_set = (d[m] & 1) ? non_final : final;
577
578
	      for (auto s: sm.states_of(m))
		dest_set->insert(det_a->state_from_number(s));
579
	    }
580
581
582
	}
    }

583
    auto res = minimize_dfa(det_a, final, non_final);
584
    res->prop_copy(a, { false, false, false, true });
585
    res->prop_deterministic(true);
586
    res->prop_weak(true);
587
588
589
590
591
592
    // If the input was terminal, then the output is also terminal.
    // FIXME:
    // (1) We should have a specialized version of this function for
    // the case where the input is terminal.  See issue #120.
    // (2) It would be nice to have a more precise detection of
    // terminal automata in the output.  Calling
593
    // is_terminal_automaton() seems overkill here.  But maybe we can
594
595
596
    // add a quick check inside minimize_dfa.
    if (a->prop_terminal())
      res->prop_terminal(true);
597
    return res;
598
599
  }

600
601
  twa_graph_ptr
  minimize_obligation(const const_twa_graph_ptr& aut_f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
602
		      formula f,
603
		      const_twa_graph_ptr aut_neg_f,
604
		      bool reject_bigger)
605
  {
606
    auto min_aut_f = minimize_wdba(aut_f);
607

608
609
610
    if (reject_bigger)
      {
	// Abort if min_aut_f has more states than aut_f.
611
	unsigned orig_states = aut_f->num_states();
612
	if (orig_states < min_aut_f->num_states())
613
	  return std::const_pointer_cast<twa_graph>(aut_f);
614
615
      }

616
617
    // If the input automaton was already weak and deterministic, the
    // output is necessary correct.
618
    if (aut_f->prop_weak() && aut_f->prop_deterministic())
619
620
      return min_aut_f;

621
622
    // if f is a syntactic obligation formula, the WDBA minimization
    // must be correct.
623
    if (f && f.is_syntactic_obligation())
624
625
      return min_aut_f;

626
    // If aut_f is a guarantee automaton, the WDBA minimization must be
627
    // correct.
628
    if (is_terminal_automaton(aut_f))
629
      return min_aut_f;
630
631
632
633

    // Build negation automaton if not supplied.
    if (!aut_neg_f)
      {
634
635
636
637
	if (f)
	  {
	    // If we know the formula, simply build the automaton for
	    // its negation.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
638
	    aut_neg_f = ltl_to_tgba_fm(formula::Not(f), aut_f->get_dict());
639
	    // Remove useless SCCs.
640
	    aut_neg_f = scc_filter(aut_neg_f, true);
641
642
643
644
645
	  }
	else if (is_deterministic(aut_f))
	  {
	    // If the automaton is deterministic, complementing is
	    // easy.
646
	    aut_neg_f = remove_fin(dtwa_complement(aut_f));
647
648
649
650
	  }
	else
	  {
	    // Otherwise, we cannot check if the minimization is safe.
651
	    return nullptr;
652
	  }
653
654
      }

655
    // If the negation is a guarantee automaton, then the
656
    // minimization is correct.
657
658
    if (is_terminal_automaton(aut_neg_f))
      return min_aut_f;
659
660
661

    bool ok = false;

662
    if (product(min_aut_f, aut_neg_f)->is_empty())
663
      {
664
	// Complement the minimized WDBA.
665
	assert(min_aut_f->prop_weak());
666
	auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
667
668
669
670
	if (product(aut_f, neg_min_aut_f)->is_empty())
	  // Finally, we are now sure that it was safe
	  // to minimize the automaton.
	  ok = true;
671
672
673
674
      }

    if (ok)
      return min_aut_f;
675
    return std::const_pointer_cast<twa_graph>(aut_f);
676
  }
677
}