tgbaexplicit.hh 9.22 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
75
    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);
76

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

86
87
    virtual bdd all_acceptance_conditions() const;
    virtual bdd neg_acceptance_conditions() const;
88

89
90
    virtual std::string format_state(const spot::state* s) const = 0;

91
  protected:
92
93
94
    virtual bdd compute_support_conditions(const spot::state* state) const;
    virtual bdd compute_support_variables(const spot::state* state) const;

95
    bdd get_acceptance_condition(const ltl::formula* f);
96

97
    bdd_dict* dict_;
98
    tgba_explicit::state* init_;
99
100
101
    mutable bdd all_acceptance_conditions_;
    bdd neg_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
102
103
104
105

  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit& other);
106
    tgba_explicit& operator=(const tgba_explicit& other);
107
108
109
  };


110

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

    virtual int compare(const spot::state* other) const;
122
    virtual size_t hash() const;
123
124
    virtual state_explicit* clone() const;

125
126
127
128
129
130
131
132
133
134
    virtual ~state_explicit()
    {
    }

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


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

    virtual
    ~tgba_explicit_succ_iterator()
    {
    }

    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
181
182
183
184
185
186
187
188
189
190
191
192
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
321
322
323
324
325
326
327
328
329
330
331
  /// 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();
    }

    /// 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()
    {
      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)
	    delete *i2;
	  delete i->second;
	}
    }

  };

  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)
    {};
    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;
  };
332
333
334
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH