ta.hh 8.27 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// Copyright (C) 2010, 2012-2017 Laboratoire de Recherche et
3
// Developpement 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
#pragma once
21
22
23
24

#include <set>

#include <cassert>
25
26
#include <spot/misc/bddlt.hh>
#include <spot/twa/twa.hh>
27
28
29

namespace spot
{
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
30

31
32
33
  // Forward declarations.  See below.
  class ta_succ_iterator;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
34
35
36
37
38
  /// \defgroup ta TA (Testing Automata)
  ///
  /// This type and its cousins are listed \ref ta_essentials "here".
  /// This is an abstract interface.  Its implementations are \ref
  /// ta_representation "concrete representations".  The
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
  /// algorithms that work on spot::ta are \ref ta_algorithms
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
40
41
42
43
44
45
  /// "listed separately".

  /// \addtogroup ta_essentials Essential TA types
  /// \ingroup ta

  /// \ingroup ta_essentials
46
  /// \brief A Testing Automaton.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
47
48
49
  ///
  /// The Testing Automata (TA) were introduced by
  /// Henri Hansen, Wojciech Penczek and Antti Valmari
50
  /// in "Stuttering-insensitive automata for on-the-fly detection of livelock
51
  /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
  /// Theoretical Computer Science.Elsevier.
  ///
  /// While a TGBA automaton observes the value of the atomic propositions, the
  /// basic idea of TA is to detect the changes in these values; if a valuation
  ///  does not change between two consecutive valuations of an execution,
  /// the TA stay in the same state. A TA transition \c (s,k,d) is labeled by a
  /// "changeset" \c k: i.e. the set of atomic propositions that change between
  /// states \c s and \c d, if the changeset is empty then the transition is
  /// called stuttering transition.
  /// To detect execution that ends by stuttering in the same TA state, a
  /// new kind of acceptance states is introduced: "livelock-acceptance states"
  /// (in addition to the standard Buchi-acceptance states).
  ///
  /// Browsing such automaton can be achieved using two functions:
  /// \c get_initial_states_set or \c get_artificial_initial_state, and \c
  /// succ_iter. The former returns the initial state(s) while the latter lists
68
  /// the successor states of any state (filtred by "changeset").
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
69
70
71
72
73
74
  ///
  /// Note that although this is a transition-based automata,
  /// we never represent transitions!  Transition informations are
  /// obtained by querying the iterator over the successors of
  /// a state.

75
  class SPOT_API ta
76
  {
77
78
  protected:
    acc_cond acc_;
79
    bdd_dict_ptr dict_;
80
81

  public:
82
    ta(const bdd_dict_ptr& d)
83
      : dict_(d)
84
85
86
    {
    }

87
88
89
90
91
92
    virtual
    ~ta()
    {
    }

    typedef std::set<state*, state_ptr_less_than> states_set_t;
93
    typedef std::set<const state*, state_ptr_less_than> const_states_set_t;
94

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
95
    /// \brief Get the initial states set of the automaton.
96
    virtual const_states_set_t
97
    get_initial_states_set() const = 0;
98

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
99
100
101
    /// \brief Get the artificial initial state set of the automaton.
    /// Return 0 if this artificial state is not implemented
    /// (in this case, use \c get_initial_states_set)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
102
    /// The aim of adding this state is to have a unique initial state. This
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
103
104
105
    /// artificial initial state have one transition to each real initial state,
    /// and this transition is labeled by the corresponding initial condition.
    /// (For more details, see the paper cited above)
106
    virtual const spot::state*
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
107
108
    get_artificial_initial_state() const
    {
109
      return nullptr;
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
110
    }
111

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
112
113
114
115
116
117
    /// \brief Get an iterator over the successors of \a state.
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
118
    virtual ta_succ_iterator*
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
119
    succ_iter(const spot::state* state) const = 0;
120

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
121
    /// \brief Get an iterator over the successors of \a state
122
    /// filtred by the changeset on transitions
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
123
124
125
126
127
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
128
    virtual ta_succ_iterator*
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
129
    succ_iter(const spot::state* state, bdd changeset) const = 0;
130

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
131
132
133
134
135
136
137
    /// \brief Get the dictionary associated to the automaton.
    ///
    /// State are represented as BDDs.  The dictionary allows
    /// to map BDD variables back to formulae, and vice versa.
    /// This is useful when dealing with several automata (which
    /// may use the same BDD variable for different formula),
    /// or simply when printing.
138
139
140
    bdd_dict_ptr
    get_dict() const
    {
141
      return dict_;
142
    }
143

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
144
145
146
147
    /// \brief Format the state as a string for printing.
    ///
    /// This formating is the responsability of the automata
    /// that owns the state.
148
    virtual std::string
149
    format_state(const spot::state* s) const = 0;
150

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
151
    /// \brief Return true if \a s is a Buchi-accepting state, otherwise false
152
    virtual bool
153
    is_accepting_state(const spot::state* s) const = 0;
154

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
155
156
    /// \brief Return true if \a s is a livelock-accepting state
    /// , otherwise false
157
    virtual bool
158
    is_livelock_accepting_state(const spot::state* s) const = 0;
159

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
160
    /// \brief Return true if \a s is an initial state, otherwise false
161
    virtual bool
162
    is_initial_state(const spot::state* s) const = 0;
163

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
164
165
    /// \brief Return a BDD condition that represents the valuation
    /// of atomic propositions in the state \a s
166
    virtual bdd
167
168
    get_state_condition(const spot::state* s) const = 0;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
169
    /// \brief Release a state \a s
170
171
    virtual void
    free_state(const spot::state* s) const = 0;
172

173
174
175
176
177
178
179
180
181
182

    const acc_cond& acc() const
    {
      return acc_;
    }

    acc_cond& acc()
    {
      return acc_;
    }
183

184
185
  };

186
187
188
  typedef std::shared_ptr<ta> ta_ptr;
  typedef std::shared_ptr<const ta> const_ta_ptr;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
189
  /// \ingroup ta_essentials
190
  /// \brief Iterate over the successors of a state.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
191
192
193
194
195
196
  ///
  /// This class provides the basic functionalities required to
  /// iterate over the successors of a state, as well as querying
  /// transition labels.  Because transitions are never explicitely
  /// encoded, labels (conditions and acceptance conditions) can only
  /// be queried while iterating over the successors.
197
  class ta_succ_iterator : public twa_succ_iterator
198
199
200
201
202
203
204
205
  {
  public:
    virtual
    ~ta_succ_iterator()
    {
    }
  };

206
#ifndef SWIG
207
  // A stack of Strongly-Connected Components
208
  class scc_stack_ta
209
210
211
212
213
214
215
216
217
218
219
220
  {
  public:
    struct connected_component
    {
    public:
      connected_component(int index = -1);

      /// Index of the SCC.
      int index;

      bool is_accepting;

221
222
      /// The bdd condition is the union of all acceptance conditions of
      /// transitions which connect the states of the connected component.
223
      acc_cond::mark_t condition;
224

225
      std::list<const state*> rem;
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
    };

    /// Stack a new SCC with index \a index.
    void
    push(int index);

    /// Access the top SCC.
    connected_component&
    top();

    /// Access the top SCC.
    const connected_component&
    top() const;

    /// Pop the top SCC.
    void
    pop();

    /// How many SCC are in stack.
    size_t
    size() const;

    /// The \c rem member of the top SCC.
249
    std::list<const state*>&
250
251
252
253
254
255
256
257
258
    rem();

    /// Is the stack empty?
    bool
    empty() const;

    typedef std::list<connected_component> stack_type;
    stack_type s;
  };
259
#endif // !SWIG
260

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
/// \addtogroup ta_representation TA representations
/// \ingroup ta

/// \addtogroup ta_algorithms TA algorithms
/// \ingroup ta

/// \addtogroup ta_io Input/Output of TA
/// \ingroup ta_algorithms

/// \addtogroup tgba_ta Transforming TGBA into TA
/// \ingroup ta_algorithms


/// \addtogroup ta_generic Algorithm patterns
/// \ingroup ta_algorithms

/// \addtogroup ta_reduction TA simplifications
/// \ingroup ta_algorithms

/// \addtogroup ta_misc Miscellaneous algorithms on TA
/// \ingroup ta_algorithms
282
}