twagraph.cc 19 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
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
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
47
48
49
50
51
52
53
54
55
56
57
58
59
    /// \brief Merge universal destinations
    ///
    /// If several states have the same universal destination, merge
    /// them all.  Also remove unused destination, and any redundant
    /// state in each destination.
  void twa_graph::merge_univ_dests()
  {
    auto& g = get_graph();
    auto& dests = g.dests_vector();
    auto& edges = g.edge_vector();

    std::vector<unsigned> old_dests;
    std::swap(dests, old_dests);
    std::vector<unsigned> seen(old_dests.size(), -1U);
60
    internal::univ_dest_mapper<twa_graph::graph_t> uniq(g);
61
62
63
64
65
66
67
68
69

    auto fixup = [&](unsigned& in_dst)
      {
        unsigned dst = in_dst;
        if ((int) dst >= 0)       // not a universal edge
          return;
        dst = ~dst;
        unsigned& nd = seen[dst];
        if (nd == -1U)
70
71
          nd = uniq.new_univ_dests(old_dests.data() + dst + 1,
                                   old_dests.data() + dst + 1 + old_dests[dst]);
72
73
74
75
76
77
78
79
80
81
82
83
84
        in_dst = nd;
      };

    unsigned tend = edges.size();
    for (unsigned t = 1; t < tend; t++)
      {
        if (g.is_dead_edge(t))
          continue;
        fixup(edges[t].dst);
      }
    fixup(init_number_);
  }

85
  void twa_graph::merge_edges()
86
  {
87
    set_named_prop("highlight-edges", nullptr);
88
    g_.remove_dead_edges_();
89
    if (!is_existential())
90
      merge_univ_dests();
91

92
93
    typedef graph_t::edge_storage_t tr_t;
    g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
94
95
96
97
98
99
100
101
102
103
104
105
106
                   {
                     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.
                   });
107

108
    auto& trans = this->edge_vector();
109
110
111
    unsigned tend = trans.size();
    unsigned out = 0;
    unsigned in = 1;
112
    // Skip any leading false edge.
113
114
115
116
    while (in < tend && trans[in].cond == bddfalse)
      ++in;
    if (in < tend)
      {
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
        ++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];
              }
          }
141
      }
142
143
144
    if (++out != tend)
      trans.resize(out);

145
146
147
    tend = out;
    out = in = 2;

148
    // FIXME: We could should also merge edges when using
149
150
151
152
    // 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())
153
      {
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
        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.
                       });
169

170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
        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);
190
191
      }

192
    g_.chain_edges_();
193
194
  }

195
  void twa_graph::purge_unreachable_states()
196
197
  {
    unsigned num_states = g_.num_states();
198
199
200
201
202
203
204
205
206
207
    // 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;
208
209
210
211
212
213
    unsigned todo_pos = 0;
    for (unsigned i: univ_dests(get_init_state_number()))
      {
        todo[i] |= seen;
        todo[todo_pos++] |= i;
      }
214
    do
215
      {
216
217
218
        unsigned cur = todo[--todo_pos] & mask;
        todo[todo_pos] ^= cur;        // Zero the state
        for (auto& t: g_.out(cur))
219
220
221
222
223
224
          for (unsigned dst: univ_dests(t.dst))
            if (!(todo[dst] & seen))
              {
                todo[dst] |= seen;
                todo[todo_pos++] |= dst;
              }
225
      }
226
    while (todo_pos > 0);
227
228
    // Now renumber each used state.
    unsigned current = 0;
229
230
    for (auto& v: todo)
      if (!(v & seen))
231
        v = -1U;
232
      else
233
        v = current++;
234
    if (current == todo.size())
235
      return;                        // No unreachable state.
236
237

    // Removing some non-deterministic dead state could make the
238
239
240
    // automaton universal.
    if (prop_universal().is_false())
      prop_universal(trival::maybe());
241
242
243
    if (prop_complete().is_false())
      prop_complete(trival::maybe());

244
    defrag_states(std::move(todo), current);
245
246
  }

247
  void twa_graph::purge_dead_states()
248
249
  {
    unsigned num_states = g_.num_states();
250
251
252
253
254
    std::vector<unsigned> useful(num_states, 0);

    // Make a DFS to compute a topological order.
    std::vector<unsigned> order;
    order.reserve(num_states);
255

256
257
    bool purge_unreachable_needed = false;

258
    if (is_existential())
259
      {
260
261
262
263
        std::vector<std::pair<unsigned, unsigned>> todo; // state, edge
        useful[get_init_state_number()] = 1;
        todo.emplace_back(init_number_, g_.state_storage(init_number_).succ);
        do
264
          {
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
            unsigned src;
            unsigned tid;
            std::tie(src, tid) = todo.back();
            if (tid == 0U)
              {
                todo.pop_back();
                order.emplace_back(src);
                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;
              }
282
          }
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
        while (!todo.empty());
      }
    else
      {
        // state, edge, begin, end
        std::vector<std::tuple<unsigned, unsigned,
                               const unsigned*, const unsigned*>> todo;
        auto& dests = g_.dests_vector();

        auto beginend = [&](const unsigned& dst,
                            const unsigned*& begin, const unsigned*& end)
          {
            if ((int)dst < 0)
              {
                begin = dests.data() + ~dst + 1;
                end = begin + dests[~dst];
              }
            else
              {
                begin = &dst;
                end = begin + 1;
              }
          };
        {
          const unsigned* begin;
          const unsigned* end;
          beginend(init_number_, begin, end);
          todo.emplace_back(init_number_, 0U, begin, end);
        }

313
        for (;;)
314
          {
315
316
317
318
319
            unsigned& tid = std::get<1>(todo.back());
            const unsigned*& begin = std::get<2>(todo.back());
            const unsigned*& end = std::get<3>(todo.back());
            if (tid == 0U && begin == end)
              {
320
                unsigned src = std::get<0>(todo.back());
321
                todo.pop_back();
322
323
324
325
                // Last transition from a state?
                if ((int)src >= 0 && (todo.empty()
                                      || src != std::get<0>(todo.back())))
                  order.emplace_back(src);
326
327
                if (todo.empty())
                  break;
328
329
                else
                  continue;
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
              }
            unsigned dst = *begin++;
            if (begin == end)
              {
                if (tid != 0)
                  tid = g_.edge_storage(tid).next_succ;
                if (tid != 0)
                  beginend(g_.edge_storage(tid).dst, begin, end);
              }
            if (useful[dst] != 1)
              {
                auto& ss = g_.state_storage(dst);
                unsigned succ = ss.succ;
                if (succ == 0U)
                  continue;
                useful[dst] = 1;
                const unsigned* begin;
                const unsigned* end;
                beginend(g_.edge_storage(succ).dst, begin, end);
                todo.emplace_back(dst, succ, begin, end);
              }
351
          }
352
353
      }

354
355
356
    // At this point, all reachable states with successors are marked
    // as useful.
    for (;;)
357
      {
358
359
360
361
        bool univ_edge_erased = false;
        // Process states in topological order to mark those without
        // successors as useless.
        for (auto s: order)
362
          {
363
364
365
            auto t = g_.out_iteraser(s);
            bool useless = true;
            while (t)
366
              {
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
                // An edge is useful if all its
                // destinations are useful.
                bool usefuledge = true;
                for (unsigned d: univ_dests(t->dst))
                  if (!useful[d])
                    {
                      usefuledge = false;
                      break;
                    }
                // Erase any useless edge
                if (!usefuledge)
                  {
                    if (is_univ_dest(t->dst))
                      univ_edge_erased = true;
                    t.erase();
                    continue;
                  }
                // if we have a edge to a useful state, then the
                // state is useful.
                useless = false;
                ++t;
388
              }
389
390
            if (useless)
              useful[s] = 0;
391
          }
392
393
394
395
396
397
398
399
400
401
        // If we have erased any universal destination, it is possible
        // that we have have created some new dead states, so we
        // actually need to redo the whole thing again until there is
        // no more universal edge to remove.  Also we might have
        // created some unreachable states, so we will simply call
        // purge_unreachable_states() later to clean this.
        if (!univ_edge_erased)
          break;
        else
          purge_unreachable_needed = true;
402
403
      }

404
405
406
    // Is the initial state actually useful?  If not, make this an
    // empty automaton by resetting the graph.
    bool usefulinit = true;
407
    for (unsigned d: univ_dests(init_number_))
408
      if (!useful[d])
409
        {
410
          usefulinit = false;
411
412
413
          break;
        }
    if (!usefulinit)
414
415
416
417
418
419
420
421
422
      {
        g_ = graph_t();
        init_number_ = new_state();
        prop_universal(true);
        prop_complete(false);
        prop_stutter_invariant(true);
        prop_weak(true);
        return;
      }
423

424
    // Renumber each used state.
425
    unsigned current = 0;
426
427
    for (unsigned s = 0; s < num_states; ++s)
      if (useful[s])
428
        useful[s] = current++;
429
      else
430
        useful[s] = -1U;
431
    if (current == num_states)
432
      return;                        // No useless state.
433
434

    // Removing some non-deterministic dead state could make the
435
436
437
    // automaton universal.  Likewise for non-complete.
    if (prop_universal().is_false())
      prop_universal(trival::maybe());
438
439
440
    if (prop_complete().is_false())
      prop_complete(trival::maybe());

441
    defrag_states(std::move(useful), current);
442
443
444

    if (purge_unreachable_needed)
      purge_unreachable_states();
445
446
447
  }

  void twa_graph::defrag_states(std::vector<unsigned>&& newst,
448
                                unsigned used_states)
449
  {
450
    if (!is_existential())
451
      {
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
        // Running defrag_states() on alternating automata is tricky,
        // because we want to
        // #1 rename the regular states
        // #2 rename the states in universal destinations
        // #3 get rid of the unused universal destinations
        // #4 merge identical universal destinations
        //
        // graph::degrag_states() actually does only #1. It it could
        // do #2, but that would prevent use from doing #3 and #4.  It
        // cannot do #3 and #4 because the graph object does not know
        // what an initial state is, and our initial state might be
        // universal.
        //
        // As a consequence this code preforms #2, #3, and #4 before
        // calling graph::degrag_states() to finish with #1.  We clear
        // the "dests vector" of the current automaton, recreate all
        // the new destination groups using a univ_dest_mapper to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
469
        // simplify and unify them, and extend newst with some new
470
471
472
        // entries that will point the those new universal destination
        // so that graph::defrag_states() does not have to deal with
        // universal destination in any way.
473
474
475
        auto& g = get_graph();
        auto& dests = g.dests_vector();

476
        // Clear the destination vector, saving the old one.
477
478
        std::vector<unsigned> old_dests;
        std::swap(dests, old_dests);
479
480
        // dests will be updated as a side effect of declaring new
        // destination groups to uniq.
481
482
        internal::univ_dest_mapper<twa_graph::graph_t> uniq(g);

483
484
485
486
487
488
489
490
491
        // The newst entry associated to each of the old destination
        // group.
        std::vector<unsigned> seen(old_dests.size(), -1U);

        // Rename a state if it denotes a universal destination.  This
        // function has to be applied to the destination of each edge,
        // as well as to the initial state.  The need to work on the
        // initial state is the reason it cannot be implemented in
        // graph::defrag_states().
492
493
494
495
496
497
498
        auto fixup = [&](unsigned& in_dst)
          {
            unsigned dst = in_dst;
            if ((int) dst >= 0)       // not a universal edge
              return;
            dst = ~dst;
            unsigned& nd = seen[dst];
499
            if (nd == -1U)      // An unprocessed destination group
500
              {
501
                // store all renamed destination states in tmp
502
503
504
505
506
507
508
509
510
511
512
513
                std::vector<unsigned> tmp;
                auto begin = old_dests.data() + dst + 1;
                auto end = begin + old_dests[dst];
                while (begin != end)
                  {
                    unsigned n = newst[*begin++];
                    if (n == -1U)
                      continue;
                    tmp.emplace_back(n);
                  }
                if (tmp.empty())
                  {
514
515
516
                    // All destinations of this group were marked for
                    // removal.  Mark this universal transition for
                    // removal as well.  Is this really what we expect?
517
518
519
520
                    nd = -1U;
                  }
                else
                  {
521
522
523
524
                    // register this new destination group, add et two
                    // newst, and use the index in newst to relabel
                    // the state so that graph::degrag_states() will
                    // eventually update it to the correct value.
525
526
527
528
529
530
531
532
533
534
535
536
                    nd = newst.size();
                    newst.emplace_back(uniq.new_univ_dests(tmp.begin(),
                                                           tmp.end()));
                  }
              }
            in_dst = nd;
          };
        fixup(init_number_);
        for (auto& e: edges())
          fixup(e.dst);
      }

537
    if (auto* names = get_named_prop<std::vector<std::string>>("state-names"))
538
      {
539
540
541
542
543
544
545
546
547
        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);
548
      }
549
550
551
552
553
554
555
556
557
558
559
560
    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);
      }
561
    init_number_ = newst[init_number_];
562
    g_.defrag_states(std::move(newst), used_states);
563
  }
564
565
566
567
568
569
570
571
572
573

  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));
574
        if (all == bddtrue)    // All APs are used.
575
576
577
578
579
580
581
582
583
584
585
          return;
      }
    auto d = get_dict();
    while (all != bddtrue)
      {
        unregister_ap(bdd_var(all));
        all = bdd_high(all);
      }
  }


586
}