isdet.cc 5.49 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#include <spot/twaalgos/isdet.hh>
21
#include <spot/twaalgos/sccinfo.hh>
22
23
24
25
26

namespace spot
{
  namespace
  {
27
    template<bool count>
28
29
    static
    unsigned
30
    count_nondet_states_aux(const const_twa_graph_ptr& aut)
31
    {
32
33
34
      unsigned nondet_states = 0;
      unsigned ns = aut->num_states();
      for (unsigned src = 0; src < ns; ++src)
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
        {
          bdd available = bddtrue;
          for (auto& t: aut->out(src))
            if (!bdd_implies(t.cond, available))
              {
                ++nondet_states;
                break;
              }
            else
              {
                available -= t.cond;
              }
          // If we are not counting non-deterministic states, abort as
          // soon as possible.
          if (!count && nondet_states)
            break;
        }
52
53
      std::const_pointer_cast<twa_graph>(aut)
        ->prop_deterministic(!nondet_states);
54
      return nondet_states;
55
56
57
58
    }
  }

  unsigned
59
  count_nondet_states(const const_twa_graph_ptr& aut)
60
  {
61
62
    if (aut->prop_deterministic())
      return 0;
63
    return count_nondet_states_aux<true>(aut);
64
65
66
  }

  bool
67
  is_deterministic(const const_twa_graph_ptr& aut)
68
  {
69
70
71
    trival d = aut->prop_deterministic();
    if (d.is_known())
      return d.is_true();
72
    return !count_nondet_states_aux<false>(aut);
73
  }
74

75
76
77
78
79
80
  void
  highlight_nondet_states(twa_graph_ptr& aut, unsigned color)
  {
    if (aut->prop_deterministic())
      return;
    unsigned ns = aut->num_states();
81
82
83
    auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-states");
    bool deterministic = true;
84
85
86
87
88
    for (unsigned src = 0; src < ns; ++src)
      {
        bdd available = bddtrue;
        for (auto& t: aut->out(src))
          if (!bdd_implies(t.cond, available))
89
90
91
92
            {
              (*highlight)[src] = color;
              deterministic = false;
            }
93
          else
94
95
96
            {
              available -= t.cond;
            }
97
      }
98
    aut->prop_deterministic(deterministic);
99
100
101
102
103
104
105
106
  }

  void
  highlight_nondet_edges(twa_graph_ptr& aut, unsigned color)
  {
    if (aut->prop_deterministic())
      return;
    unsigned ns = aut->num_states();
107
108
109
    auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-edges");
    bool deterministic = true;
110
111
112
113
114
115
116
    for (unsigned src = 0; src < ns; ++src)
      {
        // Make a first pass to gather non-deterministic labels
        bdd available = bddtrue;
        bdd extra = bddfalse;
        for (auto& t: aut->out(src))
          if (!bdd_implies(t.cond, available))
117
118
119
120
            {
              extra |= (t.cond - available);
              deterministic = false;
            }
121
          else
122
123
124
            {
              available -= t.cond;
            }
125
        // Second pass to gather the relevant edges.
126
        if (!deterministic)
127
128
          for (auto& t: aut->out(src))
            if ((t.cond & extra) != bddfalse)
129
              (*highlight)[aut->get_graph().index_of_edge(t)] = color;
130
      }
131
    aut->prop_deterministic(deterministic);
132
133
  }

134
  bool
135
  is_complete(const const_twa_graph_ptr& aut)
136
  {
137
138
    unsigned ns = aut->num_states();
    for (unsigned src = 0; src < ns; ++src)
139
      {
140
141
142
143
144
        bdd available = bddtrue;
        for (auto& t: aut->out(src))
          available -= t.cond;
        if (available != bddfalse)
          return false;
145
      }
146
147
148
    // The empty automaton is not complete since it does not have an
    // initial state.
    return ns > 0;
149
  }
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193

  bool
  is_semi_deterministic(const const_twa_graph_ptr& aut)
  {
    trival sd = aut->prop_semi_deterministic();
    if (sd.is_known())
      return sd.is_true();
    scc_info si(aut);
    si.determine_unknown_acceptance();
    unsigned nscc = si.scc_count();
    assert(nscc);
    std::vector<bool> reachable_from_acc(nscc);
    bool semi_det = true;
    do // iterator of SCCs in reverse topological order
      {
        --nscc;
        if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc])
          {
            for (unsigned succ: si.succ(nscc))
              reachable_from_acc[succ] = true;
            for (unsigned src: si.states_of(nscc))
              {
                bdd available = bddtrue;
                for (auto& t: aut->out(src))
                  if (!bdd_implies(t.cond, available))
                    {
                      semi_det = false;
                      std::cerr << "Failed on state " << src << '\n';
                      goto done;
                    }
                  else
                    {
                      available -= t.cond;
                    }
              }
          }
      }
    while (nscc);
  done:
    std::const_pointer_cast<twa_graph>(aut)
      ->prop_semi_deterministic(semi_det);
    return semi_det;
  }

194
}