minimize.cc 21.7 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
54
  // This is called hash_set for historical reason, but we need the
  // order inside hash_set to be deterministic.
  typedef std::set<const state*, state_ptr_less_than> hash_set;
55
  typedef state_map<unsigned> hash_map;
56

57
58
59
  namespace
  {
    static std::ostream&
60
    dump_hash_set(const hash_set* hs,
61
62
                  const const_twa_ptr& aut,
                  std::ostream& out)
63
    {
64
      out << '{';
65
66
      const char* sep = "";
      for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i)
67
68
69
70
        {
          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
    // 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())
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
        {
          const state* src = tovisit.front();
          tovisit.pop();

          for (auto sit: a->succ(src))
            {
              const state* dst = sit->dst();
              // 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();
            }
        }
111
    }
112

113
114
115
116
    // 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,
117
118
                 std::list<hash_set*>& sets,
                 hash_set* final)
119
120
121
122
    {
      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

      // 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)
131
132
133
134
135
136
137
        {
          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
      if (!final->empty())
143
        res->set_buchi();
144

145
      for (sit = sets.begin(); sit != sets.end(); ++sit)
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
        {
          hash_set* h = *sit;

          // 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))
            {
              const state* dst = succit->dst();
              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,
                                succit->cond(), accepting);
            }
        }
166
167
      res->merge_edges();
      if (res->num_states() > 0)
168
169
170
171
172
173
        {
          const state* init_state = a->get_init_state();
          unsigned init_num = state_num[init_state];
          init_state->destroy();
          res->set_init_state(init_num);
        }
174
175
176
177
      else
        {
          res->set_init_state(res->new_state());
        }
178
179
      return res;
    }
180

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

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

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

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


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

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

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

246
      loop_a->set_init_state(0U);
247
248
249
250
251

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

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

      return accepting;
    }

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

275
276
      // The list of equivalent states.
      partition_t done;
277

278
      hash_map state_set_map;
279

280
281
282
283
284
      // 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 =
285
        det_a->get_dict()->register_anonymous_variables(size, det_a);
286

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

292
      hash_set* final_copy;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293

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

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

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

333
334
335
      // 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;
336

337
      bool did_split = true;
338

339
      while (did_split)
340
341
342
343
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
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
        {
          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))
                    {
                      const state* dst = si->dst();
                      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;
                      f |= (bdd_ithvar(i->second) & si->cond());
                    }

                  // 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;
395
                  next_run.emplace_back(bsi->second);
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
                }
              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;
428
                          done.emplace_back(set);
429
430
431
432
433
                        }
                      else
                        {
                          trace << "set " << format_hash_set(set, det_a)
                                << " should be processed further" << std::endl;
434
                          next_run.emplace_back(set);
435
436
437
438
439
440
441
442
443
444
445
                        }
                    }
                }
              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);
        }
446

447
      done.splice(done.end(), cur_run);
448
449

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

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

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

471
472
      return res;
    }
473
  }
474

475
  twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a)
476
  {
477
478
479
480
    if (a->is_alternating())
      throw std::runtime_error
        ("minimize_monitor() does not support alternation");

481
    hash_set* final = new hash_set;
482
    hash_set* non_final = new hash_set;
483
    twa_graph_ptr det_a = tgba_powerset(a);
484
485

    // non_final contain all states.
486
    // final is empty: there is no acceptance condition
487
    build_state_set(det_a, non_final);
488
    auto res = minimize_dfa(det_a, final, non_final);
489
    res->prop_copy(a, { false, false, false, true });
490
    res->prop_deterministic(true);
491
    res->prop_weak(true);
492
    res->prop_state_acc(true);
493
    return res;
494
495
  }

496
  twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a)
497
  {
498
499
500
501
    if (a->is_alternating())
      throw std::runtime_error
        ("minimize_wdba() does not support alternation");

502
    hash_set* final = new hash_set;
503
504
    hash_set* non_final = new hash_set;

505
    twa_graph_ptr det_a;
506
507
508
509
510

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

511
512
513
514
515
      // 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
516
      // Christof Löding and published in Information Processing
517
518
519
520
521
      // 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).

522
      scc_info sm(det_a);
523
      sm.determine_unknown_acceptance();
524
      unsigned scc_count = sm.scc_count();
525
526
      // SCC that have been marked as useless.
      std::vector<bool> useless(scc_count);
527
528
529
530
531
532
533
      // 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;

534
      // SCC are numbered in topological order
535
      // (but in the reverse order as Löding's)
536
      for (unsigned m = 0; m < scc_count; ++m)
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
        {
          bool is_useless = true;
          bool transient = sm.is_trivial(m);
          auto& succ = sm.succ(m);

          if (transient && succ.empty())
            {
              // 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;
          for (unsigned j: succ)
            {
              is_useless &= useless[j];
              unsigned dj = d[j];
              if (dj < l)
                l = dj;
            }

          if (transient)
            {
              d[m] = l;
            }
          else
            {
              // Regular SCCs are accepting if any of their loop
              // corresponds to an accepted word in the original
              // automaton.
              if (wdba_scc_is_accepting(det_a, m, a, sm, pm))
                {
                  is_useless = false;
                  d[m] = l & ~1; // largest even number inferior or equal
                }
              else
                {
                  d[m] = (l - 1) | 1; // largest odd number inferior or equal
                }
            }

          useless[m] = is_useless;

          if (!is_useless)
            {
              hash_set* dest_set = (d[m] & 1) ? non_final : final;
              for (auto s: sm.states_of(m))
                dest_set->insert(det_a->state_from_number(s));
            }
        }
591
592
    }

593
    auto res = minimize_dfa(det_a, final, non_final);
594
    res->prop_copy(a, { false, false, false, true });
595
    res->prop_deterministic(true);
596
    res->prop_weak(true);
597
598
599
600
601
602
    // 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
603
    // is_terminal_automaton() seems overkill here.  But maybe we can
604
605
606
    // add a quick check inside minimize_dfa.
    if (a->prop_terminal())
      res->prop_terminal(true);
607
    return res;
608
609
  }

610
611
  twa_graph_ptr
  minimize_obligation(const const_twa_graph_ptr& aut_f,
612
613
614
                      formula f,
                      const_twa_graph_ptr aut_neg_f,
                      bool reject_bigger)
615
  {
616
617
618
619
    if (aut_f->is_alternating())
      throw std::runtime_error
        ("minimize_obligation() does not support alternation");

620
    auto min_aut_f = minimize_wdba(aut_f);
621

622
623
    if (reject_bigger)
      {
624
625
626
627
        // Abort if min_aut_f has more states than aut_f.
        unsigned orig_states = aut_f->num_states();
        if (orig_states < min_aut_f->num_states())
          return std::const_pointer_cast<twa_graph>(aut_f);
628
629
      }

630
631
    // If the input automaton was already weak and deterministic, the
    // output is necessary correct.
632
    if (aut_f->prop_weak() && aut_f->prop_deterministic())
633
634
      return min_aut_f;

635
636
    // if f is a syntactic obligation formula, the WDBA minimization
    // must be correct.
637
    if (f && f.is_syntactic_obligation())
638
639
      return min_aut_f;

640
    // If aut_f is a guarantee automaton, the WDBA minimization must be
641
    // correct.
642
    if (is_terminal_automaton(aut_f))
643
      return min_aut_f;
644
645
646
647

    // Build negation automaton if not supplied.
    if (!aut_neg_f)
      {
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
        if (f)
          {
            // If we know the formula, simply build the automaton for
            // its negation.
            aut_neg_f = ltl_to_tgba_fm(formula::Not(f), aut_f->get_dict());
            // Remove useless SCCs.
            aut_neg_f = scc_filter(aut_neg_f, true);
          }
        else if (is_deterministic(aut_f))
          {
            // If the automaton is deterministic, complementing is
            // easy.
            aut_neg_f = remove_fin(dtwa_complement(aut_f));
          }
        else
          {
            // Otherwise, we cannot check if the minimization is safe.
            return nullptr;
          }
667
668
      }

669
    // If the negation is a guarantee automaton, then the
670
    // minimization is correct.
671
672
    if (is_terminal_automaton(aut_neg_f))
      return min_aut_f;
673
674
675

    bool ok = false;

676
    if (product(min_aut_f, aut_neg_f)->is_empty())
677
      {
678
679
680
681
682
683
684
        // Complement the minimized WDBA.
        assert((bool)min_aut_f->prop_weak());
        auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
        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;
685
686
687
688
      }

    if (ok)
      return min_aut_f;
689
    return std::const_pointer_cast<twa_graph>(aut_f);
690
  }
691
}