minimize.cc 18.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
3
// 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
  typedef state_set hash_set;
  typedef state_map<unsigned> hash_map;
56

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

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

83
84
85
86
87
88
89
90
91
92
93
94
95
    // 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();
96

97
98
	  for (auto sit: a->succ(src))
	    {
99
	      const state* dst = sit->dst();
100
101
102
103
104
105
106
107
108
109
110
111
	      // 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();
	    }
	}
    }
112

113
114
115
116
117
118
119
120
121
122
    // 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);
123
      res->prop_state_acc(true);
124
125
126
127
128
129
130
131
132
133
134
135
136
137

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

139
140
      // For each transition in the initial automaton, add the corresponding
      // transition in res.
141

142
143
      if (!final->empty())
	res->set_buchi();
144

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

149
150
151
152
153
154
155
156
	  // 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))
	    {
157
	      const state* dst = succit->dst();
158
159
160
161
162
	      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,
163
				succit->cond(), accepting);
164
165
166
167
168
169
170
171
172
173
174
175
	    }
	}
      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;
    }
176
177
178

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

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

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

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


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

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

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

242
      loop_a->set_init_state(0U);
243
244
245
246
247

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

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

      return accepting;
    }

264
265
266
267
268
269
    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;
270

271
272
      // The list of equivalent states.
      partition_t done;
273

274
      hash_map state_set_map;
275

276
277
278
279
280
281
      // 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);
282

283
284
285
286
      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;
287

288
      hash_set* final_copy;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
289

290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
      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
309

310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
      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;
	}
328

329
330
331
      // 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;
332

333
      bool did_split = true;
334

335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
      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))
		    {
355
		      const state* dst = si->dst();
356
357
358
359
360
361
362
363
364
365
		      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;
366
		      f |= (bdd_ithvar(i->second) & si->cond());
367
368
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
		    }

		  // 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);
	}
442

443
      done.splice(done.end(), cur_run);
444
445

#ifdef TRACE
446
447
448
449
      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;
450
#endif
Felix Abecassis's avatar
Felix Abecassis committed
451

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

455
456
457
458
459
460
461
462
463
464
465
      // 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
466

467
468
      return res;
    }
469
  }
470

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

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

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

493
    twa_graph_ptr det_a;
494
495
496
497
498

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

499
500
501
502
503
      // 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
504
      // Christof Löding and published in Information Processing
505
506
507
508
509
      // 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).

510
      scc_info sm(det_a);
511
      sm.determine_unknown_acceptance();
512
      unsigned scc_count = sm.scc_count();
513
514
      // SCC that have been marked as useless.
      std::vector<bool> useless(scc_count);
515
516
517
518
519
520
521
      // 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;

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

530
	  if (transient && succ.empty())
531
	    {
532
533
534
535
536
537
538
539
540
541
	      // 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;
542
	  for (unsigned j: succ)
543
	    {
544
545
	      is_useless &= useless[j];
	      unsigned dj = d[j];
546
547
548
549
550
551
552
	      if (dj < l)
		l = dj;
	    }

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

570
	  useless[m] = is_useless;
571

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

581
    auto res = minimize_dfa(det_a, final, non_final);
582
    res->prop_copy(a, { false, false, false, true });
583
    res->prop_deterministic(true);
584
    res->prop_weak(true);
585
586
587
588
589
590
    // 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
591
    // is_terminal_automaton() seems overkill here.  But maybe we can
592
593
594
    // add a quick check inside minimize_dfa.
    if (a->prop_terminal())
      res->prop_terminal(true);
595
    return res;
596
597
  }

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

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

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

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

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

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

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

    bool ok = false;

660
    if (product(min_aut_f, aut_neg_f)->is_empty())
661
      {
662
	// Complement the minimized WDBA.
663
	assert(min_aut_f->prop_weak());
664
	auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
665
666
667
668
	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;
669
670
671
672
      }

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