tgbaexplicit.hh 10.2 KB
Newer Older
1
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
Guillaume Sadegh's avatar
Guillaume Sadegh committed
2
3
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
4
5
// 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
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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.

24
25
26
#ifndef SPOT_TGBA_TGBAEXPLICIT_HH
# define SPOT_TGBA_TGBAEXPLICIT_HH

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

namespace spot
{
  // Forward declarations.  See below.
  class state_explicit;
  class tgba_explicit_succ_iterator;
38
  class tgba_explicit;
39
40

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

    struct transition;
    typedef std::list<transition*> state;
49
50

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

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

61
62
    transition*
    create_transition(state* source, const state* dest);
63

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

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

74
75
76
    /// The the acceptance conditions.
    void set_acceptance_conditions(bdd acc);

77
78
79
80
    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);
81

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

91
92
    virtual bdd all_acceptance_conditions() const;
    virtual bdd neg_acceptance_conditions() const;
93

94
95
    virtual std::string format_state(const spot::state* s) const = 0;

96
  protected:
97
98
99
    virtual bdd compute_support_conditions(const spot::state* state) const;
    virtual bdd compute_support_variables(const spot::state* state) const;

100
    bdd get_acceptance_condition(const ltl::formula* f);
101

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

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


115

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

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

130
131
132
133
134
135
136
137
138
139
    virtual ~state_explicit()
    {
    }

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


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

    virtual void first();
    virtual void next();
149
    virtual bool done() const;
150

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

  private:
    const tgba_explicit::state* s_;
    tgba_explicit::state::const_iterator i_;
158
    bdd all_acceptance_conditions_;
159
160
  };

161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
  /// 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();
    }

181
182
183
184
185
186
187
188
189
190
191
192
193
194
    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());
    }

195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
    /// 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;
    }
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
321
322
    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)
    {};
323
    virtual ~tgba_explicit_string();
324
325
    virtual state* add_default_init();
    virtual std::string format_state(const spot::state* s) const;
326
327
328
329

    /// Create an alias for a state.  Any reference to \a alias_name
    /// will act as a reference to \a real_name.
    virtual
330
    void add_state_alias(const std::string& alias_name,
331
332
333
334
			 const std::string& real_name)
    {
      name_state_map_[alias_name] = add_state(real_name);
    }
335
336
337
338
339
340
341
342
343
344
345
346
347
  };

  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;
  };
348
349
350
351
352
353
354
355
356
357
358
359

  class tgba_explicit_number:
    public tgba_explicit_labelled<int, std::tr1::hash<int> >
  {
  public:
    tgba_explicit_number(bdd_dict* dict):
      tgba_explicit_labelled<int, std::tr1::hash<int> >(dict)
    {};
    virtual ~tgba_explicit_number();
    virtual state* add_default_init();
    virtual std::string format_state(const spot::state* s) const;
  };
360
361
362
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH