complete.cc 6.19 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013-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
#include <spot/twaalgos/complete.hh>
21
22
23

namespace spot
{
24
  void complete_here(twa_graph_ptr aut)
25
  {
26
    unsigned sink = -1U;
27
28
29
    if (aut->prop_complete().is_true())
      return;
    unsigned n = aut->num_states();
30
31
32
33

    // UM is a pair (bool, mark).  If the Boolean is false, the
    // acceptance is always satisfiable.  Otherwise, MARK is an
    // example of unsatisfiable mark.
34
    auto um = aut->acc().unsat_mark();
35
    if (!um.first)
36
      {
37
38
39
40
41
        // 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;
42
      }
43
    else
44
      {
45
46
47
48
49
        // Loop over the states and search a state that has only
        // self-loops 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.
50
51
52
53
        for (unsigned i = 0; i < n; ++i)
          {
            bool sinkable = true;
            bool first = true;
54
            acc_cond::mark_t loopmark = um.second;
55
56
            for (auto& t: aut->out(i))
              {
57
58
59
                // A state with an outgoing transition that isn't a
                // self-loop is not a candidate for a sink state.
                if (t.dst != i)
60
61
62
63
                  {
                    sinkable = false;
                    break;
                  }
64
65
66
                // If this is the first self-loop we see, record its
                // mark.  We will check that the mark is non accepting
                // only if this is the only self-loop.
67
68
                if (first)
                  {
69
                    loopmark = t.acc;
70
71
                    first = false;
                  }
72
73
74
75
76
77
                // If this this not the first self loop and it as a
                // different acceptance mark, do not consider this
                // state as a sink candidate: combining loops with
                // different marks might be used to build an accepting
                // cycle.
                else if (t.acc != loopmark)
78
79
80
81
82
                  {
                    sinkable = false;
                    break;
                  }
              }
83
84
85
86
87
88
89
            // Now if sinkable==true, it means that there is either no
            // outgoing transition, or just a self-loop.  In the later
            // case we have to check that the acceptance mark of that
            // self-loop is non-accepting.  In the former case
            // "loopmark" was already set to an unsatisfiable mark, so
            // it's ok to retest it.
            if (sinkable && !aut->acc().accepting(loopmark))
90
91
              {
                // We have found a sink!
92
                um.second = loopmark;
93
94
95
96
                sink = i;
                break;
              }
          }
97
98
      }

99
    unsigned t = aut->num_edges();
100

101
102
103
    // If the automaton is empty, and the initial state is not
    // universal, pretend this is the sink.
    if (t == 0 && !aut->is_univ_dest(aut->get_init_state_number()))
104
      sink = aut->get_init_state_number();
105

106
    // Now complete all states (excluding any newly added sink).
107
    for (unsigned i = 0; i < n; ++i)
108
      {
109
110
        bdd missingcond = bddtrue;
        acc_cond::mark_t acc = 0U;
111
        unsigned edge_to_sink = 0;
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
        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;
129
130
            if (t.dst == sink)
              edge_to_sink = aut->edge_number(t);
131
132
133
134
135
136
137
138
139
140
141
          }
        // 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);
              }
142
143
144
145
146
147
148
149
150
151
152
153
154
155
            // If we already have a brother-edge to the sink,
            // add the missing condition to that edge.
            if (edge_to_sink)
              {
                aut->edge_data(edge_to_sink).cond |= missingcond;
              }
            else                // otherwise, create the new edge.
              {
                // 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().is_true())
                  acc = 0U;
                aut->new_edge(i, sink, missingcond, acc);
              }
156
          }
157
      }
158

159
    aut->prop_complete(true);
160
    // Get rid of any named property if the automaton changed.
161
    if (t < aut->num_edges())
162
163
      aut->release_named_properties();
    else
164
      assert(t == aut->num_edges());
165
  }
166

167
  twa_graph_ptr complete(const const_twa_ptr& aut)
168
  {
169
    auto res = make_twa_graph(aut, twa::prop_set::all());
170
    complete_here(res);
171
    return res;
172
173
  }

174
}