taproduct.cc 11.9 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
//
//
// 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.

#include "taproduct.hh"
#include <cassert>
#include "misc/hashfunc.hh"

namespace spot
{

  ////////////////////////////////////////////////////////////
  // state_ta_product

  state_ta_product::state_ta_product(const state_ta_product& o) :
    state(), ta_state_(o.get_ta_state()), kripke_state_(
35
        o.get_kripke_state()->clone())
36
37
38
39
40
41
  {
  }

  state_ta_product::~state_ta_product()
  {
    //see ta_product::free_state() method
42
    kripke_state_->destroy();
43
44
45
46
47
  }

  int
  state_ta_product::compare(const state* other) const
  {
48
    const state_ta_product* o = down_cast<const state_ta_product*> (other);
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
    assert(o);
    int res = ta_state_->compare(o->get_ta_state());
    if (res != 0)
      return res;
    return kripke_state_->compare(o->get_kripke_state());
  }

  size_t
  state_ta_product::hash() const
  {
    // We assume that size_t is 32-bit wide.
    return wang32_hash(ta_state_->hash()) ^ wang32_hash(kripke_state_->hash());
  }

  state_ta_product*
  state_ta_product::clone() const
  {
    return new state_ta_product(*this);
  }

  ////////////////////////////////////////////////////////////
  // ta_succ_iterator_product
  ta_succ_iterator_product::ta_succ_iterator_product(const state_ta_product* s,
72
73
74
						     const ta* t,
						     const kripke* k)
    : source_(s), ta_(t), kripke_(k)
75
  {
76
77
78
79
80
    kripke_source_condition = kripke_->state_condition(s->get_kripke_state());

    kripke_succ_it_ = kripke_->succ_iter(s->get_kripke_state());
    kripke_current_dest_state = 0;
    ta_succ_it_ = 0;
81
82
83
84
85
86
87
88
89
    current_state_ = 0;
  }

  ta_succ_iterator_product::~ta_succ_iterator_product()
  {
    delete current_state_;
    current_state_ = 0;
    delete ta_succ_it_;
    delete kripke_succ_it_;
90
    if (kripke_current_dest_state != 0)
91
      kripke_current_dest_state->destroy();
92
93
94
95
96
97
98
99
100
  }

  void
  ta_succ_iterator_product::step_()
  {
    if (!ta_succ_it_->done())
      ta_succ_it_->next();
    if (ta_succ_it_->done())
      {
101
102
        delete ta_succ_it_;
        ta_succ_it_ = 0;
103
        next_kripke_dest();
104
105
106
107
      }
  }

  void
108
  ta_succ_iterator_product::next_kripke_dest()
109
110
111
112
  {
    if (!kripke_succ_it_)
      return;

113
114
115
116
117
118
119
    if (kripke_current_dest_state == 0)
      {
        kripke_succ_it_->first();
      }
    else
      {
        kripke_current_dest_state->destroy();
120
        kripke_current_dest_state = 0;
121
122
123
        kripke_succ_it_->next();
      }

124
125
126
127
128
129
    // If one of the two successor sets is empty initially, we reset
    // kripke_succ_it_, so that done() can detect this situation easily.  (We
    // choose to reset kripke_succ_it_ because this variable is already used by
    // done().)
    if (kripke_succ_it_->done())
      {
130
131
132
        delete kripke_succ_it_;
        kripke_succ_it_ = 0;
        return;
133
134
      }

135
136
137
138
139
140
141
    kripke_current_dest_state = kripke_succ_it_->current_state();
    bdd kripke_current_dest_condition = kripke_->state_condition(
        kripke_current_dest_state);
    is_stuttering_transition_ = (kripke_source_condition
        == kripke_current_dest_condition);
    if (is_stuttering_transition_)
      {
142
        current_condition_ = bddfalse;
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
      }
    else
      {
        current_condition_ = bdd_setxor(kripke_source_condition,
            kripke_current_dest_condition);
        ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(),
            current_condition_);
        ta_succ_it_->first();
      }

  }

  void
  ta_succ_iterator_product::first()
  {

    next_kripke_dest();

    if (!done())
      next_non_stuttering_();
163
164
165
166
167
168
169
170
171
  }

  void
  ta_succ_iterator_product::next()
  {
    delete current_state_;
    current_state_ = 0;
    if (is_stuttering_transition())
      {
172
        next_kripke_dest();
173
174
175
176
177
      }
    else
      step_();

    if (!done())
178
      next_non_stuttering_();
179

180
181
182
183
184
185
186
187
  }

  void
  ta_succ_iterator_product::next_non_stuttering_()
  {

    while (!done())
      {
188
189
190
191
192

        if (is_stuttering_transition_)
          {
            //if stuttering transition, the TA automata stays in the same state
            current_state_ = new state_ta_product(source_->get_ta_state(),
193
                kripke_current_dest_state->clone());
194
            current_acceptance_conditions_ = bddfalse;
195
196
197
198
199
200
            return;
          }

        if (!ta_succ_it_->done())
          {
            current_state_ = new state_ta_product(ta_succ_it_->current_state(),
201
                kripke_current_dest_state->clone());
202
203
            current_acceptance_conditions_
                = ta_succ_it_->current_acceptance_conditions();
204
205
206
207
            return;
          }

        step_();
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
      }
  }

  bool
  ta_succ_iterator_product::done() const
  {
    return !kripke_succ_it_ || kripke_succ_it_->done();
  }

  state_ta_product*
  ta_succ_iterator_product::current_state() const
  {
    return current_state_->clone();
  }

  bool
  ta_succ_iterator_product::is_stuttering_transition() const
  {
    return is_stuttering_transition_;
  }

  bdd
  ta_succ_iterator_product::current_condition() const
  {
    return current_condition_;
  }

235
236
237
238
239
240
  bdd
  ta_succ_iterator_product::current_acceptance_conditions() const
  {
    return current_acceptance_conditions_;
  }

241
242
243
244
245
246
247
  ////////////////////////////////////////////////////////////
  // ta_product


  ta_product::ta_product(const ta* testing_automata,
      const kripke* kripke_structure) :
    dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_(
248
        kripke_structure)
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
  {
    assert(dict_ == kripke_structure->get_dict());
    dict_->register_all_variables_of(&ta_, this);
    dict_->register_all_variables_of(&kripke_, this);

  }

  ta_product::~ta_product()
  {
    dict_->unregister_all_my_variables(this);
  }

  const ta::states_set_t
  ta_product::get_initial_states_set() const
  {
    //build initial states set

266
    ta::states_set_t ta_init_states_set;
267
268
269
    ta::states_set_t::const_iterator it;

    ta::states_set_t initial_states_set;
270
271
272
    state* kripke_init_state = kripke_->get_init_state();
    bdd kripke_init_state_condition = kripke_->state_condition(
        kripke_init_state);
273

274
275
    spot::state* artificial_initial_state =
      ta_->get_artificial_initial_state();
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292

    if (artificial_initial_state != 0)
      {
        ta_succ_iterator* ta_init_it_ = ta_->succ_iter(
            artificial_initial_state, kripke_init_state_condition);
        for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next())
          {
            ta_init_states_set.insert(ta_init_it_->current_state());
          }
        delete ta_init_it_;

      }
    else
      {
        ta_init_states_set = ta_->get_initial_states_set();
      }

293
294
    for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++)
      {
295

296
297
        if ((artificial_initial_state != 0) || (kripke_init_state_condition
            == ta_->get_state_condition(*it)))
298
299
300
301
302
303
          {
            state_ta_product* stp = new state_ta_product((*it),
                kripke_init_state->clone());

            initial_states_set.insert(stp);
          }
304
305
306

      }

307
    kripke_init_state->destroy();
308
309
310
311
312
313
    return initial_states_set;
  }

  ta_succ_iterator_product*
  ta_product::succ_iter(const state* s) const
  {
314
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
315
316
317
318
319
    assert(s);

    return new ta_succ_iterator_product(stp, ta_, kripke_);
  }

320
321
322
323
324
325
326
327
328
329
330

  ta_succ_iterator_product*
  ta_product::succ_iter(const spot::state* s, bdd changeset) const
  {
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(s);
    return new ta_succ_iterator_product_by_changeset(stp, ta_, kripke_,
        changeset);

  }

331
332
333
334
335
336
337
338
339
  bdd_dict*
  ta_product::get_dict() const
  {
    return dict_;
  }

  std::string
  ta_product::format_state(const state* state) const
  {
340
    const state_ta_product* s = down_cast<const state_ta_product*> (state);
341
342
    assert(s);
    return kripke_->format_state(s->get_kripke_state()) + " * \n"
343
        + ta_->format_state(s->get_ta_state());
344
345
346
347
348
  }

  bool
  ta_product::is_accepting_state(const spot::state* s) const
  {
349
350
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(stp);
351
352
353
354
355
356
357

    return ta_->is_accepting_state(stp->get_ta_state());
  }

  bool
  ta_product::is_livelock_accepting_state(const spot::state* s) const
  {
358
359
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(stp);
360
361
362
363
364
365
366

    return ta_->is_livelock_accepting_state(stp->get_ta_state());
  }

  bool
  ta_product::is_initial_state(const spot::state* s) const
  {
367
368
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(stp);
369
370
371
372
373

    state* ta_s = stp->get_ta_state();
    state* kr_s = stp->get_kripke_state();

    return (ta_->is_initial_state(ta_s))
374
375
376
        && ((kripke_->get_init_state())->compare(kr_s) == 0)
        && ((kripke_->state_condition(kr_s))
            == (ta_->get_state_condition(ta_s)));
377
378
  }

379
380
381
382
383
384
385
386
387
388
  bool
  ta_product::is_hole_state_in_ta_component(const spot::state* s) const
  {
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    ta_succ_iterator* ta_succ_iter = get_ta()->succ_iter(stp->get_ta_state());
    bool is_hole_state = ta_succ_iter->done();
    delete ta_succ_iter;
    return is_hole_state;
  }

389
390
391
392
393
394
  bdd
  ta_product::all_acceptance_conditions() const
  {
    return get_ta()->all_acceptance_conditions();
  }

395
396
397
  bdd
  ta_product::get_state_condition(const spot::state* s) const
  {
398
399
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(stp);
400
401
402
403
404
405
406
407
    state* ta_s = stp->get_ta_state();
    return ta_->get_state_condition(ta_s);
  }

  void
  ta_product::free_state(const spot::state* s) const
  {

408
409
    const state_ta_product* stp = down_cast<const state_ta_product*> (s);
    assert(stp);
410
411
412
413
414
    ta_->free_state(stp->get_ta_state());
    delete stp;

  }

415
416
417
418
  ta_succ_iterator_product_by_changeset::
  ta_succ_iterator_product_by_changeset(const state_ta_product* s, const ta* t,
					const kripke* k, bdd changeset)
    : ta_succ_iterator_product(s, t, k)
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
  {
    current_condition_ = changeset;
  }

  void
  ta_succ_iterator_product_by_changeset::next_kripke_dest()
  {
    if (!kripke_succ_it_)
      return;

    if (kripke_current_dest_state == 0)
      {
        kripke_succ_it_->first();
      }
    else
      {
        kripke_current_dest_state->destroy();
        kripke_current_dest_state = 0;
        kripke_succ_it_->next();
      }

    // If one of the two successor sets is empty initially, we reset
    // kripke_succ_it_, so that done() can detect this situation easily.  (We
    // choose to reset kripke_succ_it_ because this variable is already used by
    // done().)
    if (kripke_succ_it_->done())
      {
        delete kripke_succ_it_;
        kripke_succ_it_ = 0;
        return;
      }

    kripke_current_dest_state = kripke_succ_it_->current_state();
    bdd kripke_current_dest_condition = kripke_->state_condition(
        kripke_current_dest_state);

    if (current_condition_ != bdd_setxor(kripke_source_condition,
        kripke_current_dest_condition))
      next_kripke_dest();
    is_stuttering_transition_ = (kripke_source_condition
        == kripke_current_dest_condition);
    if (!is_stuttering_transition_)
      {
        ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(),
            current_condition_);
        ta_succ_it_->first();
      }
  }
467
}