tgbatba.cc 7.91 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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
25
26
27
28
#include <cassert>
#include "tgbatba.hh"
#include "bddprint.hh"
#include "ltlast/constant.hh"

namespace spot
{
29
  namespace
30
  {
31
32
33
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
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
184
185
186
187
188
189
190
191
192
193
    /// \brief A state for spot::tgba_tba_proxy.
    ///
    /// This state is in fact a pair of state: the state from the tgba
    /// automaton, and a state of the "counter" (we use a pointer
    /// to the position in the cycle_acc_ list).
    class state_tba_proxy: public state
    {
      typedef tgba_tba_proxy::cycle_list::const_iterator iterator;
    public:
      state_tba_proxy(state* s, iterator acc)
	:	s_(s), acc_(acc)
      {
      }

      /// Copy constructor
      state_tba_proxy(const state_tba_proxy& o)
	: state(),
	  s_(o.real_state()->clone()),
	  acc_(o.acceptance_iterator())
      {
      }

      virtual
      ~state_tba_proxy()
      {
	delete s_;
      }

      state*
      real_state() const
      {
	return s_;
      }

      bdd
      acceptance_cond() const
      {
	return *acc_;
      }

      iterator
      acceptance_iterator() const
      {
	return acc_;
      }

      virtual int
      compare(const state* other) const
      {
	const state_tba_proxy* o = dynamic_cast<const state_tba_proxy*>(other);
	assert(o);
	int res = s_->compare(o->real_state());
	if (res != 0)
	  return res;
	return acc_->id() - o->acceptance_cond().id();
      }

      virtual size_t
      hash() const
      {
	// We expect to have many more states than acceptance conditions.
	// Hence we keep only 8 bits for acceptance conditions.
	return (s_->hash() << 8) + (acc_->id() & 0xFF);
      }

      virtual
      state_tba_proxy* clone() const
      {
	return new state_tba_proxy(*this);
      }

    private:
      state* s_;
      iterator acc_;
    };


    /// \brief Iterate over the successors of tgba_tba_proxy computed
    /// on the fly.
    class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator
    {
      typedef tgba_tba_proxy::cycle_list list;
      typedef tgba_tba_proxy::cycle_list::const_iterator iterator;
    public:
      tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
				   iterator expected, iterator end,
				   bdd the_acceptance_cond)
	: it_(it), expected_(expected), end_(end),
	  the_acceptance_cond_(the_acceptance_cond)
      {
      }

      virtual
      ~tgba_tba_proxy_succ_iterator()
      {
	delete it_;
      }

      // iteration

      void
      first()
      {
	it_->first();
      }

      void
      next()
      {
	it_->next();
      }

      bool
      done() const
      {
	return it_->done();
      }

      // inspection

      state_tba_proxy*
      current_state() const
      {
	// A transition in the *EXPECTED acceptance set should be directed
	// to the next acceptance set.  If the current transition is also
	// in the next acceptance set, then go the one after, etc.
	//
	// See Denis Oddoux's PhD thesis for a nice explanation (in French).
	//  @PhDThesis{	  oddoux.03.phd,
	//    author	= {Denis Oddoux},
	//    title	= {Utilisation des automates alternants pour un
	//  		  model-checking efficace des logiques temporelles
	//  		  lin{\'e}aires.},
	//    school	= {Universit{\'e}e Paris 7},
	//    year	= {2003},
	//    address	= {Paris, France},
	//    month	= {December}
	//  }
	//
	iterator next = expected_;
	bdd acc = it_->current_acceptance_conditions();
	while ((acc & *next) == *next && next != end_)
	  ++next;
	return new state_tba_proxy(it_->current_state(), next);
      }

      bdd
      current_condition() const
      {
	return it_->current_condition();
      }

      bdd
      current_acceptance_conditions() const
      {
	return the_acceptance_cond_;
      }

    protected:
      tgba_succ_iterator* it_;
      const iterator expected_;
      const iterator end_;
      const bdd the_acceptance_cond_;
194
      friend class tgba_tba_proxy;
195
196
197
    };

  } // anonymous
198
199
200
201

  tgba_tba_proxy::tgba_tba_proxy(const tgba* a)
    : a_(a)
  {
202
    bdd all = a_->all_acceptance_conditions();
203

204
    // We will use one acceptance condition for this automata.
205
206
    // Let's call it Acc[True].
    int v = get_dict()
207
208
      ->register_acceptance_variable(ltl::constant::true_instance(), this);
    the_acceptance_cond_ = bdd_ithvar(v);
209

210
    // Now build the "cycle" of acceptance conditions.
211

212
    acc_cycle_.push_front(bddtrue);
213
214
215
216

    while (all != bddfalse)
      {
	bdd next = bdd_satone(all);
217
	all -= next;
218
	acc_cycle_.push_front(next);
219
220
221
222
223
224
225
226
      }
  }

  tgba_tba_proxy::~tgba_tba_proxy()
  {
    get_dict()->unregister_all_my_variables(this);
  }

227
  state*
228
229
  tgba_tba_proxy::get_init_state() const
  {
230
    return new state_tba_proxy(a_->get_init_state(), acc_cycle_.begin());
231
232
233
234
235
236
237
  }

  tgba_succ_iterator*
  tgba_tba_proxy::succ_iter(const state* local_state,
			    const state* global_state,
			    const tgba* global_automaton) const
  {
238
    const state_tba_proxy* s =
239
240
241
      dynamic_cast<const state_tba_proxy*>(local_state);
    assert(s);

242
    tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
243
					   global_state, global_automaton);
244
245
246
247
248
249
250
251

    cycle_list::const_iterator j = s->acceptance_iterator();
    cycle_list::const_iterator i = j++;
    if (j == acc_cycle_.end())
      return new tgba_tba_proxy_succ_iterator(it, acc_cycle_.begin(),
					      acc_cycle_.end(),
					      the_acceptance_cond_);
    return new tgba_tba_proxy_succ_iterator(it, i, acc_cycle_.end(), bddfalse);
252
  }
253
254

  bdd_dict*
255
256
257
258
  tgba_tba_proxy::get_dict() const
  {
    return a_->get_dict();
  }
259
260

  std::string
261
262
  tgba_tba_proxy::format_state(const state* state) const
  {
263
    const state_tba_proxy* s = dynamic_cast<const state_tba_proxy*>(state);
264
    assert(s);
265
266
267
268
    std::string a = bdd_format_accset(get_dict(), s->acceptance_cond());
    if (a != "")
      a = " " + a;
    return a_->format_state(s->real_state()) + a;
269
  }
270

271
  state*
272
273
274
275
276
277
278
279
280
281
  tgba_tba_proxy::project_state(const state* s, const tgba* t) const
  {
    const state_tba_proxy* s2 = dynamic_cast<const state_tba_proxy*>(s);
    assert(s2);
    if (t == this)
      return s2->clone();
    return a_->project_state(s2->real_state(), t);
  }


282
  bdd
283
  tgba_tba_proxy::all_acceptance_conditions() const
284
  {
285
    return the_acceptance_cond_;
286
  }
287
288

  bdd
289
  tgba_tba_proxy::neg_acceptance_conditions() const
290
  {
291
    return !the_acceptance_cond_;
292
  }
293
294
295
296
297
298
299

  bool
  tgba_tba_proxy::state_is_accepting(const state* state) const
  {
    const state_tba_proxy* s =
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
300
    return bddtrue == s->acceptance_cond();
301
302
303
  }

  bdd
304
305
  tgba_tba_proxy::compute_support_conditions(const state* state) const
  {
306
    const state_tba_proxy* s =
307
308
309
310
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
    return a_->support_conditions(s->real_state());
  }
311
312

  bdd
313
314
  tgba_tba_proxy::compute_support_variables(const state* state) const
  {
315
    const state_tba_proxy* s =
316
317
318
319
320
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
    return a_->support_variables(s->real_state());
  }

321
322
323
324
325
326
327
328
329
  std::string
  tgba_tba_proxy::transition_annotation(const tgba_succ_iterator* t) const
  {
    const tgba_tba_proxy_succ_iterator* i =
      dynamic_cast<const tgba_tba_proxy_succ_iterator*>(t);
    assert(i);
    return a_->transition_annotation(i->it_);
  }

330
}