taproduct.hh 5.42 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
// 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
// the Free Software Foundation; either version 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#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.
31
  /// \ingroup ta_emptiness_check
32
  ///
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
33
  /// This state is in fact a pair of state: the state from the TA
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
78
79
  /// 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:
80
81
    ta_succ_iterator_product(const state_ta_product* s, const ta* t,
        const kripke* k);
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

    virtual
    ~ta_succ_iterator_product();

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

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

100
101
102
    bdd
    current_acceptance_conditions() const;

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

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

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

119
120
121
122
123
124
125
126
127
128
    //@}

  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_;
129
    bdd current_acceptance_conditions_;
130
    bool is_stuttering_transition_;
131
132
    bdd kripke_source_condition;
    state * kripke_current_dest_state;
133
134
135

  };

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
136
137
  /// \brief A lazy product between a Testing automaton and a Kripke structure.
  /// (States are computed on the fly.)
138
  /// \ingroup ta_emptiness_check
139
140
141
  class ta_product : public ta
  {
  public:
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
142
143
144
145
    /// \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);
146
147
148
149

    virtual
    ~ta_product();

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

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

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

159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
    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
174
    /// \brief Return true if the state \a s has no succeseurs
175
    /// in the TA automaton (the TA component of the product automaton)
176
177
178
    virtual bool
    is_hole_state_in_ta_component(const spot::state* s) const;

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

182
183
184
    virtual bdd
    all_acceptance_conditions() const;

185
186
187
    virtual void
    free_state(const spot::state* s) const;

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

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

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

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

211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227

   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();


   };


228
229
230
}

#endif // SPOT_TA_TAPRODUCT_HH