tgbaexplicit.hh 9.43 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2006, 2009 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
//
// 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.

22
23
24
#ifndef SPOT_TGBA_TGBAEXPLICIT_HH
# define SPOT_TGBA_TGBAEXPLICIT_HH

25
#include "misc/hash.hh"
26
27
28
#include <list>
#include "tgba.hh"
#include "ltlast/formula.hh"
29
#include <cassert>
30
31
32
33
34
35

namespace spot
{
  // Forward declarations.  See below.
  class state_explicit;
  class tgba_explicit_succ_iterator;
36
  class tgba_explicit;
37
38

  /// Explicit representation of a spot::tgba.
39
  /// \ingroup tgba_representation
40
  class tgba_explicit: public tgba
41
42
  {
  public:
43
    tgba_explicit(bdd_dict* dict);
44
45
46

    struct transition;
    typedef std::list<transition*> state;
47
48

    /// Explicit transitions (used by spot::tgba_explicit).
49
50
51
    struct transition
    {
      bdd condition;
52
      bdd acceptance_conditions;
53
      const state* dest;
54
55
    };

56
57
    /// Add a default initial state.
    virtual state* add_default_init() = 0;
58

59
60
    transition*
    create_transition(state* source, const state* dest);
61

62
    void add_condition(transition* t, const ltl::formula* f);
63
64
    /// This assumes that all variables in \a f are known from dict.
    void add_conditions(transition* t, bdd f);
65
66
67
68
69
70
71

    /// \brief Copy the acceptance conditions of a tgba.
    ///
    /// If used, this function should be called before creating any
    /// transition.
    void copy_acceptance_conditions_of(const tgba *a);

72
73
74
    /// The the acceptance conditions.
    void set_acceptance_conditions(bdd acc);

75
76
77
78
    bool has_acceptance_condition(const ltl::formula* f) const;
    void add_acceptance_condition(transition* t, const ltl::formula* f);
    /// This assumes that all acceptance conditions in \a f are known from dict.
    void add_acceptance_conditions(transition* t, bdd f);
79

80
81
82
83
    // tgba interface
    virtual ~tgba_explicit();
    virtual spot::state* get_init_state() const;
    virtual tgba_succ_iterator*
84
85
86
    succ_iter(const spot::state* local_state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const;
87
    virtual bdd_dict* get_dict() const;
88

89
90
    virtual bdd all_acceptance_conditions() const;
    virtual bdd neg_acceptance_conditions() const;
91

92
93
    virtual std::string format_state(const spot::state* s) const = 0;

94
  protected:
95
96
97
    virtual bdd compute_support_conditions(const spot::state* state) const;
    virtual bdd compute_support_variables(const spot::state* state) const;

98
    bdd get_acceptance_condition(const ltl::formula* f);
99

100
    bdd_dict* dict_;
101
    tgba_explicit::state* init_;
102
103
104
    mutable bdd all_acceptance_conditions_;
    bdd neg_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
105
106
107
108

  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit& other);
109
    tgba_explicit& operator=(const tgba_explicit& other);
110
111
112
  };


113

114
  /// States used by spot::tgba_explicit.
115
  /// \ingroup tgba_representation
116
117
118
119
120
121
122
123
124
  class state_explicit : public spot::state
  {
  public:
    state_explicit(const tgba_explicit::state* s)
      : state_(s)
    {
    }

    virtual int compare(const spot::state* other) const;
125
    virtual size_t hash() const;
126
127
    virtual state_explicit* clone() const;

128
129
130
131
132
133
134
135
136
137
    virtual ~state_explicit()
    {
    }

    const tgba_explicit::state* get_state() const;
  private:
    const tgba_explicit::state* state_;
  };


138
  /// Successor iterators used by spot::tgba_explicit.
139
  /// \ingroup tgba_representation
140
  class tgba_explicit_succ_iterator: public tgba_succ_iterator
141
142
  {
  public:
143
    tgba_explicit_succ_iterator(const tgba_explicit::state* s, bdd all_acc);
144
145
146

    virtual void first();
    virtual void next();
147
    virtual bool done() const;
148

149
150
    virtual state_explicit* current_state() const;
    virtual bdd current_condition() const;
151
    virtual bdd current_acceptance_conditions() const;
152
153
154
155

  private:
    const tgba_explicit::state* s_;
    tgba_explicit::state::const_iterator i_;
156
    bdd all_acceptance_conditions_;
157
158
  };

159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
  /// A tgba_explicit instance with states labeled by a given type.
  template<typename label, typename label_hash>
  class tgba_explicit_labelled: public tgba_explicit
  {
  protected:
    typedef label label_t;
    typedef Sgi::hash_map<label, tgba_explicit::state*,
			  label_hash> ns_map;
    typedef Sgi::hash_map<const tgba_explicit::state*, label,
			  ptr_hash<tgba_explicit::state> > sn_map;
    ns_map name_state_map_;
    sn_map state_name_map_;
  public:
    tgba_explicit_labelled(bdd_dict* dict) : tgba_explicit(dict) {};

    bool has_state(const label& name)
    {
      return name_state_map_.find(name) != name_state_map_.end();
    }

179
180
181
182
183
184
185
186
187
188
189
190
191
192
    const label& get_label(const tgba_explicit::state* s) const
    {
      typename sn_map::const_iterator i = state_name_map_.find(s);
      assert(i != state_name_map_.end());
      return i->second;
    }

    const label& get_label(const spot::state* s) const
    {
      const state_explicit* se = dynamic_cast<const state_explicit*>(s);
      assert(se);
      return get_label(se->get_state());
    }

193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
    /// Return the tgba_explicit::state for \a name, creating the state if
    /// it does not exist.
    state* add_state(const label& name)
    {
      typename ns_map::iterator i = name_state_map_.find(name);
      if (i == name_state_map_.end())
	{
	  tgba_explicit::state* s = new tgba_explicit::state;
	  name_state_map_[name] = s;
	  state_name_map_[s] = name;

	  // The first state we add is the inititial state.
	  // It can also be overridden with set_init_state().
	  if (!init_)
	    init_ = s;

	  return s;
	}
      return i->second;
    }

    state*
    set_init_state(const label& state)
    {
      tgba_explicit::state* s = add_state(state);
      init_ = s;
      return s;
    }


    transition*
    create_transition(state* source, const state* dest)
    {
      return tgba_explicit::create_transition(source, dest);
    }

    transition*
    create_transition(const label& source, const label& dest)
    {
      // It's important that the source be created before the
      // destination, so the first source encountered becomes the
      // default initial state.
      state* s = add_state(source);
      return tgba_explicit::create_transition(s, add_state(dest));
    }

    void
    complement_all_acceptance_conditions()
    {
      bdd all = all_acceptance_conditions();
      typename ns_map::iterator i;
      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
	{
	  tgba_explicit::state::iterator i2;
	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	    {
	      (*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions;
	    }
	}
    }

    void
    declare_acceptance_condition(const ltl::formula* f)
    {
      int v = dict_->register_acceptance_variable(f, this);
      f->destroy();
      bdd neg = bdd_nithvar(v);
      neg_acceptance_conditions_ &= neg;

      // Append neg to all acceptance conditions.
      typename ns_map::iterator i;
      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
	{
	  tgba_explicit::state::iterator i2;
	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	    (*i2)->acceptance_conditions &= neg;
	}

      all_acceptance_conditions_computed_ = false;
    }


    void
    merge_transitions()
    {
      typename ns_map::iterator i;
      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
	{
	  state::iterator t1;
	  for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
	    {
	      bdd acc = (*t1)->acceptance_conditions;
	      const state* dest = (*t1)->dest;

	      // Find another transition with the same destination and
	      // acceptance conditions.
	      state::iterator t2 = t1;
	      ++t2;
	      while (t2 != i->second->end())
		{
		  state::iterator t2copy = t2++;
		  if ((*t2copy)->acceptance_conditions == acc
		      && (*t2copy)->dest == dest)
		    {
		      (*t1)->condition |= (*t2copy)->condition;
		      delete *t2copy;
		      i->second->erase(t2copy);
		    }
		}
	    }
	}
    }


    virtual
    ~tgba_explicit_labelled()
    {
    }

  };

  class tgba_explicit_string:
    public tgba_explicit_labelled<std::string, string_hash>
  {
  public:
    tgba_explicit_string(bdd_dict* dict):
      tgba_explicit_labelled<std::string, string_hash>(dict)
    {};
321
    virtual ~tgba_explicit_string();
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
    virtual state* add_default_init();
    virtual std::string format_state(const spot::state* s) const;
  };

  class tgba_explicit_formula:
    public tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>
  {
  public:
    tgba_explicit_formula(bdd_dict* dict):
      tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict)
    {};
    virtual ~tgba_explicit_formula();
    virtual state* add_default_init();
    virtual std::string format_state(const spot::state* s) const;
  };
337
338
339
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH