kripkeexplicit.hh 5.02 KB
Newer Older
1
2
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
3
4
5
6
7
8
// 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
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
33
  class state_kripke : public state
  {
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
93
94
  };


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

98
    ~kripke_explicit_succ_iterator();
99

100
101
102
    virtual void first();
    virtual void next();
    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
114
115
  };


  /// \class kripke_explicit
  /// \brief Kripke Structure.
  class kripke_explicit : public kripke
  {
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
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
177
178
179
180
181
182
183
  public:
    kripke_explicit(bdd_dict*);
    kripke_explicit(bdd_dict*, state_kripke*);
    ~kripke_explicit();

    bdd_dict* get_dict() const;
    state_kripke* get_init_state() const;

    /// \brief Allow to get an iterator on the state we passed in
    /// parameter.
    kripke_explicit_succ_iterator*
    succ_iter(const spot::state* local_state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const;

    /// \brief Get the condition on the state
    bdd state_condition(const state* s) const;
    /// \brief Get the condition on the state
    bdd state_condition(const std::string) const;

    /// \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);

    bdd_dict* dict_;
    state_kripke* init_;
    std::map<const std::string, state_kripke*> ns_nodes_;
    std::map<const state_kripke*, std::string> sn_nodes_;
184
185
186
  };
}
#endif /* !SPOT_KRIPKEEXPLICIT_HH_ */