sccinfo.cc 14.7 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
31
32
33
34
35
36
namespace spot
{

  namespace
  {
    struct scc
    {
    public:
37
      scc(int index, acc_cond::mark_t in_acc):
38
        in_acc(in_acc), index(index)
39
40
41
      {
      }

42
      acc_cond::mark_t in_acc;  // Acceptance sets on the incoming transition
43
44
      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
45
46
47
      int index;                // Index of the SCC
      bool trivial = true;        // Whether the SCC has no cycle
      bool accepting = false;        // Necessarily accepting
48
49
50
    };
  }

51
52
53
54
55
56
  scc_info::scc_info(const_twa_graph_ptr aut,
                     unsigned initial_state,
                     edge_filter filter,
                     void* filter_data)
    : aut_(aut), initial_state_(initial_state),
      filter_(filter), filter_data_(filter_data)
57
58
59
60
  {
    unsigned n = aut->num_states();
    sccof_.resize(n, -1U);

61
    std::deque<unsigned> live;
62
    std::deque<scc> root_;        // Stack of SCC roots.
63
64
65
66
67
    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.

68
69
70
71
72
73
74
75
76
77
78
79
80
81
    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();

82
83
84
85
86
87
88
89
90
91
92

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

93
94
    // Setup depth-first search from the initial state.  But we may
    // have a conjunction of initial state in alternating automata.
95
96
97
98
99
100
    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())
101
      {
102
103
        unsigned init = init_states.front();
        init_states.pop_front();
104
105
106
107
108
109
110
111
        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);
112

113
        while (!todo_.empty())
114
          {
115
116
            // We are looking at the next successor in SUCC.
            unsigned tr_succ = todo_.top().out_edge;
117

118
119
120
121
122
            // If there is no more successor, backtrack.
            if (!tr_succ)
              {
                // We have explored all successors of state CURR.
                unsigned curr = todo_.top().src;
123

124
125
126
127
128
129
130
131
132
133
                // 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());
                if (root_.back().index == h_[curr])
                  {
                    unsigned num = node_.size();
134
135
                    acc_cond::mark_t acc = root_.back().acc;
                    acc_cond::mark_t common = root_.back().common;
136
                    bool triv = root_.back().trivial;
137
                    node_.emplace_back(acc, common, triv);
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159

                    // Move all elements of this SCC from the live stack
                    // to the the node.
                    auto i = std::find(live.rbegin(), live.rend(), curr);
                    assert(i != live.rend());
                    ++i;                // Because base() does -1
                    auto& nbs = node_.back().states_;
                    nbs.insert(nbs.end(), i.base(), live.end());
                    live.erase(i.base(), live.end());

                    std::set<unsigned> dests;
                    unsigned np1 = num + 1;
                    for (unsigned s: nbs)
                      {
                        sccof_[s] = num;
                        h_[s] = np1;
                      }
                    // Gather all successor SCCs
                    for (unsigned s: nbs)
                      for (auto& t: aut->out(s))
                        for (unsigned d: aut->univ_dests(t))
                          {
160
161
162
163
164
165
166
167
168
169
170
                            // 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;
                                }
171
172
173
174
175
176
177
178
179
180
                            unsigned n = sccof_[d];
                            assert(n != -1U);
                            if (n == num)
                              continue;
                            dests.insert(n);
                          }
                    auto& succ = node_.back().succ_;
                    succ.insert(succ.end(), dests.begin(), dests.end());
                    bool accept = !triv && root_.back().accepting;
                    node_.back().accepting_ = accept;
181
182
                    bool reject = triv ||
                      aut->acc().maybe_accepting(acc, common).is_false();
183
184
185
186
187
188
189
190
191
                    node_.back().rejecting_ = reject;
                    root_.pop_back();
                  }
                continue;
              }

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

193
194
            unsigned dest = e.dst;
            if ((int) dest < 0)
195
              {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
196
                // Iterate over all destinations of a universal edge.
197
198
199
200
201
202
                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)
203
                  {
204
205
                    todo_.top().out_edge = e.next_succ;
                    todo_.top().univ_pos = 0;
206
                  }
207
                else
208
                  {
209
                    ++todo_.top().univ_pos;
210
                  }
211
              }
212
213
214
215
            else
              {
                todo_.top().out_edge = e.next_succ;
              }
216

217
218
219
220
221
222
223
224
225
226
227
228
229
            // 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;
                }

230
            acc_cond::mark_t acc = e.acc;
231

232
233
234
235
236
237
238
239
240
241
242
243
            // 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;
              }
244

245
            // We already know the state.
246

247
248
249
            // Have we reached a maximal SCC?
            if (spi > 0)
              continue;
250

251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
            // 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);
267

268
            acc_cond::mark_t common = acc;
269
            assert(!root_.empty());
270
271
272
            while (threshold > root_.back().index)
              {
                acc |= root_.back().acc;
273
274
275
276
                acc_cond::mark_t in_acc = root_.back().in_acc;
                acc |= in_acc;
                common &= root_.back().common;
                common &= in_acc;
277
278
279
280
                is_accepting |= root_.back().accepting;
                root_.pop_back();
                assert(!root_.empty());
              }
281

282
283
284
285
286
287
            // 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;
288
            root_.back().common &= common;
289
290
291
292
293
            root_.back().accepting |= is_accepting
              || aut->acc().accepting(root_.back().acc);
            // This SCC is no longer trivial.
            root_.back().trivial = false;
          }
294
      }
295
296
297
298
299
    determine_usefulness();
  }

  void scc_info::determine_usefulness()
  {
300
301
    // An SCC is useful if it is not rejecting or it has a successor
    // SCC that is useful.
302
    unsigned scccount = scc_count();
303
    for (unsigned i = 0; i < scccount; ++i)
304
      {
305
306
307
308
309
310
311
312
313
314
315
316
        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;
            }
317
318
319
      }
  }

320

321
322
323
  std::set<acc_cond::mark_t> scc_info::used_acc_of(unsigned scc) const
  {
    std::set<acc_cond::mark_t> res;
324
325
    for (auto& t: inner_edges_of(scc))
      res.insert(t.acc);
326
327
328
    return res;
  }

329
  std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
330
  {
331
    unsigned n = aut_->num_states();
332
    std::vector<std::set<acc_cond::mark_t>> result(scc_count());
333
334
335

    for (unsigned src = 0; src < n; ++src)
      {
336
337
338
339
340
341
342
343
344
345
        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);
          }
346
347
348
349
      }
    return result;
  }

350
351
352
353
354
355
  std::vector<bool> scc_info::weak_sccs() const
  {
    unsigned n = scc_count();
    std::vector<bool> result(scc_count());
    auto acc = used_acc();
    for (unsigned s = 0; s < n; ++s)
356
      result[s] = is_rejecting_scc(s) || acc[s].size() == 1;
357
358
359
    return result;
  }

360
361
362
  bdd scc_info::scc_ap_support(unsigned scc) const
  {
    bdd support = bddtrue;
363
364
    for (auto& t: edges_of(scc))
      support &= bdd_support(t.cond);
365
366
367
    return support;
  }

368
369
370
  void scc_info::determine_unknown_acceptance()
  {
    std::vector<bool> k;
371
    unsigned s = scc_count();
372
    bool changed = false;
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
    // iterate over SCCs in topological order
    do
      {
        --s;
        if (!is_rejecting_scc(s) && !is_accepting_scc(s))
          {
            if (!aut_->is_existential())
              throw std::runtime_error(
                  "scc_info::determine_unknown_acceptance() "
                  "does not support alternating automata");
            auto& node = node_[s];
            if (k.empty())
              k.resize(aut_->num_states());
            for (auto i: node.states_)
              k[i] = true;
            if (mask_keep_accessible_states(aut_, k, node.states_.front())
                ->is_empty())
              node.rejecting_ = true;
            else
              node.accepting_ = true;
            changed = true;
          }
      }
    while (s);
397
398
399
400
    if (changed)
      determine_usefulness();
  }

401
402
  std::ostream&
  dump_scc_info_dot(std::ostream& out,
403
                    const_twa_graph_ptr aut, scc_info* sccinfo)
404
405
406
407
408
409
410
411
412
413
414
415
416
417
  {
    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())
      {
418
419
        int state = q.front();
        q.pop();
420

421
        out << "  " << state << " [shape=box,"
422
            << (aut->acc().accepting(m->acc(state)) ? "style=bold," : "")
423
            << "label=\"" << state;
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
        {
          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);
          }
441
442
443
444
445
446
447
448
449
      }

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

}