twagraph.cc 9.55 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement de
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// l'Epita.
//
// 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
21
#include <spot/twa/twagraph.hh>
#include <spot/tl/print.hh>
22
23
24

namespace spot
{
25
  void
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
26
  twa_graph::release_formula_namer(namer<formula>* namer,
27
                                   bool keep_names)
28
29
30
  {
    if (keep_names)
      {
31
32
33
34
35
36
37
38
39
40
41
        auto v = new std::vector<std::string>(num_states());
        auto& n = namer->names();
        unsigned ns = n.size();
        assert(n.size() <= v->size());
        for (unsigned i = 0; i < ns; ++i)
          {
            auto f = n[i];
            if (f)
              (*v)[i] = str_psl(f);
          }
        set_named_prop("state-names", v);
42
43
44
      }
    delete namer;
  }
45

46
  void twa_graph::merge_edges()
47
  {
48
    set_named_prop("highlight-edges", nullptr);
49
    g_.remove_dead_edges_();
50

51
52
    typedef graph_t::edge_storage_t tr_t;
    g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
53
54
55
56
57
58
59
60
61
62
63
64
65
                   {
                     if (lhs.src < rhs.src)
                       return true;
                     if (lhs.src > rhs.src)
                       return false;
                     if (lhs.dst < rhs.dst)
                       return true;
                     if (lhs.dst > rhs.dst)
                       return false;
                     return lhs.acc < rhs.acc;
                     // Do not sort on conditions, we'll merge
                     // them.
                   });
66

67
    auto& trans = this->edge_vector();
68
69
70
    unsigned tend = trans.size();
    unsigned out = 0;
    unsigned in = 1;
71
    // Skip any leading false edge.
72
73
74
75
    while (in < tend && trans[in].cond == bddfalse)
      ++in;
    if (in < tend)
      {
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
        ++out;
        if (out != in)
          trans[out] = trans[in];
        for (++in; in < tend; ++in)
          {
            if (trans[in].cond == bddfalse) // Unusable edge
              continue;
            // Merge edges with the same source, destination, and
            // acceptance.  (We test the source last, because this is the
            // most likely test to be true as edges are ordered by
            // sources and then destinations.)
            if (trans[out].dst == trans[in].dst
                && trans[out].acc == trans[in].acc
                && trans[out].src == trans[in].src)
              {
                trans[out].cond |= trans[in].cond;
              }
            else
              {
                ++out;
                if (in != out)
                  trans[out] = trans[in];
              }
          }
100
      }
101
102
103
    if (++out != tend)
      trans.resize(out);

104
105
106
    tend = out;
    out = in = 2;

107
    // FIXME: We could should also merge edges when using
108
109
110
111
    // fin_acceptance, but the rule for Fin sets are different than
    // those for Inf sets, (and we need to be careful if a set is used
    // both as Inf and Fin)
    if ((in < tend) && !acc().uses_fin_acceptance())
112
      {
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
        typedef graph_t::edge_storage_t tr_t;
        g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
                       {
                         if (lhs.src < rhs.src)
                           return true;
                         if (lhs.src > rhs.src)
                           return false;
                         if (lhs.dst < rhs.dst)
                           return true;
                         if (lhs.dst > rhs.dst)
                           return false;
                         return lhs.cond.id() < rhs.cond.id();
                         // Do not sort on acceptance, we'll merge
                         // them.
                       });
128

129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
        for (; in < tend; ++in)
          {
            // Merge edges with the same source, destination,
            // and conditions.  (We test the source last, for the
            // same reason as above.)
            if (trans[out].dst == trans[in].dst
                && trans[out].cond.id() == trans[in].cond.id()
                && trans[out].src == trans[in].src)
              {
                trans[out].acc |= trans[in].acc;
              }
            else
              {
                ++out;
                if (in != out)
                  trans[out] = trans[in];
              }
          }
        if (++out != tend)
          trans.resize(out);
149
150
      }

151
    g_.chain_edges_();
152
153
  }

154
  void twa_graph::purge_unreachable_states()
155
156
  {
    unsigned num_states = g_.num_states();
157
158
159
160
161
162
163
164
165
166
    // The TODO vector serves two purposes:
    // - it is a stack of state to process,
    // - it is a set of processed states.
    // The lower 31 bits of each entry is a state on the stack. (The
    // next usable entry on the stack is indicated by todo_pos.)  The
    // 32th bit (i.e., the sign bit) of todo[x] indicates whether
    // states number x has been seen.
    std::vector<unsigned> todo(num_states, 0);
    const unsigned seen = 1 << (sizeof(unsigned)*8-1);
    const unsigned mask = seen - 1;
167
    todo[0] = get_init_state_number();
168
169
170
    todo[init_number_] |= seen;
    unsigned todo_pos = 1;
    do
171
      {
172
173
174
175
176
177
178
179
        unsigned cur = todo[--todo_pos] & mask;
        todo[todo_pos] ^= cur;        // Zero the state
        for (auto& t: g_.out(cur))
          if (!(todo[t.dst] & seen))
            {
              todo[t.dst] |= seen;
              todo[todo_pos++] |= t.dst;
            }
180
      }
181
    while (todo_pos > 0);
182
183
    // Now renumber each used state.
    unsigned current = 0;
184
185
    for (auto& v: todo)
      if (!(v & seen))
186
        v = -1U;
187
      else
188
        v = current++;
189
    if (current == todo.size())
190
      return;                        // No unreachable state.
191
    init_number_ = todo[init_number_];
192
    defrag_states(std::move(todo), current);
193
194
  }

195
  void twa_graph::purge_dead_states()
196
197
  {
    unsigned num_states = g_.num_states();
198
199
200
201
202
203
    std::vector<unsigned> useful(num_states, 0);

    // Make a DFS to compute a topological order.
    std::vector<unsigned> order;
    order.reserve(num_states);
    std::vector<std::pair<unsigned, unsigned>> todo; // state, trans
204
    useful[get_init_state_number()] = 1;
205
    todo.emplace_back(init_number_, g_.state_storage(init_number_).succ);
206
207
    do
      {
208
209
210
211
212
213
        unsigned src;
        unsigned tid;
        std::tie(src, tid) = todo.back();
        if (tid == 0U)
          {
            todo.pop_back();
214
            order.emplace_back(src);
215
216
217
218
219
220
221
222
223
224
            continue;
          }
        auto& t = g_.edge_storage(tid);
        todo.back().second = t.next_succ;
        unsigned dst = t.dst;
        if (useful[dst] != 1)
          {
            todo.emplace_back(dst, g_.state_storage(dst).succ);
            useful[dst] = 1;
          }
225
226
227
228
229
230
      }
    while (!todo.empty());

    // Process states in topological order
    for (auto s: order)
      {
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
        auto t = g_.out_iteraser(s);
        bool useless = true;
        while (t)
          {
            // Erase any edge to a useless state.
            if (!useful[t->dst])
              {
                t.erase();
                continue;
              }
            // if we have a edge to a useful state, then the
            // state is useful.
            useless = false;
            ++t;
          }
        if (useless)
          useful[s] = 0;
248
249
      }

250
251
252
253
254
    // Make sure the initial state is useful (even if it has been
    // marked as useless by the previous loop because it has no
    // successor).
    useful[init_number_] = 1;

255
256
    // Now renumber each used state.
    unsigned current = 0;
257
258
    for (unsigned s = 0; s < num_states; ++s)
      if (useful[s])
259
        useful[s] = current++;
260
      else
261
        useful[s] = -1U;
262
    if (current == num_states)
263
      return;                        // No useless state.
264
    init_number_ = useful[init_number_];
265
266
267
268
    defrag_states(std::move(useful), current);
  }

  void twa_graph::defrag_states(std::vector<unsigned>&& newst,
269
                                unsigned used_states)
270
  {
271
    if (auto* names = get_named_prop<std::vector<std::string>>("state-names"))
272
      {
273
274
275
276
277
278
279
280
281
        unsigned size = names->size();
        for (unsigned s = 0; s < size; ++s)
          {
            unsigned dst = newst[s];
            if (dst == s || dst == -1U)
              continue;
            (*names)[dst] = std::move((*names)[s]);
          }
        names->resize(used_states);
282
      }
283
284
285
286
287
288
289
290
291
292
293
294
    if (auto hs = get_named_prop<std::map<unsigned, unsigned>>
        ("highlight-states"))
      {
        std::map<unsigned, unsigned> hs2;
        for (auto p: *hs)
          {
            unsigned dst = newst[p.first];
            if (dst != -1U)
              hs2[dst] = p.second;
          }
        std::swap(*hs, hs2);
      }
295
    g_.defrag_states(std::move(newst), used_states);
296
  }
297
298
299
300
301
302
303
304
305
306

  void twa_graph::remove_unused_ap()
  {
    if (ap().empty())
      return;
    std::set<bdd> conds;
    bdd all = ap_vars();
    for (auto& e: g_.edges())
      {
        all = bdd_exist(all, bdd_support(e.cond));
307
        if (all == bddtrue)    // All APs are used.
308
309
310
311
312
313
314
315
316
317
318
          return;
      }
    auto d = get_dict();
    while (all != bddtrue)
      {
        unregister_ap(bdd_var(all));
        all = bdd_high(all);
      }
  }


319
}