sccinfo.cc 20.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
3
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#include "config.h"
21
#include <spot/twaalgos/sccinfo.hh>
22
23
24
#include <stack>
#include <algorithm>
#include <queue>
25
26
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/mask.hh>
27
#include <spot/twaalgos/genem.hh>
28
#include <spot/misc/escape.hh>
29

30

31
32
namespace spot
{
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  void scc_info::report_need_track_states()
  {
    throw std::runtime_error
      ("scc_info was not run with option TRACK_STATES");
  }

  void scc_info::report_need_track_succs()
  {
    throw std::runtime_error
      ("scc_info was not run with option TRACK_SUCCS");
  }

  void scc_info::report_incompatible_stop_on_acc()
  {
    throw std::runtime_error
      ("scc_info was run with option STOP_ON_ACC");
  }
50
51
52
53
54
55

  namespace
  {
    struct scc
    {
    public:
56
      scc(int index, acc_cond::mark_t in_acc):
57
        in_acc(in_acc), index(index)
58
59
60
      {
      }

61
      acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition
62
63
64
      acc_cond::mark_t acc = {}; // union of all acceptance marks in the SCC
      // intersection of all marks in the SCC
      acc_cond::mark_t common = acc_cond::mark_t::all();
65
66
      int index;                     // Index of the SCC
      bool trivial = true;           // Whether the SCC has no cycle
67
      bool accepting = false;        // Necessarily accepting
68
69
70
    };
  }

71
72
73
  scc_info::scc_info(const_twa_graph_ptr aut,
                     unsigned initial_state,
                     edge_filter filter,
74
75
                     void* filter_data,
                     scc_info_options options)
76
    : aut_(aut), initial_state_(initial_state),
77
78
      filter_(filter), filter_data_(filter_data),
      options_(options)
79
80
  {
    unsigned n = aut->num_states();
81
82
83
84
85

    if (initial_state != -1U && n <= initial_state)
      throw std::runtime_error
        ("scc_info: supplied initial state does not exist");

86
87
    sccof_.resize(n, -1U);

88
89
90
91
92
93
    if (!!(options & scc_info_options::TRACK_STATES_IF_FIN_USED)
        && aut->acc().uses_fin_acceptance())
      options_ = options = options | scc_info_options::TRACK_STATES;

    std::vector<unsigned> live;
    live.reserve(n);
94
    std::deque<scc> root_;        // Stack of SCC roots.
95
96
97
98
99
    std::vector<int> h_(n, 0);
    // Map of visited states.  Values > 0 designate maximal SCC.
    // Values < 0 number states that are part of incomplete SCCs being
    // completed.  0 denotes non-visited states.

100
101
102
103
104
105
106
107
108
109
110
111
112
113
    int num_ = 0;               // Number of visited nodes, negated.

    struct stack_item {
      unsigned src;
      unsigned out_edge;
      unsigned univ_pos;
    };
    // DFS stack.  Holds (STATE, TRANS, UNIV_POS) pairs where TRANS is
    // the current outgoing transition of STATE, and UNIV_POS is used
    // when the transition is universal to iterate over all possible
    // destinations.
    std::stack<stack_item> todo_;
    auto& gr = aut->get_graph();

114
115
116
117
118
119
120
121
122
123
    std::deque<unsigned> init_states;
    std::vector<bool> init_seen(n, false);
    auto push_init = [&](unsigned s)
      {
        if (h_[s] != 0 || init_seen[s])
          return;
        init_seen[s] = true;
        init_states.push_back(s);
      };

124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
    bool track_states = !!(options & scc_info_options::TRACK_STATES);
    bool track_succs = !!(options & scc_info_options::TRACK_SUCCS);
    auto backtrack = [&](unsigned curr)
      {
        if (root_.back().index == h_[curr])
          {
            unsigned num = node_.size();
            acc_cond::mark_t acc = root_.back().acc;
            acc_cond::mark_t common = root_.back().common;
            bool triv = root_.back().trivial;
            node_.emplace_back(acc, common, triv);

            auto& succ = node_.back().succ_;
            unsigned np1 = num + 1;
            auto s = live.rbegin();
            do
              {
                sccof_[*s] = num;
                h_[*s] = np1;

                // Gather all successor SCCs
                if (track_succs)
                  for (auto& t: aut->out(*s))
                    for (unsigned d: aut->univ_dests(t))
                      {
                        unsigned n = sccof_[d];
                        if (n == num || n == -1U)
                          continue;
                        // If edges are cut, we are not able to
                        // maintain proper successor information.
                        if (filter_)
                          switch (filter_(t, d, filter_data_))
                            {
                            case edge_filter_choice::keep:
                              break;
                            case edge_filter_choice::ignore:
                            case edge_filter_choice::cut:
                              continue;
                            }
                        succ.emplace_back(n);
                      }
              }
            while (*s++ != curr);

            if (track_states)
              {
                auto& nbs = node_.back().states_;
                nbs.insert(nbs.end(), s.base(), live.end());
              }

            node_.back().one_state_ = curr;
            live.erase(s.base(), live.end());

            if (track_succs)
              {
                std::sort(succ.begin(), succ.end());
                succ.erase(std::unique(succ.begin(), succ.end()), succ.end());
              }

            bool accept = !triv && root_.back().accepting;
            node_.back().accepting_ = accept;
            if (accept)
              one_acc_scc_ = num;
            bool reject = triv ||
Clément Gillard's avatar
Clément Gillard committed
188
              aut->acc().maybe_accepting(acc, common).is_false();
189
190
191
192
193
            node_.back().rejecting_ = reject;
            root_.pop_back();
          }
      };

194
195
    // Setup depth-first search from the initial state.  But we may
    // have a conjunction of initial state in alternating automata.
196
197
198
199
200
201
    if (initial_state_ == -1U)
      initial_state_ = aut->get_init_state_number();
    for (unsigned init: aut->univ_dests(initial_state_))
      push_init(init);

    while (!init_states.empty())
202
      {
203
204
        unsigned init = init_states.front();
        init_states.pop_front();
205
206
207
208
209
        int spi = h_[init];
        if (spi > 0)
          continue;
        assert(spi == 0);
        h_[init] = --num_;
210
        root_.emplace_back(num_, acc_cond::mark_t({}));
211
212
        todo_.emplace(stack_item{init, gr.state_storage(init).succ, 0});
        live.emplace_back(init);
213

214
        while (!todo_.empty())
215
          {
216
217
            // We are looking at the next successor in SUCC.
            unsigned tr_succ = todo_.top().out_edge;
218

219
220
221
222
223
            // If there is no more successor, backtrack.
            if (!tr_succ)
              {
                // We have explored all successors of state CURR.
                unsigned curr = todo_.top().src;
224

225
226
227
228
229
230
231
                // Backtrack TODO_.
                todo_.pop();

                // When backtracking the root of an SCC, we must also
                // remove that SCC from the ARC/ROOT stacks.  We must
                // discard from H all reachable states from this SCC.
                assert(!root_.empty());
232
                backtrack(curr);
233
234
235
236
237
238
                continue;
              }

            // We have a successor to look at.
            // Fetch the values we are interested in...
            auto& e = gr.edge_storage(tr_succ);
239

240
241
            unsigned dest = e.dst;
            if ((int) dest < 0)
242
              {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
243
                // Iterate over all destinations of a universal edge.
244
245
246
247
248
249
                if (todo_.top().univ_pos == 0)
                  todo_.top().univ_pos = ~dest + 1;
                const auto& v = gr.dests_vector();
                dest = v[todo_.top().univ_pos];
                // Last universal destination?
                if (~e.dst + v[~e.dst] == todo_.top().univ_pos)
250
                  {
251
252
                    todo_.top().out_edge = e.next_succ;
                    todo_.top().univ_pos = 0;
253
                  }
254
                else
255
                  {
256
                    ++todo_.top().univ_pos;
257
                  }
258
              }
259
260
261
262
            else
              {
                todo_.top().out_edge = e.next_succ;
              }
263

264
265
266
267
268
269
270
271
272
273
274
275
276
            // Do we really want to look at this
            if (filter_)
              switch (filter_(e, dest, filter_data_))
                {
                case edge_filter_choice::keep:
                  break;
                case edge_filter_choice::ignore:
                  continue;
                case edge_filter_choice::cut:
                  push_init(e.dst);
                  continue;
                }

277
            acc_cond::mark_t acc = e.acc;
278

279
280
281
282
283
284
285
286
287
288
289
290
            // Are we going to a new state?
            int spi = h_[dest];
            if (spi == 0)
              {
                // Yes.  Number it, stack it, and register its successors
                // for later processing.
                h_[dest] = --num_;
                root_.emplace_back(num_, acc);
                todo_.emplace(stack_item{dest, gr.state_storage(dest).succ, 0});
                live.emplace_back(dest);
                continue;
              }
291

292
            // We already know the state.
293

294
295
296
            // Have we reached a maximal SCC?
            if (spi > 0)
              continue;
297

298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
            // Now this is the most interesting case.  We have reached a
            // state S1 which is already part of a non-dead SCC.  Any such
            // non-dead SCC has necessarily been crossed by our path to
            // this state: there is a state S2 in our path which belongs
            // to this SCC too.  We are going to merge all states between
            // this S1 and S2 into this SCC..
            //
            // This merge is easy to do because the order of the SCC in
            // ROOT is descending: we just have to merge all SCCs from the
            // top of ROOT that have an index lesser than the one of
            // the SCC of S2 (called the "threshold").
            int threshold = spi;
            bool is_accepting = false;
            // If this is a self-loop, check its acceptance alone.
            if (dest == e.src)
              is_accepting = aut->acc().accepting(acc);
314

315
            acc_cond::mark_t common = acc;
316
            assert(!root_.empty());
317
318
319
            while (threshold > root_.back().index)
              {
                acc |= root_.back().acc;
320
321
322
323
                acc_cond::mark_t in_acc = root_.back().in_acc;
                acc |= in_acc;
                common &= root_.back().common;
                common &= in_acc;
324
325
326
327
                is_accepting |= root_.back().accepting;
                root_.pop_back();
                assert(!root_.empty());
              }
328

329
330
331
332
333
334
            // Note that we do not always have
            //  threshold == root_.back().index
            // after this loop, the SCC whose index is threshold might have
            // been merged with a higher SCC.

            root_.back().acc |= acc;
335
            root_.back().common &= common;
336
337
338
339
            root_.back().accepting |= is_accepting
              || aut->acc().accepting(root_.back().acc);
            // This SCC is no longer trivial.
            root_.back().trivial = false;
340
341
342
343
344
345
346
347
348
349
350
351

            if (root_.back().accepting
                && !!(options & scc_info_options::STOP_ON_ACC))
              {
                while (!todo_.empty())
                  {
                    unsigned curr = todo_.top().src;
                    todo_.pop();
                    backtrack(curr);
                  }
                return;
              }
352
          }
353
      }
354
355
    if (track_succs && !(options & scc_info_options::STOP_ON_ACC))
      determine_usefulness();
356
357
358
359
  }

  void scc_info::determine_usefulness()
  {
360
361
    // An SCC is useful if it is not rejecting or it has a successor
    // SCC that is useful.
362
    unsigned scccount = scc_count();
363
    for (unsigned i = 0; i < scccount; ++i)
364
      {
365
366
367
368
369
370
371
372
373
374
375
376
        if (!node_[i].is_rejecting())
          {
            node_[i].useful_ = true;
            continue;
          }
        node_[i].useful_ = false;
        for (unsigned j: node_[i].succ())
          if (node_[j].is_useful())
            {
              node_[i].useful_ = true;
              break;
            }
377
378
379
      }
  }

380
  std::set<acc_cond::mark_t> scc_info::marks_of(unsigned scc) const
381
382
  {
    std::set<acc_cond::mark_t> res;
383
384
    for (auto& t: inner_edges_of(scc))
      res.insert(t.acc);
385
386
387
    return res;
  }

388
  std::vector<std::set<acc_cond::mark_t>> scc_info::marks() const
389
  {
390
    unsigned n = aut_->num_states();
391
    std::vector<std::set<acc_cond::mark_t>> result(scc_count());
392
393
394

    for (unsigned src = 0; src < n; ++src)
      {
395
396
397
398
399
400
401
402
403
404
        unsigned src_scc = scc_of(src);
        if (src_scc == -1U || is_rejecting_scc(src_scc))
          continue;
        auto& s = result[src_scc];
        for (auto& t: aut_->out(src))
          {
            if (scc_of(t.dst) != src_scc)
              continue;
            s.insert(t.acc);
          }
405
406
407
408
      }
    return result;
  }

409
410
411
412
  std::vector<bool> scc_info::weak_sccs() const
  {
    unsigned n = scc_count();
    std::vector<bool> result(scc_count());
413
    auto acc = marks();
414
    for (unsigned s = 0; s < n; ++s)
415
      result[s] = is_rejecting_scc(s) || acc[s].size() == 1;
416
417
418
    return result;
  }

419
420
421
  bdd scc_info::scc_ap_support(unsigned scc) const
  {
    bdd support = bddtrue;
422
423
    for (auto& t: edges_of(scc))
      support &= bdd_support(t.cond);
424
425
426
    return support;
  }

427
  bool scc_info::check_scc_emptiness(unsigned n)
428
429
430
431
432
433
  {
    if (SPOT_UNLIKELY(!aut_->is_existential()))
      throw std::runtime_error("scc_info::check_scc_emptiness() "
                               "does not support alternating automata");
    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
      report_need_track_states();
434
    return generic_emptiness_check_for_scc(*this, n);
435
436
  }

437
438
  void scc_info::determine_unknown_acceptance()
  {
439
    unsigned s = scc_count();
440
    bool changed = false;
441
442
443
444
445
446
    // iterate over SCCs in topological order
    do
      {
        --s;
        if (!is_rejecting_scc(s) && !is_accepting_scc(s))
          {
447
            if (SPOT_UNLIKELY(!aut_->is_existential()))
448
449
450
451
              throw std::runtime_error(
                  "scc_info::determine_unknown_acceptance() "
                  "does not support alternating automata");
            auto& node = node_[s];
452
            if (check_scc_emptiness(s))
453
454
455
456
457
458
459
              node.rejecting_ = true;
            else
              node.accepting_ = true;
            changed = true;
          }
      }
    while (s);
460
    if (changed && !!(options_ & scc_info_options::TRACK_SUCCS))
461
462
463
      determine_usefulness();
  }

464
465
  std::ostream&
  dump_scc_info_dot(std::ostream& out,
466
                    const_twa_graph_ptr aut, scc_info* sccinfo)
467
468
469
470
471
472
473
474
475
476
477
478
479
480
  {
    scc_info* m = sccinfo ? sccinfo : new scc_info(aut);

    out << "digraph G {\n  i [label=\"\", style=invis, height=0]\n";
    int start = m->scc_of(aut->get_init_state_number());
    out << "  i -> " << start << std::endl;

    std::vector<bool> seen(m->scc_count());
    seen[start] = true;

    std::queue<int> q;
    q.push(start);
    while (!q.empty())
      {
481
482
        int state = q.front();
        q.pop();
483

484
        out << "  " << state << " [shape=box,"
485
486
            << (aut->acc().accepting(m->acc_sets_of(state)) ?
                "style=bold," : "")
487
            << "label=\"" << state;
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
        {
          size_t n = m->states_of(state).size();
          out << " (" << n << " state";
          if (n > 1)
            out << 's';
          out << ')';
        }
        out << "\"]\n";

        for (unsigned dest: m->succ(state))
          {
            out << "  " << state << " -> " << dest << '\n';
            if (seen[dest])
              continue;
            seen[dest] = true;
            q.push(dest);
          }
505
506
507
508
509
510
511
512
      }

    out << "}\n";
    if (!sccinfo)
      delete m;
    return out;
  }

513
  std::vector<twa_graph_ptr>
514
515
  scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets,
                          bool preserve_names) const
516
  {
517
518
    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
      report_need_track_states();
519
520
521
522
523
524
525
526
527
528
529
530
    std::vector<twa_graph_ptr> res;

    std::vector<bool> seen(aut_->num_states(), false);
    std::vector<bool> cur(aut_->num_states(), false);

    for (unsigned init: states_of(scc))
      {
        if (seen[init])
          continue;
        cur.assign(aut_->num_states(), false);

        auto copy = make_twa_graph(aut_->get_dict());
531
        copy->copy_ap_of(aut_);
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
        copy->copy_acceptance_of(aut_);
        copy->prop_state_acc(aut_->prop_state_acc());
        transform_accessible(aut_, copy, [&](unsigned src,
                                             bdd& cond,
                                             acc_cond::mark_t& m,
                                             unsigned dst)
                             {
                               cur[src] = seen[src] = true;
                               if (scc_of(dst) != scc
                                   || (m & sets)
                                   || (seen[dst] && !cur[dst]))
                                 {
                                   cond = bddfalse;
                                   return;
                                 }
                             },
                             init);
        if (copy->num_edges())
550
551
552
553
554
          {
            if (preserve_names)
              copy->copy_state_names_from(aut_);
            res.push_back(copy);
          }
555
556
557
558
559
560
561
562
563
564
565
566
567
      }
    return res;
  }

  void
  scc_info::states_on_acc_cycle_of_rec(unsigned scc,
                                       acc_cond::mark_t all_fin,
                                       acc_cond::mark_t all_inf,
                                       unsigned nb_pairs,
                                       std::vector<acc_cond::rs_pair>& pairs,
                                       std::vector<unsigned>& res,
                                       std::vector<unsigned>& old) const
  {
568
    if (is_useful_scc(scc) && !is_rejecting_scc(scc))
569
570
571
572
573
574
575
      {
        acc_cond::mark_t all_acc = acc_sets_of(scc);
        acc_cond::mark_t fin = all_fin & all_acc;
        acc_cond::mark_t inf = all_inf & all_acc;

        // Get all Fin acceptance set that appears in the SCC and does not have
        // their corresponding Inf appearing in the SCC.
576
        acc_cond::mark_t m = {};
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
        if (fin)
          for (unsigned p = 0; p < nb_pairs; ++p)
            if (fin & pairs[p].fin && !(inf & pairs[p].inf))
              m |= pairs[p].fin;

        if (m)
          for (const twa_graph_ptr& aut : split_on_sets(scc, m))
            {
              auto orig_sts = aut->get_named_prop
                <std::vector<unsigned>>("original-states");

              // Update mapping of state numbers between the current automaton
              // and the starting one.
              for (unsigned i = 0; i < orig_sts->size(); ++i)
                (*orig_sts)[i] = old[(*orig_sts)[i]];

593
594
              scc_info si_tmp(aut, scc_info_options::TRACK_STATES
                                   | scc_info_options::TRACK_SUCCS);
595
596
              unsigned scccount_tmp = si_tmp.scc_count();
              for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp)
597
598
                si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf,
                                                  nb_pairs, pairs, res,
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
                                                  *orig_sts);
            }

        else  // Accepting cycle found.
          for (unsigned s : states_of(scc))
            res.push_back(old[s]);
      }
  }

  std::vector<unsigned>
  scc_info::states_on_acc_cycle_of(unsigned scc) const
  {
    std::vector<acc_cond::rs_pair> pairs;
    if (!aut_->acc().is_streett_like(pairs))
      throw std::runtime_error("states_on_acc_cycle_of only works with "
                               "Streett-like acceptance condition");
    unsigned nb_pairs = pairs.size();

    std::vector<unsigned> res;
618
    if (is_useful_scc(scc) && !is_rejecting_scc(scc))
619
620
621
622
623
624
      {
        std::vector<unsigned> old;
        unsigned nb_states = aut_->num_states();
        for (unsigned i = 0; i < nb_states; ++i)
          old.push_back(i);

625
626
        acc_cond::mark_t all_fin = {};
        acc_cond::mark_t all_inf = {};
627
628
629
630
631
632
633
634
        std::tie(all_inf, all_fin) = aut_->get_acceptance().used_inf_fin_sets();

        states_on_acc_cycle_of_rec(scc, all_fin, all_inf, nb_pairs, pairs, res,
                                   old);
      }

    return res;
  }
635
}