taexplicit.hh 6.79 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 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
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
13
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
15
// License for more details.
16
17
//
// 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
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

#ifndef SPOT_TA_TAEXPLICIT_HH
# define SPOT_TA_TAEXPLICIT_HH

#include "misc/hash.hh"
#include <list>
#include "tgba/tgba.hh"
#include <set>
#include "ltlast/formula.hh"
#include <cassert>
#include "misc/bddlt.hh"
#include "ta.hh"

namespace spot
{
  // Forward declarations.  See below.
  class state_ta_explicit;
  class ta_explicit_succ_iterator;
  class ta_explicit;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
39
40
  /// Explicit representation of a spot::ta.
  /// \ingroup ta_representation
41
  class SPOT_API ta_explicit : public ta
42
43
  {
  public:
44
    ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
45
46
		state_ta_explicit* artificial_initial_state = 0,
		bool own_tgba = false);
47
48
49
50
51
52
53

    const tgba*
    get_tgba() const;

    state_ta_explicit*
    add_state(state_ta_explicit* s);

54
    void
55
    add_to_initial_states_set(state* s, bdd condition = bddfalse);
56

57
58
    void
    create_transition(state_ta_explicit* source, bdd condition,
59
60
        bdd acceptance_conditions, state_ta_explicit* dest,
        bool add_at_beginning = false);
61

62
63
64
65
66
    void
    delete_stuttering_transitions();
    // ta interface
    virtual
    ~ta_explicit();
67
    virtual const states_set_t
68
69
70
71
72
    get_initial_states_set() const;

    virtual ta_succ_iterator*
    succ_iter(const spot::state* s) const;

73
74
75
    virtual ta_succ_iterator*
    succ_iter(const spot::state* s, bdd condition) const;

76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
    virtual bdd_dict*
    get_dict() const;

    virtual std::string
    format_state(const spot::state* s) const;

    virtual bool
    is_accepting_state(const spot::state* s) const;

    virtual bool
    is_livelock_accepting_state(const spot::state* s) const;

    virtual bool
    is_initial_state(const spot::state* s) const;

    virtual bdd
    get_state_condition(const spot::state* s) const;

94
95
96
    virtual void
    free_state(const spot::state* s) const;

97
98
99
100
101
102
103
104
105
106
107
108
109
    spot::state*
    get_artificial_initial_state() const
    {
      return (spot::state*) artificial_initial_state_;
    }

    void
    set_artificial_initial_state(state_ta_explicit* s)
    {
      artificial_initial_state_ = s;

    }

110
111
112
    virtual void
    delete_stuttering_and_hole_successors(spot::state* s);

113
114
115
116
117
118
    ta::states_set_t
    get_states_set()
    {
      return states_set_;
    }

119
120
121
122
123
124
125
126
127
128
129
    /// \brief Return the set of all acceptance conditions used
    /// by this automaton.
    ///
    /// The goal of the emptiness check is to ensure that
    /// a strongly connected component walks through each
    /// of these acceptiong conditions.  I.e., the union
    /// of the acceptiong conditions of all transition in
    /// the SCC should be equal to the result of this function.
    bdd
    all_acceptance_conditions() const
    {
130
      return all_acceptance_conditions_;
131
132
    }

133
134
  private:
    // Disallow copy.
135
136
    ta_explicit(const ta_explicit& other) = delete;
    ta_explicit& operator=(const ta_explicit& other) = delete;
137
138

    const tgba* tgba_;
139
    bdd all_acceptance_conditions_;
140
    state_ta_explicit* artificial_initial_state_;
141
142
    ta::states_set_t states_set_;
    ta::states_set_t initial_states_set_;
143
    bool own_tgba_;
144
145
146
  };

  /// states used by spot::ta_explicit.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
147
  /// \ingroup ta_representation
148
  class SPOT_API state_ta_explicit : public spot::state
149
  {
150
#ifndef SWIG
151
152
  public:

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
153
    /// Explicit transitions.
154
155
156
    struct transition
    {
      bdd condition;
157
      bdd acceptance_conditions;
158
159
160
161
162
163
164
      state_ta_explicit* dest;
    };

    typedef std::list<transition*> transitions;

    state_ta_explicit(const state* tgba_state, const bdd tgba_condition,
        bool is_initial_state = false, bool is_accepting_state = false,
165
        bool is_livelock_accepting_state = false, transitions* trans = 0) :
166
167
168
169
170
171
172
173
174
175
176
177
178
179
      tgba_state_(tgba_state), tgba_condition_(tgba_condition),
          is_initial_state_(is_initial_state), is_accepting_state_(
              is_accepting_state), is_livelock_accepting_state_(
              is_livelock_accepting_state), transitions_(trans)
    {
    }

    virtual int
    compare(const spot::state* other) const;
    virtual size_t
    hash() const;
    virtual state_ta_explicit*
    clone() const;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
180
181
    virtual void
    destroy() const
182
183
184
    {
    }

185
186
187
188
189
190
191
192
    virtual
    ~state_ta_explicit()
    {
    }

    transitions*
    get_transitions() const;

193
194
195
196
    // return transitions filtred by condition
    transitions*
    get_transitions(bdd condition) const;

197
    void
198
    add_transition(transition* t, bool add_at_beginning = false);
199
200
201
202
203
204
205
206
207
208
209
210
211

    const state*
    get_tgba_state() const;
    const bdd
    get_tgba_condition() const;
    bool
    is_accepting_state() const;
    void
    set_accepting_state(bool is_accepting_state);
    bool
    is_livelock_accepting_state() const;
    void
    set_livelock_accepting_state(bool is_livelock_accepting_state);
212

213
214
215
216
    bool
    is_initial_state() const;
    void
    set_initial_state(bool is_initial_state);
217

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
218
    /// \brief Return true if the state has no successors
219
220
221
    bool
    is_hole_state() const;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
222
223
    /// \brief Remove stuttering transitions
    /// and transitions leading to states having no successors
224
225
226
227
228
    void
    delete_stuttering_and_hole_successors();

    void
    free_transitions();
229

230
    state_ta_explicit* stuttering_reachable_livelock;
231
232
233
234
235
236
237
  private:
    const state* tgba_state_;
    const bdd tgba_condition_;
    bool is_initial_state_;
    bool is_accepting_state_;
    bool is_livelock_accepting_state_;
    transitions* transitions_;
238
239
    std::unordered_map<int, transitions*, std::hash<int>>
      transitions_by_condition;
240
#endif // !SWIG
241
242
243
  };

  /// Successor iterators used by spot::ta_explicit.
244
  class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator
245
246
247
248
  {
  public:
    ta_explicit_succ_iterator(const state_ta_explicit* s);

249
250
    ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);

251
252
253
254
255
256
257
258
259
260
261
262
    virtual void
    first();
    virtual void
    next();
    virtual bool
    done() const;

    virtual state*
    current_state() const;
    virtual bdd
    current_condition() const;

263
264
265
    virtual bdd
    current_acceptance_conditions() const;

266
267
268
269
270
271
272
273
  private:
    state_ta_explicit::transitions* transitions_;
    state_ta_explicit::transitions::const_iterator i_;
  };

}

#endif // SPOT_TA_TAEXPLICIT_HH