taproduct.hh 5.42 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 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
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
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
{

29
  /// \ingroup ta_emptiness_check
30
  /// \brief A state for spot::ta_product.
31
  ///
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
32
  /// This state is in fact a pair of state: the state from the TA
33
  /// automaton and that of Kripke structure.
34
  class SPOT_API state_ta_product : public state
35
36
37
38
  {
  public:
    /// \brief Constructor
    /// \param ta_state The state from the ta automaton.
39
    /// \param kripke_state The state from Kripke structure.
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
    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.
76
  class SPOT_API ta_succ_iterator_product : public ta_succ_iterator
77
78
  {
  public:
79
80
    ta_succ_iterator_product(const state_ta_product* s, const ta* t,
        const kripke* k);
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

    virtual
    ~ta_succ_iterator_product();

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

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

99
100
101
    bdd
    current_acceptance_conditions() const;

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

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

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

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

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

  };

135
  /// \ingroup ta_emptiness_check
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
  class SPOT_API ta_product: public ta
139
140
  {
  public:
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
141
142
143
144
    /// \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);
145
146
147
148

    virtual
    ~ta_product();

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

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

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

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

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

181
182
183
    virtual bdd
    all_acceptance_conditions() const;

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

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

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

199
200
201
202
203
204
  private:
    bdd_dict* dict_;
    const ta* ta_;
    const kripke* kripke_;

    // Disallow copy.
205
206
    ta_product(const ta_product&) = delete;
    ta_product& operator=(const ta_product&) = delete;
207
208
  };

209

210
211
  class SPOT_API ta_succ_iterator_product_by_changeset :
    public ta_succ_iterator_product
212
213
214
  {
  public:
    ta_succ_iterator_product_by_changeset(const state_ta_product* s,
215
216
					  const ta* t, const kripke* k,
					  bdd changeset);
217

218
219
220
    /// \brief Move to the next successor in the Kripke structure
    void next_kripke_dest();
  };
221

222
223
224
}

#endif // SPOT_TA_TAPRODUCT_HH