sccinfo.cc 20.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
// 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 <spot/twaalgos/sccinfo.hh>
21
22
23
#include <stack>
#include <algorithm>
#include <queue>
24
25
26
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/misc/escape.hh>
27

28

29
30
namespace spot
{
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
  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");
  }
48
49
50
51
52
53

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

59
      acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition
60
61
      acc_cond::mark_t acc = 0U; // union of all acceptance marks in the SCC
      acc_cond::mark_t common = -1U; // intersection of all marks in the SCC
62
63
      int index;                     // Index of the SCC
      bool trivial = true;           // Whether the SCC has no cycle
64
      bool accepting = false;        // Necessarily accepting
65
66
67
    };
  }

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

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

83
84
    sccof_.resize(n, -1U);

85
86
87
88
89
90
    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);
91
    std::deque<scc> root_;        // Stack of SCC roots.
92
93
94
95
96
    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.

97
98
99
100
101
102
103
104
105
106
107
108
109
110
    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();

111
112
113
114
115
116
117
118
119
120
    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);
      };

121
122
123
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
188
189
190
    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 ||
            aut->acc().maybe_accepting(acc, common).is_false();
            node_.back().rejecting_ = reject;
            root_.pop_back();
          }
      };

191
192
    // Setup depth-first search from the initial state.  But we may
    // have a conjunction of initial state in alternating automata.
193
194
195
196
197
198
    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())
199
      {
200
201
        unsigned init = init_states.front();
        init_states.pop_front();
202
203
204
205
206
207
208
209
        int spi = h_[init];
        if (spi > 0)
          continue;
        assert(spi == 0);
        h_[init] = --num_;
        root_.emplace_back(num_, 0U);
        todo_.emplace(stack_item{init, gr.state_storage(init).succ, 0});
        live.emplace_back(init);
210

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

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

222
223
224
225
226
227
228
                // 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());
229
                backtrack(curr);
230
231
232
233
234
235
                continue;
              }

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

237
238
            unsigned dest = e.dst;
            if ((int) dest < 0)
239
              {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240
                // Iterate over all destinations of a universal edge.
241
242
243
244
245
246
                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)
247
                  {
248
249
                    todo_.top().out_edge = e.next_succ;
                    todo_.top().univ_pos = 0;
250
                  }
251
                else
252
                  {
253
                    ++todo_.top().univ_pos;
254
                  }
255
              }
256
257
258
259
            else
              {
                todo_.top().out_edge = e.next_succ;
              }
260

261
262
263
264
265
266
267
268
269
270
271
272
273
            // 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;
                }

274
            acc_cond::mark_t acc = e.acc;
275

276
277
278
279
280
281
282
283
284
285
286
287
            // 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;
              }
288

289
            // We already know the state.
290

291
292
293
            // Have we reached a maximal SCC?
            if (spi > 0)
              continue;
294

295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
            // 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);
311

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

326
327
328
329
330
331
            // 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;
332
            root_.back().common &= common;
333
334
335
336
            root_.back().accepting |= is_accepting
              || aut->acc().accepting(root_.back().acc);
            // This SCC is no longer trivial.
            root_.back().trivial = false;
337
338
339
340
341
342
343
344
345
346
347
348

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

  void scc_info::determine_usefulness()
  {
357
358
    // An SCC is useful if it is not rejecting or it has a successor
    // SCC that is useful.
359
    unsigned scccount = scc_count();
360
    for (unsigned i = 0; i < scccount; ++i)
361
      {
362
363
364
365
366
367
368
369
370
371
372
373
        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;
            }
374
375
376
      }
  }

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

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

    for (unsigned src = 0; src < n; ++src)
      {
392
393
394
395
396
397
398
399
400
401
        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);
          }
402
403
404
405
      }
    return result;
  }

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

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

424
425
426
  void scc_info::determine_unknown_acceptance()
  {
    std::vector<bool> k;
427
    unsigned s = scc_count();
428
    bool changed = false;
429
430
431
432
433
434
    // iterate over SCCs in topological order
    do
      {
        --s;
        if (!is_rejecting_scc(s) && !is_accepting_scc(s))
          {
435
            if (SPOT_UNLIKELY(!aut_->is_existential()))
436
437
438
              throw std::runtime_error(
                  "scc_info::determine_unknown_acceptance() "
                  "does not support alternating automata");
439
440
            if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
              report_need_track_states();
441
442
443
444
445
            auto& node = node_[s];
            if (k.empty())
              k.resize(aut_->num_states());
            for (auto i: node.states_)
              k[i] = true;
446
            if (mask_keep_accessible_states(aut_, k, node.one_state_)
447
448
449
450
451
452
453
454
                ->is_empty())
              node.rejecting_ = true;
            else
              node.accepting_ = true;
            changed = true;
          }
      }
    while (s);
455
    if (changed && !!(options_ & scc_info_options::TRACK_SUCCS))
456
457
458
      determine_usefulness();
  }

459
460
  std::ostream&
  dump_scc_info_dot(std::ostream& out,
461
                    const_twa_graph_ptr aut, scc_info* sccinfo)
462
463
464
465
466
467
468
469
470
471
472
473
474
475
  {
    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())
      {
476
477
        int state = q.front();
        q.pop();
478

479
        out << "  " << state << " [shape=box,"
480
481
            << (aut->acc().accepting(m->acc_sets_of(state)) ?
                "style=bold," : "")
482
            << "label=\"" << state;
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
        {
          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);
          }
500
501
502
503
504
505
506
507
      }

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

508
  std::vector<twa_graph_ptr>
509
510
  scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets,
                          bool preserve_names) const
511
  {
512
513
    if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
      report_need_track_states();
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
    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());
        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())
544
545
546
547
548
          {
            if (preserve_names)
              copy->copy_state_names_from(aut_);
            res.push_back(copy);
          }
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
      }
    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
  {
    if (!is_rejecting_scc(scc))
      {
        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.
        acc_cond::mark_t m = 0u;
        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]];

              scc_info si_tmp(aut);
              unsigned scccount_tmp = si_tmp.scc_count();
              for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp)
590
591
                si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf,
                                                  nb_pairs, pairs, res,
592
593
594
595
596
597
598
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;
    if (!is_rejecting_scc(scc))
      {
        std::vector<unsigned> old;
        unsigned nb_states = aut_->num_states();
        for (unsigned i = 0; i < nb_states; ++i)
          old.push_back(i);

618
619
        acc_cond::mark_t all_fin = 0U;
        acc_cond::mark_t all_inf = 0U;
620
621
622
623
624
625
626
627
        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;
  }
628
}