kripkeexplicit.hh 5.14 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
3
// 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
29
30


#ifndef SPOT_KRIPKE_KRIPKEEXPLICIT_HH
# define SPOT_KRIPKE_KRIPKEEXPLICIT_HH

# include <iosfwd>
# include "kripke.hh"
# include "ltlast/formula.hh"
# include "kripkeprint.hh"

namespace spot
{
31
  /// \brief Concrete class for kripke states.
32
  class SPOT_API state_kripke : public state
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
80
81
82
83
84
85
86
87
    friend class kripke_explicit;
    friend class kripke_explicit_succ_iterator;
  private:
    state_kripke();

    /// \brief Compare two states.
    ///
    /// This method returns an integer less than, equal to, or greater
    /// than zero if \a this is found, respectively, to be less than, equal
    /// to, or greater than \a other according to some implicit total order.
    ///
    /// For moment, this method only compare the adress on the heap of the
    /// twice pointers.
    virtual int compare (const state* other) const;

    /// \brief Hash a state
    virtual size_t hash() const;

    /// \brief Duplicate a state.
    virtual state_kripke* clone() const;

    /// \brief Add a condition to the conditions already in the state.
    /// \param f The condition to add.
    void add_conditions(bdd f);

    /// \brief Add a new successor in the list.
    /// \param succ The successor state to add.
    void add_succ(state_kripke* succ);

    virtual bdd
    as_bdd() const
    {
      return bdd_;
    }

    /// \brief Release a state.
    ///
    virtual void
    destroy() const
    {
    }

    virtual
    ~state_kripke ()
    {
    }

    ////////////////////////////////
    // Management for succ_iterator

    const std::list<state_kripke*>& get_succ() const;

    bdd bdd_;
    std::list<state_kripke*> succ_;
88
89
90
91
92
  };


  /// \class kripke_explicit_succ_iterator
  /// \brief Implement iterator pattern on successor of a state_kripke.
93
  class SPOT_API kripke_explicit_succ_iterator : public kripke_succ_iterator
94
  {
95
96
  public:
    kripke_explicit_succ_iterator(const state_kripke*, bdd);
97

98
    ~kripke_explicit_succ_iterator();
99

100
101
    virtual bool first();
    virtual bool next();
102
    virtual bool done() const;
103

104
    virtual state_kripke* current_state() const;
105
106

    private:
107
108
    const state_kripke* s_;
    std::list<state_kripke*>::const_iterator it_;
109
110
111
112
113
  };


  /// \class kripke_explicit
  /// \brief Kripke Structure.
114
  class SPOT_API kripke_explicit : public kripke
115
  {
116
  public:
117
    kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr);
118
119
    ~kripke_explicit();

120
    bdd_dict_ptr get_dict() const;
121
122
123
124
125
    state_kripke* get_init_state() const;

    /// \brief Allow to get an iterator on the state we passed in
    /// parameter.
    kripke_explicit_succ_iterator*
126
    succ_iter(const spot::state* state) const;
127
128
129
130

    /// \brief Get the condition on the state
    bdd state_condition(const state* s) const;
    /// \brief Get the condition on the state
131
    bdd state_condition(const std::string&) const;
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
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

    /// \brief Return the name of the state.
    std::string format_state(const state*) const;


    /// \brief Create state, if it does not already exists.
    ///
    /// Used by the parser.
    void add_state(std::string);

    /// \brief Add a transition between two states.
    void add_transition(std::string source,
			std::string dest);

    /// \brief Add a BDD condition to the state
    ///
    /// \param add the condition.
    /// \param on_me where add the condition.
    void add_conditions(bdd add,
			std::string on_me);

    /// \brief Add a formula to the state corresponding to the name.
    ///
    /// \param f the formula to add.
    /// \param on_me the state where to add.
    void add_condition(const ltl::formula* f,
		       std::string on_me);

    /// \brief Return map between states and their names.
    const std::map<const state_kripke*, std::string>&
    sn_get() const;

  private:
    /// \brief Add a state in the two maps.
    void add_state(std::string, state_kripke*);

    void add_conditions(bdd add,
			state_kripke* on_me);

    void add_transition(std::string source,
			const state_kripke* dest);

    void add_transition(state_kripke* source,
			const state_kripke* dest);

177
    bdd_dict_ptr dict_;
178
179
180
    state_kripke* init_;
    std::map<const std::string, state_kripke*> ns_nodes_;
    std::map<const state_kripke*, std::string> sn_nodes_;
181
  };
182
183
184
185
186
187
188

  inline kripke_explicit_ptr
  make_kripke_explicit(const bdd_dict_ptr& d,
		       state_kripke* init = nullptr)
  {
    return std::make_shared<kripke_explicit>(d, init);
  }
189
}
190
#endif // SPOT_KRIPKE_KRIPKEEXPLICIT_HH