complete.cc 4.88 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// 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 <spot/twaalgos/complete.hh>
21
22
23

namespace spot
{
24
  unsigned complete_here(twa_graph_ptr aut)
25
  {
26
27
    unsigned n = aut->num_states();
    unsigned sink = -1U;
28
29
30
31

    // UM is a pair (bool, mark).  If the Boolean is false, the
    // acceptance is always satisfiable.  Otherwise, MARK is an
    // example of unsatisfiable mark.
32
    auto um = aut->acc().unsat_mark();
33
    if (!um.first)
34
      {
35
36
37
38
39
        // We cannot safely complete an automaton if its
        // acceptance is always satisfiable.
        auto acc = aut->set_buchi();
        for (auto& t: aut->edge_vector())
          t.acc = acc;
40
      }
41
    else
42
      {
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
        // Loop over the states and search a state that has only self
        // loop labeled by the same non-accepting mark.  This will be
        // our sink state.  Note that we do not even have to ensure
        // that the state is complete as we will complete the whole
        // automaton in a second pass.
        for (unsigned i = 0; i < n; ++i)
          {
            bool sinkable = true;
            bool first = true;
            acc_cond::mark_t commonacc = 0U;
            for (auto& t: aut->out(i))
              {
                if (t.dst != i)        // Not a self-loop
                  {
                    sinkable = false;
                    break;
                  }
                if (first)
                  {
                    commonacc = t.acc;
                    first = false;
                  }
                else if (t.acc != commonacc)
                  {
                    sinkable = false;
                    break;
                  }
              }
            if (sinkable && !aut->acc().accepting(commonacc))
              {
                // We have found a sink!
                um.second = commonacc;
                sink = i;
                break;
              }
          }
79
80
      }

81
    unsigned t = aut->num_edges();
82

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
83
    // If the automaton is empty, pretend that state 0 is a sink.
84
    if (t == 0)
85
      sink = aut->get_init_state_number();
86

87
    // Now complete all states (excluding any newly added the sink).
88
    for (unsigned i = 0; i < n; ++i)
89
      {
90
91
92
93
94
95
96
97
98
99
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
        bdd missingcond = bddtrue;
        acc_cond::mark_t acc = 0U;
        for (auto& t: aut->out(i))
          {
            missingcond -= t.cond;
            // FIXME: This is ugly.
            //
            // In case the automaton uses state-based acceptance, we
            // need to put the new edge in the same set as all
            // the other.
            //
            // In case the automaton uses edge-based acceptance,
            // it does not matter what acceptance set we put the new
            // edge into.
            //
            // So in both cases, we put the edge in the same
            // acceptance sets as the last outgoing edge of the
            // state.
            acc = t.acc;
          }
        // If the state has incomplete successors, we need to add a
        // edge to some sink state.
        if (missingcond != bddfalse)
          {
            // If we haven't found any sink, simply add one.
            if (sink == -1U)
              {
                sink = aut->new_state();
                aut->new_edge(sink, sink, bddtrue, um.second);
              }
            // In case the automaton use state-based acceptance, propagate
            // the acceptance of the first edge to the one we add.
            if (aut->prop_state_acc() != true)
              acc = 0U;
            aut->new_edge(i, sink, missingcond, acc);
          }
126
      }
127
128

    // Get rid of any named property if the automaton changed.
129
    if (t < aut->num_edges())
130
131
      aut->release_named_properties();
    else
132
      assert(t == aut->num_edges());
133

134
135
    return sink;
  }
136

137
  twa_graph_ptr complete(const const_twa_ptr& aut)
138
  {
139
    auto res = make_twa_graph(aut, {
140
141
142
143
144
                                        true, // state based
                                        true, // inherently_weak
                                        true, // deterministic
                                        true, // stutter inv.
                                      });
145
    complete_here(res);
146
    return res;
147
148
  }

149
}