taproduct.hh 5.33 KB
Newer Older
1
2
3
4
5
6
7
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
// de l Epita (LRDE).
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
// (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
17
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
19
20
21
22
23
24
25
26
27
28

#ifndef SPOT_TA_TAPRODUCT_HH
# define SPOT_TA_TAPRODUCT_HH

#include "ta.hh"
#include "kripke/kripke.hh"

namespace spot
{

  /// \brief A state for spot::ta_product.
29
  /// \ingroup ta_emptiness_check
30
  ///
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
31
  /// This state is in fact a pair of state: the state from the TA
32
33
34
35
36
37
38
39
40
41
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
  /// automaton and that of Kripke structure.
  class state_ta_product : public state
  {
  public:
    /// \brief Constructor
    /// \param ta_state The state from the ta automaton.
    /// \param kripke_state_ The state from Kripke structure.
    state_ta_product(state* ta_state, state* kripke_state) :
      ta_state_(ta_state), kripke_state_(kripke_state)
    {
    }

    /// Copy constructor
    state_ta_product(const state_ta_product& o);

    virtual
    ~state_ta_product();

    state*
    get_ta_state() const
    {
      return ta_state_;
    }

    state*
    get_kripke_state() const
    {
      return kripke_state_;
    }

    virtual int
    compare(const state* other) const;
    virtual size_t
    hash() const;
    virtual state_ta_product*
    clone() const;

  private:
    state* ta_state_; ///< State from the ta automaton.
    state* kripke_state_; ///< State from the kripke structure.
  };

  /// \brief Iterate over the successors of a product computed on the fly.
  class ta_succ_iterator_product : public ta_succ_iterator
  {
  public:
78
79
    ta_succ_iterator_product(const state_ta_product* s, const ta* t,
        const kripke* k);
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

    virtual
    ~ta_succ_iterator_product();

    // iteration
    void
    first();
    void
    next();
    bool
    done() const;

    // inspection
    state_ta_product*
    current_state() const;
    bdd
    current_condition() const;

98
99
100
    bdd
    current_acceptance_conditions() const;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
101
    /// \brief Return true if the changeset of the current transition is empty
102
103
104
    bool
    is_stuttering_transition() const;

105
  protected:
106
107
108
109
110
111
    //@{
    /// Internal routines to advance to the next successor.
    void
    step_();
    void
    next_non_stuttering_();
112

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
113
    /// \brief Move to the next successor in the kripke structure
114
115
116
    void
    next_kripke_dest();

117
118
119
120
121
122
123
124
125
126
    //@}

  protected:
    const state_ta_product* source_;
    const ta* ta_;
    const kripke* kripke_;
    ta_succ_iterator* ta_succ_it_;
    tgba_succ_iterator* kripke_succ_it_;
    state_ta_product* current_state_;
    bdd current_condition_;
127
    bdd current_acceptance_conditions_;
128
    bool is_stuttering_transition_;
129
130
    bdd kripke_source_condition;
    state * kripke_current_dest_state;
131
132
133

  };

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
134
135
  /// \brief A lazy product between a Testing automaton and a Kripke structure.
  /// (States are computed on the fly.)
136
  /// \ingroup ta_emptiness_check
137
138
139
  class ta_product : public ta
  {
  public:
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
140
141
142
143
    /// \brief Constructor.
    /// \param testing_automaton The TA component in the product.
    /// \param kripke_structure The Kripke component in the product.
    ta_product(const ta* testing_automaton, const kripke* kripke_structure);
144
145
146
147

    virtual
    ~ta_product();

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
148
    virtual const std::set<state*, state_ptr_less_than>
149
150
151
152
153
    get_initial_states_set() const;

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

154
155
156
    virtual ta_succ_iterator_product*
    succ_iter(const spot::state* s, bdd changeset) const;

157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
    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;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
172
    /// \brief Return true if the state \a s has no succeseurs
173
    /// in the TA automaton (the TA component of the product automaton)
174
175
176
    virtual bool
    is_hole_state_in_ta_component(const spot::state* s) const;

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

180
181
182
    virtual bdd
    all_acceptance_conditions() const;

183
184
185
    virtual void
    free_state(const spot::state* s) const;

186
187
188
189
190
191
192
193
194
195
196
197
    const ta*
    get_ta() const
    {
      return ta_;
    }

    const kripke*
    get_kripke() const
    {
      return kripke_;
    }

198
199
200
201
202
203
204
205
206
207
208
  private:
    bdd_dict* dict_;
    const ta* ta_;
    const kripke* kripke_;

    // Disallow copy.
    ta_product(const ta_product&);
    ta_product&
    operator=(const ta_product&);
  };

209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225

   class ta_succ_iterator_product_by_changeset : public ta_succ_iterator_product
  {
  public:
    ta_succ_iterator_product_by_changeset(const state_ta_product* s,
        const ta* t, const kripke* k, bdd changeset);



    /// \brief Move to the next successor in the kripke structure
    void
    next_kripke_dest();


   };


226
227
228
}

#endif // SPOT_TA_TAPRODUCT_HH