sccinfo.cc 14.2 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
43
      acc_cond::mark_t in_acc;  // Acceptance sets on the incoming transition
      acc_cond::mark_t acc = 0U; // union of all acceptance sets in the SCC
44
45
46
      int index;                // Index of the SCC
      bool trivial = true;        // Whether the SCC has no cycle
      bool accepting = false;        // Necessarily accepting
47
48
49
    };
  }

50
  scc_info::scc_info(const_twa_graph_ptr aut)
51
    : aut_(aut)
52
53
54
55
  {
    unsigned n = aut->num_states();
    sccof_.resize(n, -1U);

56
    std::deque<unsigned> live;
57
    std::deque<scc> root_;        // Stack of SCC roots.
58
59
60
61
62
    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.

63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
    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();

    // Setup depth-first search from the initial state.  But we may
    // have a conjunction of initial state in alternating automata.
    for (unsigned init: aut->univ_dests(aut->get_init_state_number()))
80
      {
81
82
83
84
85
86
87
88
        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);
89

90
        while (!todo_.empty())
91
          {
92
93
            // We are looking at the next successor in SUCC.
            unsigned tr_succ = todo_.top().out_edge;
94

95
96
97
98
99
            // If there is no more successor, backtrack.
            if (!tr_succ)
              {
                // We have explored all successors of state CURR.
                unsigned curr = todo_.top().src;
100

101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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
                // 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();
                    auto acc = root_.back().acc;
                    bool triv = root_.back().trivial;
                    node_.emplace_back(acc, triv);

                    // 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))
                          {
                            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;
                    bool reject = triv || !aut->acc().inf_satisfiable(acc);
                    // If the SCC acceptance is indeterminate, but has
                    // only self-loops with the same mark, it is
                    // necessarily rejecting, otherwise we would have
                    // found it to be accepting.
                    if (!accept && !reject && nbs.size() == 1)
                      {
                        acc_cond::mark_t selfacc = 0;
                        bool first = true;
                        reject = true;
                        for (const auto& e: aut->out(nbs.front()))
                          for (unsigned d: aut->univ_dests(e))
                            if (e.src == d)
                              {
                                if (first)
                                  {
                                    selfacc = e.acc;
                                    first = false;
                                  }
                                else if (selfacc != e.acc)
                                  {
                                    reject = false;
                                    goto break2;
                                  }
                              }
                      }
                  break2:
                    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);
            unsigned dest = e.dst;
            if ((int) dest < 0)
184
              {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
185
                // Iterate over all destinations of a universal edge.
186
187
188
189
190
191
                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)
192
                  {
193
194
                    todo_.top().out_edge = e.next_succ;
                    todo_.top().univ_pos = 0;
195
                  }
196
                else
197
                  {
198
                    ++todo_.top().univ_pos;
199
                  }
200
              }
201
202
203
204
            else
              {
                todo_.top().out_edge = e.next_succ;
              }
205

206
            auto acc = e.acc;
207

208
209
210
211
212
213
214
215
216
217
218
219
            // 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;
              }
220

221
            // We already know the state.
222

223
224
225
            // Have we reached a maximal SCC?
            if (spi > 0)
              continue;
226

227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
            // 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);
243
244

            assert(!root_.empty());
245
246
247
248
249
250
251
252
            while (threshold > root_.back().index)
              {
                acc |= root_.back().acc;
                acc |= root_.back().in_acc;
                is_accepting |= root_.back().accepting;
                root_.pop_back();
                assert(!root_.empty());
              }
253

254
255
256
257
258
259
260
261
262
263
264
265
266
            // 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.

            // Accumulate all acceptance conditions, states, SCC
            // successors, and conditions into the merged SCC.
            root_.back().acc |= acc;
            root_.back().accepting |= is_accepting
              || aut->acc().accepting(root_.back().acc);
            // This SCC is no longer trivial.
            root_.back().trivial = false;
          }
267
      }
268
269
270
271
272
    determine_usefulness();
  }

  void scc_info::determine_usefulness()
  {
273
274
    // An SCC is useful if it is not rejecting or it has a successor
    // SCC that is useful.
275
    unsigned scccount = scc_count();
276
    for (unsigned i = 0; i < scccount; ++i)
277
      {
278
279
280
281
282
283
284
285
286
287
288
289
        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;
            }
290
291
292
      }
  }

293

294
295
296
297
298
  std::set<acc_cond::mark_t> scc_info::used_acc_of(unsigned scc) const
  {
    std::set<acc_cond::mark_t> res;
    for (auto src: states_of(scc))
      for (auto& t: aut_->out(src))
299
300
        if (scc_of(t.dst) == scc)
          res.insert(t.acc);
301
302
303
    return res;
  }

304
305
306
307
308
  acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const
  {
    acc_cond::mark_t res = 0U;
    for (auto src: states_of(scc))
      for (auto& t: aut_->out(src))
309
310
        if (scc_of(t.dst) == scc)
          res |= t.acc;
311
312
313
    return res;
  }

314
  std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
315
  {
316
    unsigned n = aut_->num_states();
317
    std::vector<std::set<acc_cond::mark_t>> result(scc_count());
318
319
320

    for (unsigned src = 0; src < n; ++src)
      {
321
322
323
324
325
326
327
328
329
330
        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);
          }
331
332
333
334
      }
    return result;
  }

335
336
337
338
339
340
  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)
341
      result[s] = is_rejecting_scc(s) || acc[s].size() == 1;
342
343
344
    return result;
  }

345
346
347
348
349
  bdd scc_info::scc_ap_support(unsigned scc) const
  {
    bdd support = bddtrue;
    for (auto s: states_of(scc))
      for (auto& t: aut_->out(s))
350
        support &= bdd_support(t.cond);
351
352
353
    return support;
  }

354
355
  void scc_info::determine_unknown_acceptance()
  {
356
    if (!aut_->is_existential())
357
358
      throw std::runtime_error("scc_info::determine_unknown_acceptance() "
                               "does not support alternating automata");
359
360
361
362
363
    std::vector<bool> k;
    unsigned n = scc_count();
    bool changed = false;
    for (unsigned s = 0; s < n; ++s)
      if (!is_rejecting_scc(s) && !is_accepting_scc(s))
364
365
366
367
368
369
        {
          auto& node = node_[s];
          if (k.empty())
            k.resize(aut_->num_states());
          for (auto i: node.states_)
            k[i] = true;
370
371
          if (mask_keep_accessible_states(aut_, k, node.states_.front())
              ->is_empty())
372
373
374
375
376
            node.rejecting_ = true;
          else
            node.accepting_ = true;
          changed = true;
        }
377
378
379
380
    if (changed)
      determine_usefulness();
  }

381
382
  std::ostream&
  dump_scc_info_dot(std::ostream& out,
383
                    const_twa_graph_ptr aut, scc_info* sccinfo)
384
385
386
387
388
389
390
391
392
393
394
395
396
397
  {
    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())
      {
398
399
        int state = q.front();
        q.pop();
400

401
        out << "  " << state << " [shape=box,"
402
            << (aut->acc().accepting(m->acc(state)) ? "style=bold," : "")
403
            << "label=\"" << state;
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
        {
          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);
          }
421
422
423
424
425
426
427
428
429
      }

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

}