taproduct.hh 4.25 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
31
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
78
79
// 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.
  ///
  /// This state is in fact a pair of state: the state from the ta
  /// 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
100
101
102
103
104
105
106
107
108
109

    virtual
    ~ta_succ_iterator_product();

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

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

    bool
    is_stuttering_transition() const;

  private:
    //@{
    /// Internal routines to advance to the next successor.
    void
    step_();
    void
    next_non_stuttering_();
110
111
112
113

    void
    next_kripke_dest();

114
115
116
117
118
119
120
121
122
123
124
    //@}

  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_;
    bool is_stuttering_transition_;
125
126
    bdd kripke_source_condition;
    state * kripke_current_dest_state;
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

  };

  /// \brief A lazy product.  (States are computed on the fly.)
  class ta_product : public ta
  {
  public:
    ta_product(const ta* testing_automata, const kripke* kripke_structure);

    virtual
    ~ta_product();

    virtual const states_set_t
    get_initial_states_set() const;

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

    virtual ta_succ_iterator_product*
146
147
    succ_iter(const spot::state* s, bdd condition) const
    {
148

149
150
      if (condition == bddtrue)
        return succ_iter(s);
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
      //TODO
      return 0;
    }

    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;

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

  private:
    bdd_dict* dict_;
    const ta* ta_;
    const kripke* kripke_;

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

}

#endif // SPOT_TA_TAPRODUCT_HH