determinize.cc 22.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015, 2016 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
#include <algorithm>
21
#include <deque>
22
#include <stack>
23
24
#include <utility>
#include <unordered_map>
25
26
#include <set>
#include <map>
27

28
29
30
31
32
33
34

#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/simulation.hh>
35

36
37
38

namespace spot
{
39
40
41
42
43
44
45
46
47
48
  namespace node_helper
  {
    using brace_t = unsigned;
    void renumber(std::vector<brace_t>& braces,
                  const std::vector<unsigned>& decr_by);
    void truncate_braces(std::vector<brace_t>& braces,
                         const std::vector<unsigned>& rem_succ_of,
                         std::vector<size_t>& nb_braces);
  };

49
  class safra_state final
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
  {
  public:
    using state_t = unsigned;
    using color_t = unsigned;
    using bdd_id_t = unsigned;
    using nodes_t = std::map<state_t, std::vector<node_helper::brace_t>>;
    using succs_t = std::vector<std::pair<safra_state, bdd_id_t>>;
    using safra_node_t = std::pair<state_t, std::vector<node_helper::brace_t>>;

    bool operator<(const safra_state& other) const;
    // Printh the number of states in each brace
    safra_state(state_t state_number, bool init_state = false,
                bool acceptance_scc = false);
    // Given a certain transition_label, compute all the successors of that
    // label, and return that new node.
    void
    compute_succs(const const_twa_graph_ptr& aut,
                  succs_t& res,
                  const scc_info& scc,
69
                  const std::vector<bdd>& implications,
70
71
72
                  const std::vector<bool>& is_connected,
                  std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num,
                  std::vector<bdd>& all_bdds,
73
74
                  bool use_scc,
                  bool use_simulation,
75
76
77
78
79
80
                  bool use_stutter) const;
    // Compute successor for transition ap
    safra_state
    compute_succ(const const_twa_graph_ptr& aut,
                 const bdd& ap,
                 const scc_info& scc,
81
                 const std::vector<bdd>& implications,
82
                 const std::vector<bool>& is_connected,
83
84
                 bool use_scc,
                 bool use_simulation) const;
85
86
87
    // The outermost brace of each node cannot be green
    void ungreenify_last_brace();
    // When a nodes a implies a node b, remove the node a.
88
    void merge_redundant_states(const std::vector<bdd>& implications,
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
                                const scc_info& scc,
                                const std::vector<bool>& is_connected);
    // Used when creating the list of successors
    // A new intermediate node is created with  src's braces and with dst as id
    // A merge is done if dst already existed in *this
    void update_succ(const std::vector<node_helper::brace_t>& braces,
                     state_t dst, const acc_cond::mark_t acc);
    // Return the emitted color, red or green
    color_t finalize_construction();
    // A list of nodes similar to the ones of a
    // safra tree.  These are constructed in the same way as the powerset
    // algorithm.
    nodes_t nodes_;
    // A counter that indicates the nomber of states within a brace.
    // This enables us to compute the red value
    std::vector<size_t> nb_braces_;
    // A bitfield to know if a brace can emit green.
    std::vector<bool> is_green_;
    color_t color_;
  };

110
111
  namespace
  {
112
113
    using power_set = std::map<safra_state, int>;
    const char* const sub[10] =
114
      {
115
116
117
118
119
120
121
122
123
124
        "\u2080",
        "\u2081",
        "\u2082",
        "\u2083",
        "\u2084",
        "\u2085",
        "\u2086",
        "\u2087",
        "\u2088",
        "\u2089",
125
      };
126
127
128
129
130
131
132
133
134
135
136
137
138

    std::string subscript(unsigned start)
    {
      std::string res;
      do
        {
          res = sub[start % 10] + res;
          start /= 10;
        }
      while (start);
      return res;
    }

139
140
141
142
143
144
145
146
147
    // Returns true if lhs has a smaller nesting pattern than rhs
    // If lhs and rhs are the same, return false.
    bool nesting_cmp(const std::vector<node_helper::brace_t>& lhs,
                     const std::vector<node_helper::brace_t>& rhs)
    {
      size_t m = std::min(lhs.size(), rhs.size());
      size_t i = 0;
      for (; i < m; ++i)
        {
148
149
          if (lhs[i] != rhs[i])
            return lhs[i] < rhs[i];
150
151
152
153
        }
      return lhs.size() > rhs.size();
    }

154
155
156
157
158
159
    // Used to remove all acceptance whos value is above and equal max_acc
    void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
    {
      assert(max_acc < 32);
      unsigned mask = (1 << max_acc) - 1;
      for (auto& t: aut->edges())
160
161
162
        {
          t.acc &= mask;
        }
163
164
165
166
167
168
    }

    struct compare
    {
      bool
      operator() (const safra_state::safra_node_t& lhs,
169
                  const safra_state::safra_node_t& rhs)
170
      {
171
        return lhs.second < rhs.second;
172
      }
173
    };
174

175
176
177
    // Return the sorteds nodes in ascending order
    std::vector<safra_state::safra_node_t>
    sorted_nodes(const safra_state::nodes_t& nodes)
178
    {
179
180
      std::vector<safra_state::safra_node_t> res;
      for (auto& n: nodes)
181
        res.emplace_back(n.first, n.second);
182
183
184
185
186
187
188
189
190
191
192
193
      std::sort(res.begin(), res.end(), compare());
      return res;
    }

    std::string
    nodes_to_string(const safra_state::nodes_t& states)
    {
      auto copy = sorted_nodes(states);
      std::ostringstream os;
      std::stack<unsigned> s;
      bool first = true;
      for (auto& n: copy)
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
        {
          auto it = n.second.begin();
          // Find brace on top of stack in vector
          // If brace is not present, then we close it as no other ones of that
          // type will be found since we ordered our vector
          while (!s.empty())
            {
              it = std::lower_bound(n.second.begin(), n.second.end(),
                                    s.top());
              if (it == n.second.end() || *it != s.top())
                {
                  os << subscript(s.top()) << '}';
                  s.pop();
                }
              else
                {
                  if (*it == s.top())
                    ++it;
                  break;
                }
            }
          // Add new braces
          while (it != n.second.end())
            {
              os << '{' << subscript(*it);
              s.push(*it);
              ++it;
              first = true;
            }
          if (!first)
            os << ' ';
          os << n.first;
          first = false;
        }
228
229
      // Finish unwinding stack to print last braces
      while (!s.empty())
230
231
232
233
        {
          os << subscript(s.top()) << '}';
          s.pop();
        }
234
235
236
237
238
239
240
241
      return os.str();
    }

    std::vector<std::string>*
    print_debug(std::map<safra_state, int>& states)
    {
      auto res = new std::vector<std::string>(states.size());
      for (auto& p: states)
242
        (*res)[p.second] = nodes_to_string(p.first.nodes_);
243
      return res;
244
    }
245

246
247
  }

248
249
250
251
252

  std::vector<bool> find_scc_paths(const scc_info& scc);

  safra_state
  safra_state::compute_succ(const const_twa_graph_ptr& aut,
253
254
                            const bdd& ap,
                            const scc_info& scc,
255
                            const std::vector<bdd>& implications,
256
257
258
                            const std::vector<bool>& is_connected,
                            bool use_scc,
                            bool use_simulation) const
259
260
261
  {
    safra_state ss = safra_state(nb_braces_.size());
    for (auto& node: nodes_)
262
      {
263
264
265
266
267
268
269
270
        for (auto& t: aut->out(node.first))
          {
            if (!bdd_implies(ap, t.cond))
              continue;
            // Check if we are leaving the SCC, if so we delete all the
            // braces as no cycles can be found with that node
            if (use_scc && scc.scc_of(node.first) != scc.scc_of(t.dst))
              if (scc.is_accepting_scc(scc.scc_of(t.dst)))
271
272
                // Entering accepting SCC so add brace
                ss.update_succ({ /* no braces */ }, t.dst, { 0 });
273
274
275
276
277
278
279
              else
                // When entering non accepting SCC don't create any braces
                ss.update_succ({ /* no braces */ }, t.dst, { /* empty */ });
            else
              ss.update_succ(node.second, t.dst, t.acc);
            assert(ss.nb_braces_.size() == ss.is_green_.size());
          }
280
      }
281
    if (use_simulation)
282
283
284
285
      ss.merge_redundant_states(implications, scc, is_connected);
    ss.ungreenify_last_brace();
    ss.color_ = ss.finalize_construction();
    return ss;
286
  }
287

288
289
  void
  safra_state::compute_succs(const const_twa_graph_ptr& aut,
290
291
                             succs_t& res,
                             const scc_info& scc,
292
                             const std::vector<bdd>& implications,
293
294
295
296
297
298
299
                             const std::vector<bool>& is_connected,
                             std::unordered_map<bdd, unsigned, bdd_hash>&
                             bdd2num,
                             std::vector<bdd>& all_bdds,
                             bool use_scc,
                             bool use_simulation,
                             bool use_stutter) const
300
  {
301
302
    for (auto& ap: all_bdds)
      {
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
        safra_state ss = *this;

        if (use_stutter && aut->prop_stutter_invariant())
          {
            std::vector<color_t> colors;
            unsigned int counter = 0;
            std::map<safra_state, unsigned int> safra2id;
            bool stop = false;
            while (!stop)
              {
                auto pair = safra2id.insert({ss, counter++});
                // insert should never fail
                assert(pair.second);
                ss = ss.compute_succ(aut, ap, scc, implications, is_connected,
                                     use_scc, use_simulation);
                colors.push_back(ss.color_);
                stop = safra2id.find(ss) != safra2id.end();
              }
            // Add color of final transition that loops back
            colors.push_back(ss.color_);
            unsigned int loop_start = safra2id[ss];
            for (auto& min: safra2id)
              {
                if (min.second >= loop_start && ss < min.first)
                  ss = min.first;
              }
            ss.color_ = *std::min_element(colors.begin(), colors.end());
          }
        else
          ss = compute_succ(aut, ap, scc, implications, is_connected,
                            use_scc, use_simulation);
        unsigned bdd_idx = bdd2num[ap];
        res.emplace_back(ss, bdd_idx);
336
      }
337
338
  }

339
  void
340
  safra_state::merge_redundant_states(const std::vector<bdd>& implications,
341
342
343
344
345
346
347
348
349
350
351
352
                                      const scc_info& scc,
                                      const std::vector<bool>& is_connected)
  {
    std::vector<int> to_remove;
    for (auto& n1: nodes_)
      {
        for (auto& n2: nodes_)
          {
            if (n1 == n2)
              continue;
            // index to see if there is a path from scc2 -> scc1
            unsigned idx = scc.scc_count() * scc.scc_of(n2.first) +
353
              scc.scc_of(n1.first);
354
355
            if (bdd_implies(implications.at(n1.first),
                            implications.at(n2.first)) && !is_connected[idx])
356
357
358
              {
                to_remove.push_back(n1.first);
              }
359
360
361
362
363
364
365
366
367
368
369
370
          }
      }
    for (auto& n: to_remove)
      {
        for (auto& brace: nodes_[n])
          {
            --nb_braces_[brace];
          }
        nodes_.erase(n);
      }
  }

371
372
373
374
375
  void safra_state::ungreenify_last_brace()
  {
    // Step A4: For a brace to emit green it must surround other braces.
    // Hence, the last brace cannot emit green as it is the most inside brace.
    for (auto& n: nodes_)
376
377
378
379
      {
        if (!n.second.empty())
          is_green_[n.second.back()] = false;
      }
380
381
  }

382
  safra_state::color_t safra_state::finalize_construction()
383
  {
384
385
    unsigned red = -1U;
    unsigned green = -1U;
386
387
388
    std::vector<unsigned> rem_succ_of;
    assert(is_green_.size() == nb_braces_.size());
    for (unsigned i = 0; i < is_green_.size(); ++i)
389
390
391
      {
        if (nb_braces_[i] == 0)
          {
392
            // Step A3: Brackets that do not contain any nodes emit red
393
            is_green_[i] = false;
394
395
396
397

            // First brace can now be zero with new optim making it possible to
            // emit red 0
            red = std::min(red, 2 * i);
398
          }
399
400
        else if (is_green_[i])
          {
401
            green = std::min(green, 2 * i + 1);
402
403
404
            // Step A4 Emit green
            rem_succ_of.emplace_back(i);
          }
405
406
407
      }
    for (auto& n: nodes_)
      {
408
        // Step A4 Remove all brackets inside each green pair
409
        node_helper::truncate_braces(n.second, rem_succ_of, nb_braces_);
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
      }

    // Step A5 define the rem variable
    std::vector<unsigned> decr_by(nb_braces_.size());
    unsigned decr = 0;
    for (unsigned i = 0; i < nb_braces_.size(); ++i)
      {
        // Step A5 renumber braces
        nb_braces_[i - decr] = nb_braces_[i];
        if (nb_braces_[i] == 0)
          {
            ++decr;
          }
        // Step A5, renumber braces
        decr_by[i] = decr;
      }
    nb_braces_.resize(nb_braces_.size() - decr);
    for (auto& n: nodes_)
      {
429
        node_helper::renumber(n.second, decr_by);
430
      }
431
    return std::min(red, green);
432
433
  }

434
435
  void node_helper::renumber(std::vector<brace_t>& braces,
                             const std::vector<unsigned>& decr_by)
436
  {
437
    for (unsigned idx = 0; idx < braces.size(); ++idx)
438
      {
439
        braces[idx] -= decr_by[braces[idx]];
440
441
442
443
      }
  }

  void
444
  node_helper::truncate_braces(std::vector<brace_t>& braces,
445
446
                               const std::vector<unsigned>& rem_succ_of,
                               std::vector<size_t>& nb_braces)
447
  {
448
    for (unsigned idx = 0; idx < braces.size(); ++idx)
449
450
451
452
453
      {
        bool found = false;
        // find first brace that matches rem_succ_of
        for (auto s: rem_succ_of)
          {
454
            found |= braces[idx] == s;
455
456
457
          }
        if (found)
          {
458
            assert(idx < braces.size() - 1);
459
460
            // For each deleted brace, decrement elements of nb_braces
            // This corresponds to A4 step
461
            for (unsigned i = idx + 1; i < braces.size(); ++i)
462
              {
463
                --nb_braces[braces[i]];
464
              }
465
            braces.resize(idx + 1);
466
467
468
469
470
            break;
          }
      }
  }

471
  void safra_state::update_succ(const std::vector<node_helper::brace_t>& braces,
472
                                state_t dst, const acc_cond::mark_t acc)
473
  {
474
475
476
    std::vector<node_helper::brace_t> copy = braces;
    if (acc.count())
      {
477
        assert(acc.has(0) && acc.count() == 1 && "Only TBA are accepted");
478
        // Accepting edge generate new braces: step A1
479
480
481
482
483
484
485
486
487
        copy.emplace_back(nb_braces_.size());
        // nb_braces_ gets updated later so put 0 for now
        nb_braces_.emplace_back(0);
        // Newly created braces cannot emit green as they won't have
        // any braces inside them (by construction)
        is_green_.push_back(false);
      }
    auto i = nodes_.emplace(dst, copy);
    if (!i.second)
488
      {
489
490
491
        // Step A2: Only keep the smallest nesting pattern (i-e  braces_) for
        // identical nodes.  Nesting_cmp returnes true if copy is smaller
        if (nesting_cmp(copy, i.first->second))
492
          {
493
494
495
496
            // Remove brace count of replaced node
            for (auto b: i.first->second)
              --nb_braces_[b];
            i.first->second = std::move(copy);
497
498
          }
        else
499
          // Node already exists and has bigger nesting pattern value
500
501
          return;
      }
502
503
504
    // After inserting new node, update the brace count per node
    for (auto b: i.first->second)
      ++nb_braces_[b];
505
506
507
  }

  // Called only to initialize first state
508
  safra_state::safra_state(state_t val, bool init_state, bool accepting_scc)
509
510
511
512
  {
    if (init_state)
      {
        unsigned state_num = val;
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
        if (!accepting_scc)
          {
            std::vector<node_helper::brace_t> braces = { /* no braces */ };
            nodes_.emplace(state_num, std::move(braces));
          }
        else
          {
            std::vector<node_helper::brace_t> braces = { 0 };
            nodes_.emplace(state_num, std::move(braces));
            // First brace has init_state hence one state inside the first
            // braces.
            nb_braces_.push_back(1);
            // One brace set
            is_green_.push_back(true);
          }
528
529
530
531
532
      }
    else
      {
        unsigned nb_braces = val;
        // One brace set
533
        is_green_.assign(nb_braces, true);
534
        // Newly created states are the empty mocrstate
535
536
537
538
539
        nb_braces_.assign(nb_braces, 0);
      }
  }

  bool
540
  safra_state::operator<(const safra_state& other) const
541
  {
542
543
544
545
546
547
548
549
550
551
552
553
    if (nodes_ == other.nodes_)
      {
        for (auto& n: nodes_)
          {
            auto it = other.nodes_.find(n.first);
            assert(it != other.nodes_.end());
            if (nesting_cmp(n.second, it->second))
              return true;
          }
        return false;
      }

554
    return nodes_ < other.nodes_;
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
  std::vector<bool>
  find_scc_paths(const scc_info& scc)
  {
    unsigned scccount = scc.scc_count();
    std::vector<bool> res(scccount * scccount, 0);
    for (unsigned i = 0; i < scccount; ++i)
      res[i + scccount * i] = 1;
    for (unsigned i = 0; i < scccount; ++i)
      {
        std::stack<unsigned> s;
        s.push(i);
        while (!s.empty())
          {
            unsigned src = s.top();
            s.pop();
            for (auto& d: scc.succ(src))
              {
                s.push(d);
                unsigned idx = scccount * i + d;
                res[idx] = 1;
              }
          }
      }
    return res;
  }

583
  twa_graph_ptr
584
  tgba_determinize(const const_twa_graph_ptr& a,
585
586
                   bool pretty_print, bool use_scc,
                   bool use_simulation, bool use_stutter)
587
  {
588
589
590
    if (a->prop_deterministic())
      return std::const_pointer_cast<twa_graph>(a);

591
    // Degeneralize
592
    twa_graph_ptr aut = spot::degeneralize_tba(a);
593
    std::vector<bdd> implications;
594
    if (use_simulation)
595
596
597
598
      {
        aut = spot::scc_filter(aut);
        aut = simulation(aut, &implications);
      }
599
    scc_info scc = scc_info(aut);
600
    std::vector<bool> is_connected = find_scc_paths(scc);
601
602
603
604
605
606

    bdd allap = bddtrue;
    {
      typedef std::set<bdd, bdd_less_than> sup_map;
      sup_map sup;
      // Record occurrences of all guards
607
      for (auto& t: aut->edges())
608
609
610
611
612
613
614
615
616
617
618
619
        sup.emplace(t.cond);
      for (auto& i: sup)
        allap &= bdd_support(i);
    }

    // Preprocessing
    // Used to convert atomic bdd to id
    std::unordered_map<bdd, unsigned, bdd_hash> bdd2num;
    std::vector<bdd> num2bdd;
    // Nedded for compute succs
    // Used to convert large bdd to indexes
    std::unordered_map<bdd, std::pair<unsigned, unsigned>, bdd_hash> deltas;
620
    std::vector<safra_state::bdd_id_t> bddnums;
621
    for (auto& t: aut->edges())
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
      {
        auto it = deltas.find(t.cond);
        if (it == deltas.end())
          {
            bdd all = t.cond;
            unsigned prev = bddnums.size();
            while (all != bddfalse)
              {
                bdd one = bdd_satoneset(all, allap, bddfalse);
                all -= one;
                auto p = bdd2num.emplace(one, num2bdd.size());
                if (p.second)
                  num2bdd.push_back(one);
                bddnums.emplace_back(p.first->second);
              }
            deltas[t.cond] = std::make_pair(prev, bddnums.size());
          }
      }

641
642
643
    auto res = make_twa_graph(aut->get_dict());
    res->copy_ap_of(aut);
    res->prop_copy(aut,
644
                   { false, // state based
645
646
647
648
                       false, // inherently_weak
                       false, // deterministic
                       true // stutter inv
                       });
649
650

    // Given a safra_state get its associated state in output automata.
651
    // Required to create new edges from 2 safra-state
652
    power_set seen;
653
    auto init_state = aut->get_init_state_number();
654
655
    bool start_accepting =
      !use_scc || scc.is_accepting_scc(scc.scc_of(init_state));
656
    safra_state init(init_state, true, start_accepting);
657
658
659
660
661
    unsigned num = res->new_state();
    res->set_init_state(num);
    seen.insert(std::make_pair(init, num));
    std::deque<safra_state> todo;
    todo.push_back(init);
662
    unsigned sets = 0;
663
664
    using succs_t = safra_state::succs_t;
    succs_t succs;
665
666
667
668
669
    while (!todo.empty())
      {
        safra_state curr = todo.front();
        unsigned src_num = seen.find(curr)->second;
        todo.pop_front();
670
        curr.compute_succs(aut, succs, scc, implications, is_connected,
671
                           bdd2num, num2bdd, use_scc, use_simulation,
672
                           use_stutter);
673
674
        for (auto s: succs)
          {
675
            // Don't construct sink state as complete does a better job at this
676
            if (s.first.nodes_.empty())
677
              continue;
678
            auto i = seen.find(s.first);
679
680
681
682
683
684
685
            unsigned dst_num;
            if (i != seen.end())
              {
                dst_num = i->second;
              }
            else
              {
686
687
688
689
                dst_num = res->new_state();
                todo.push_back(s.first);
                seen.insert(std::make_pair(s.first, dst_num));
              }
690
            if (s.first.color_ != -1U)
691
              {
692
                res->new_edge(src_num, dst_num, num2bdd[s.second],
693
                              {s.first.color_});
694
695
                // We only care about green acc which are odd
                if (s.first.color_ % 2 == 1)
696
697
                  sets = std::max(s.first.color_ + 1, sets);
              }
698
            else
699
              res->new_edge(src_num, dst_num, num2bdd[s.second]);
700
          }
701
        succs.clear();
702
      }
703
    remove_dead_acc(res, sets);
704
705
    // Acceptance is now min(odd) since we con emit Red on paths 0 with new opti
    res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
706
    res->prop_deterministic(true);
707
    res->prop_state_acc(false);
708

709
710
    if (pretty_print)
      res->set_named_prop("state-names", print_debug(seen));
711
712
713
    return res;
  }
}