minimize.cc 21.2 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
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
      return res;
    }
176

177
    struct wdba_search_acc_loop final : public bfs_steps
178
    {
179
      wdba_search_acc_loop(const const_twa_ptr& det_a,
180
181
182
                           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)
183
      {
184
        seen(dest);
185
186
187
      }

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

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

      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
    wdba_scc_is_accepting(const const_twa_graph_ptr& det_a, unsigned scc_n,
213
214
                          const const_twa_graph_ptr& orig_a, scc_info& sm,
                          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
      int n;
      for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
233
234
235
236
        {
          loop_a->new_edge(n - 1, n, i->label);
          i->s->destroy();
        }
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
      const power_map::power_state& ps =
249
        pm.states_of(det_a->state_number(start));
250
      for (auto& s: ps)
251
252
253
254
255
256
257
258
259
        {
          // 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;
            }
        }
260
261
262
263

      return accepting;
    }

264
    static twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a,
265
                                      hash_set* final, hash_set* non_final)
266
267
268
269
    {
      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
      // 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 =
281
        det_a->get_dict()->register_anonymous_variables(size, det_a);
282

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

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

290
      if (!final->empty())
291
292
293
294
295
296
297
298
299
300
301
302
303
304
        {
          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);
        }
305
      else
306
307
308
        {
          final_copy = final;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
309

310
      if (!non_final->empty())
311
312
313
314
315
316
317
318
319
320
321
322
323
        {
          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;
        }
324
      else
325
326
327
        {
          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
      while (did_split)
336
337
338
339
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
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
        {
          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;
                  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
      trace << "Final partition: ";
      for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
448
        trace << format_hash_set(*i, det_a) << ' ';
449
      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
      // Free all the allocated memory.
      delete final_copy;
      hash_map::iterator hit;
      for (hit = state_set_map.begin(); hit != state_set_map.end();)
459
460
461
462
        {
          hash_map::iterator old = hit++;
          old->first->destroy();
        }
463
464
      std::list<hash_set*>::iterator it;
      for (it = done.begin(); it != done.end(); ++it)
465
        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
527
528
529
530
531
532
533
534
535
536
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
        {
          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));
            }
        }
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,
600
601
602
                      formula f,
                      const_twa_graph_ptr aut_neg_f,
                      bool reject_bigger)
603
  {
604
    auto min_aut_f = minimize_wdba(aut_f);
605

606
607
    if (reject_bigger)
      {
608
609
610
611
        // 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);
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
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
        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;
          }
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
663
664
665
666
667
668
        // 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;
669
670
671
672
      }

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