taatgba.hh 10.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2011, 2012, 2013 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
#ifndef SPOT_TGBA_TAATGBA_HH
# define SPOT_TGBA_TAATGBA_HH
22
23

#include <set>
Damien Lefortier's avatar
Damien Lefortier committed
24
#include <iosfwd>
25
26
27
28
29
30
31
32
#include <vector>
#include "misc/hash.hh"
#include "ltlast/formula.hh"
#include "bdddict.hh"
#include "tgba.hh"

namespace spot
{
33
34
  /// \brief A self-loop Transition-based Alternating Automaton (TAA)
  /// which is seen as a TGBA (abstract class, see below).
35
  class SPOT_API taa_tgba : public tgba
36
37
  {
  public:
38
    taa_tgba(bdd_dict* dict);
39
40
41
42
43
44
45
46
47
48
49
50
51
52

    struct transition;
    typedef std::list<transition*> state;
    typedef std::set<state*> state_set;

    /// Explicit transitions.
    struct transition
    {
      bdd condition;
      bdd acceptance_conditions;
      const state_set* dst;
    };

    void add_condition(transition* t, const ltl::formula* f);
Damien Lefortier's avatar
Damien Lefortier committed
53

54
    /// TGBA interface.
55
    virtual ~taa_tgba();
56
57
58
59
60
61
    virtual spot::state* get_init_state() const;
    virtual tgba_succ_iterator*
    succ_iter(const spot::state* local_state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const;
    virtual bdd_dict* get_dict() const;
62
    virtual std::string format_state(const spot::state* state) const = 0;
63
64
65
66
67
68
69
    virtual bdd all_acceptance_conditions() const;
    virtual bdd neg_acceptance_conditions() const;

  protected:
    virtual bdd compute_support_conditions(const spot::state* state) const;
    virtual bdd compute_support_variables(const spot::state* state) const;

70
    typedef std::vector<taa_tgba::state_set*> ss_vec;
71
72
73
74
75

    bdd_dict* dict_;
    mutable bdd all_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
    bdd neg_acceptance_conditions_;
76
    taa_tgba::state_set* init_;
77
78
79
80
    ss_vec state_set_vec_;

  private:
    // Disallow copy.
81
82
    taa_tgba(const taa_tgba& other) = delete;
    taa_tgba& operator=(const taa_tgba& other) = delete;
83
84
85
  };

  /// Set of states deriving from spot::state.
86
  class SPOT_API set_state : public spot::state
87
88
  {
  public:
89
    set_state(const taa_tgba::state_set* s, bool delete_me = false)
90
      : s_(s), delete_me_(delete_me)
91
92
93
94
95
    {
    }

    virtual int compare(const spot::state*) const;
    virtual size_t hash() const;
96
    virtual set_state* clone() const;
97

98
    virtual ~set_state()
99
    {
100
101
      if (delete_me_)
	delete s_;
102
103
    }

104
    const taa_tgba::state_set* get_state() const;
105
  private:
106
    const taa_tgba::state_set* s_;
107
    bool delete_me_;
108
109
  };

110
  class SPOT_API taa_succ_iterator : public tgba_succ_iterator
111
112
  {
  public:
113
    taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc);
Damien Lefortier's avatar
Damien Lefortier committed
114
    virtual ~taa_succ_iterator();
115
116
117
118
119

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

120
    virtual set_state* current_state() const;
121
122
123
124
    virtual bdd current_condition() const;
    virtual bdd current_acceptance_conditions() const;

  private:
125
126
    /// Those typedefs are used to generate all possible successors in
    /// the constructor using a cartesian product.
127
    typedef taa_tgba::state::const_iterator iterator;
128
129
    typedef std::pair<iterator, iterator> iterator_pair;
    typedef std::vector<iterator_pair> bounds_t;
130
131
132
    typedef std::unordered_map<const spot::set_state*,
			       std::vector<taa_tgba::transition*>,
			       state_ptr_hash, state_ptr_equal> seen_map;
133
134
135
136
137
138
139
140
141
142
143
144

    struct distance_sort :
      public std::binary_function<const iterator_pair&,
				  const iterator_pair&, bool>
    {
      bool
      operator()(const iterator_pair& lhs, const iterator_pair& rhs) const
      {
	return std::distance(lhs.first, lhs.second) <
	       std::distance(rhs.first, rhs.second);
      }
    };
145

146
147
    std::vector<taa_tgba::transition*>::const_iterator i_;
    std::vector<taa_tgba::transition*> succ_;
148
    bdd all_acceptance_conditions_;
Damien Lefortier's avatar
Damien Lefortier committed
149
    seen_map seen_;
150
  };
151
152
153
154

  /// A taa_tgba instance with states labeled by a given type.
  /// Still an abstract class, see below.
  template<typename label, typename label_hash>
155
  class SPOT_API taa_tgba_labelled : public taa_tgba
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
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
  {
  public:
    taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};

    void set_init_state(const label& s)
    {
      std::vector<label> v(1);
      v[0] = s;
      set_init_state(v);
    }
    void set_init_state(const std::vector<label>& s)
    {
      init_ = add_state_set(s);
    }

    transition*
    create_transition(const label& s,
		      const std::vector<label>& d)
    {
      state* src = add_state(s);
      state_set* dst = add_state_set(d);
      transition* t = new transition;
      t->dst = dst;
      t->condition = bddtrue;
      t->acceptance_conditions = bddfalse;
      src->push_back(t);
      return t;
    }
    transition*
    create_transition(const label& s, const label& d)
    {
      std::vector<std::string> vec;
      vec.push_back(d);
      return create_transition(s, vec);
    }

    void add_acceptance_condition(transition* t, const ltl::formula* f)
    {
      if (dict_->acc_map.find(f) == dict_->acc_map.end())
      {
	int v = dict_->register_acceptance_variable(f, this);
	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)
	{
	  taa_tgba::state::iterator i2;
	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	    (*i2)->acceptance_conditions &= neg;
	}

	all_acceptance_conditions_computed_ = false;
      }

      bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
      assert(i != dict_->acc_map.end());
      f->destroy();
      bdd v = bdd_ithvar(i->second);
      t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v);
    }

    /// \brief Format the state as a string for printing.
    ///
221
    /// If state is a spot::set_state of only one element, then the
222
223
224
    /// string corresponding to state->get_state() is returned.
    ///
    /// Otherwise a string composed of each string corresponding to
225
    /// each state->get_state() in the spot::set_state is returned,
226
227
228
    /// e.g. like {string_1,...,string_n}.
    virtual std::string format_state(const spot::state* s) const
    {
229
      const spot::set_state* se = down_cast<const spot::set_state*>(s);
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
      assert(se);
      const state_set* ss = se->get_state();
      return format_state_set(ss);
    }

    /// \brief Output a TAA in a stream.
    void output(std::ostream& os) const
    {
      typename ns_map::const_iterator i;
      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      {
	taa_tgba::state::const_iterator i2;
	os << "State: " << label_to_string(i->first) << std::endl;
	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	{
	  os << " " << format_state_set((*i2)->dst)
	     << ", C:" << (*i2)->condition
	     << ", A:" << (*i2)->acceptance_conditions << std::endl;
	}
      }
    }

  protected:
253
254
    typedef label label_t;

255
256
257
258
    typedef std::unordered_map<const label, taa_tgba::state*,
			       label_hash> ns_map;
    typedef std::unordered_map<const taa_tgba::state*, label,
			       ptr_hash<taa_tgba::state>> sn_map;
259
260
261
262
263

    ns_map name_state_map_;
    sn_map state_name_map_;

    /// \brief Return a label as a string.
264
265
266
267
268
    virtual std::string label_to_string(const label_t& lbl) const = 0;

    /// \brief Clone the label if necessary to assure it is owned by
    /// this, avoiding memory issues when label is a pointer.
    virtual label_t clone_if(const label_t& lbl) const = 0;
269
270
271
272
273
274
275
276
277

  private:
    /// \brief Return the taa_tgba::state for \a name, creating it
    /// when it does not exist already.
    taa_tgba::state* add_state(const label& name)
    {
      typename ns_map::iterator i = name_state_map_.find(name);
      if (i == name_state_map_.end())
      {
278
	const label& name_ = clone_if(name);
279
	taa_tgba::state* s = new taa_tgba::state;
280
281
	name_state_map_[name_] = s;
	state_name_map_[s] = name_;
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
	return s;
      }
      return i->second;
    }

    /// \brief Return the taa::state_set for \a names.
    taa_tgba::state_set* add_state_set(const std::vector<label>& names)
    {
      state_set* ss = new state_set;
      for (unsigned i = 0; i < names.size(); ++i)
	ss->insert(add_state(names[i]));
      state_set_vec_.push_back(ss);
      return ss;
    }

    std::string format_state_set(const taa_tgba::state_set* ss) const
    {
      state_set::const_iterator i1 = ss->begin();
      typename sn_map::const_iterator i2;
      if (ss->empty())
	return std::string("{}");
      if (ss->size() == 1)
      {
	i2 = state_name_map_.find(*i1);
	assert(i2 != state_name_map_.end());
	return "{" + label_to_string(i2->second) + "}";
      }
      else
      {
	std::string res("{");
	while (i1 != ss->end())
	{
	  i2 = state_name_map_.find(*i1++);
	  assert(i2 != state_name_map_.end());
	  res += label_to_string(i2->second);
	  res += ",";
	}
	res[res.size() - 1] = '}';
	return res;
      }
    }
  };

325
  class SPOT_API taa_tgba_string :
326
327
328
329
330
    public taa_tgba_labelled<std::string, string_hash>
  {
  public:
    taa_tgba_string(bdd_dict* dict) :
      taa_tgba_labelled<std::string, string_hash>(dict) {};
331
    ~taa_tgba_string();
332
  protected:
333
334
    virtual std::string label_to_string(const std::string& label) const;
    virtual std::string clone_if(const std::string& label) const;
335
336
  };

337
  class SPOT_API taa_tgba_formula :
338
339
340
    public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
  {
  public:
341
    taa_tgba_formula(bdd_dict* dict) :
342
      taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
343
    ~taa_tgba_formula();
344
  protected:
345
    virtual std::string label_to_string(const label_t& label) const;
346
    virtual const ltl::formula* clone_if(const label_t& label) const;
347
  };
348
349
}

350
#endif // SPOT_TGBA_TAATGBA_HH