ssp.cc 30.8 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
4
// Copyright (C) 2003, 2004, 2005, 2006, 2007  Laboratoire
5
6
// 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
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
24
25
26
#include <cstring>
#include <map>
#include <cassert>
#include <gspnlib.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
27
#include "ssp.hh"
28
#include "misc/bddlt.hh"
29
#include "misc/hash.hh"
30
#include <bdd.h>
31
32
#include "tgbaalgos/gtec/explscc.hh"
#include "tgbaalgos/gtec/nsheap.hh"
33
34
35
36

namespace spot
{

37
38
39
40
41
42
43
44
  namespace
  {
    static bdd*
    bdd_realloc(bdd* t, int size, int new_size)
    {
      assert(new_size);
      bdd* tmp = new bdd[new_size];

45
      for (int i = 0; i < size; i++)
46
47
48
49
50
	tmp[i] = t[i];

      delete[] t;
      return tmp;
    }
51
52

    static bool doublehash;
53
    static bool pushfront;
54
55
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
56
  // state_gspn_ssp
57
58
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
  class state_gspn_ssp: public state
60
61
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
    state_gspn_ssp(State left, const state* right)
63
64
65
66
67
      : left_(left), right_(right)
    {
    }

    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
68
    ~state_gspn_ssp()
69
    {
70
      right_->destroy();
71
72
73
74
75
    }

    virtual int
    compare(const state* other) const
    {
76
      const state_gspn_ssp* o = down_cast<const state_gspn_ssp*>(other);
77
      assert(o);
78
79
80
81
82
83
      if (o->left() == left())
	return right_->compare(o->right());
      if (o->left() < left())
	return -1;
      else
	return 1;
84
85
86
87
88
    }

    virtual size_t
    hash() const
    {
89
90
      return ((reinterpret_cast<char*>(left())
	       - static_cast<char*>(0)) << 10) + right_->hash();
91
92
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
93
    virtual state_gspn_ssp* clone() const
94
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
95
      return new state_gspn_ssp(left(), right()->clone());
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
    }

    State
    left() const
    {
      return left_;
    }

    const state*
    right() const
    {
      return right_;
    }

  private:
    State left_;
    const state* right_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
113
  }; // state_gspn_ssp
114

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
  // tgba_gspn_ssp_private_
116
117
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
118
  struct tgba_gspn_ssp_private_
119
120
121
122
123
124
125
126
127
128
129
130
  {
    int refs;			// reference count

    bdd_dict* dict;
    typedef std::map<int, AtomicProp> prop_map;
    prop_map prop_dict;

    signed char* all_props;

    size_t prop_count;
    const tgba* operand;

131
132
133
    tgba_gspn_ssp_private_(bdd_dict* dict,
			   const ltl::declarative_environment& env,
			   const tgba* operand)
134
135
136
      : refs(1), dict(dict), all_props(0),
	operand(operand)
    {
137
      const ltl::declarative_environment::prop_map& p = env.get_prop_map();
138
139
140
141
142

      try
	{
	  AtomicProp max_prop = 0;

143
144
	  for (ltl::declarative_environment::prop_map::const_iterator i
		 = p.begin(); i != p.end(); ++i)
145
146
147
148
149
	    {
	      int var = dict->register_proposition(i->second, this);
	      AtomicProp index;
	      int err = prop_index(i->first.c_str(), &index);
	      if (err)
150
		throw gspn_exception("prop_index(" + i->first + ")", err);
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167

	      prop_dict[var] = index;

	      max_prop = std::max(max_prop, index);
	    }
	  prop_count = 1 + max_prop;
	  all_props = new signed char[prop_count];
	}
      catch (...)
	{
	  // If an exception occurs during the loop, we need to clean
	  // all BDD variables which have been registered so far.
	  dict->unregister_all_my_variables(this);
	  throw;
	}
    }

168
    ~tgba_gspn_ssp_private_()
169
170
    {
      dict->unregister_all_my_variables(this);
171
      delete[] all_props;
172
173
174
175
    }
  };


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
176
  // tgba_succ_iterator_gspn_ssp
177
178
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
179
  class tgba_succ_iterator_gspn_ssp: public tgba_succ_iterator
180
181
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
182
    tgba_succ_iterator_gspn_ssp(Succ_* succ_tgba,
183
184
185
186
187
188
				size_t size_tgba,
				bdd* bdd_array,
				state** state_array,
				size_t size_states,
				Props_* prop,
				int size_prop)
189
190
191
      : successors_(succ_tgba),
	size_succ_(size_tgba),
	current_succ_(0),
192
193
	bdd_array_(bdd_array),
	state_array_(state_array),
194
195
196
	size_states_(size_states),
	props_(prop),
	size_prop_(size_prop)
197
198
199
200
    {
    }

    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
201
    ~tgba_succ_iterator_gspn_ssp()
202
203
    {

204
      for (size_t i = 0; i < size_states_; i++)
205
	state_array_[i]->destroy();
206

207
208
      delete[] bdd_array_;
      free(state_array_);
209

210
211
212
213
214
215
      if (props_)
	{
	  for (int i = 0; i < size_prop_; i++)
	    free(props_[i].arc);
	  free(props_);
	}
216

217
218
      if (size_succ_ != 0)
	succ_free(successors_);
219

220
221
222
223
224
    }

    virtual void
    first()
    {
225
226
      if (!successors_)
	return;
227
      current_succ_=0;
228
229
230
231
232
    }

    virtual void
    next()
    {
233
      ++current_succ_;
234
235
236
237
238
    }

    virtual bool
    done() const
    {
239
      return current_succ_ + 1 > size_succ_;
240
241
242
243
244
    }

    virtual state*
    current_state() const
    {
245
      state_gspn_ssp* s =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
246
	new state_gspn_ssp(successors_[current_succ_].succ_,
247
248
			   (state_array_[successors_[current_succ_]
					 .arc->curr_state])->clone());
249
      return s;
250
251
252
253
254
255
256
257
258
    }

    virtual bdd
    current_condition() const
    {
      return bddtrue;
    }

    virtual bdd
259
    current_acceptance_conditions() const
260
261
    {
      // There is no acceptance conditions in GSPN systems, so we just
262
      // return those from operand_.
263
      return bdd_array_[successors_[current_succ_].arc->curr_acc_conds];
264
265
    }
  private:
266

267
268
    // All successors of STATE matching a selection conjunctions from
    // ALL_CONDS.
269
270
    Succ_* successors_;		/// array of successors
    size_t size_succ_;		/// size of successors_
271
    size_t current_succ_;	/// current position in successors_
272
273
274
275
276
277

    bdd * bdd_array_;
    state** state_array_;
    size_t size_states_;
    Props_* props_;
    int size_prop_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
278
  }; // tgba_succ_iterator_gspn_ssp
279
280


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
281
  // tgba_gspn_ssp
282
283
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
284
  class tgba_gspn_ssp: public tgba
285
286
  {
  public:
287
288
    tgba_gspn_ssp(bdd_dict* dict, const ltl::declarative_environment& env,
		  const tgba* operand);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
289
290
291
    tgba_gspn_ssp(const tgba_gspn_ssp& other);
    tgba_gspn_ssp& operator=(const tgba_gspn_ssp& other);
    virtual ~tgba_gspn_ssp();
292
293
294
295
296
297
298
299
300
301
302
303
304
305
    virtual state* get_init_state() const;
    virtual tgba_succ_iterator*
    succ_iter(const state* local_state,
	      const state* global_state = 0,
	      const tgba* global_automaton = 0) const;
    virtual bdd_dict* get_dict() const;
    virtual std::string format_state(const state* state) const;
    virtual state* project_state(const state* s, const tgba* t) const;
    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;
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
306
    tgba_gspn_ssp_private_* data_;
307
  };
308

309
310
311
  tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict,
			       const ltl::declarative_environment& env,
			       const tgba* operand)
312
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
313
    data_ = new tgba_gspn_ssp_private_(dict, env, operand);
314
315
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
316
  tgba_gspn_ssp::tgba_gspn_ssp(const tgba_gspn_ssp& other)
317
318
319
320
321
322
    : tgba()
  {
    data_ = other.data_;
    ++data_->refs;
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
323
  tgba_gspn_ssp::~tgba_gspn_ssp()
324
325
326
327
328
  {
    if (--data_->refs == 0)
      delete data_;
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
329
330
  tgba_gspn_ssp&
  tgba_gspn_ssp::operator=(const tgba_gspn_ssp& other)
331
332
333
  {
    if (&other == this)
      return *this;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
334
335
    this->~tgba_gspn_ssp();
    new (this) tgba_gspn_ssp(other);
336
337
338
    return *this;
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
339
  state* tgba_gspn_ssp::get_init_state() const
340
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
341
    // Use 0 as initial state for the SSP side.  State 0 does not
342
343
    // exists, but when passed to succ() it will produce the list
    // of initial states.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
344
    return new state_gspn_ssp(0, data_->operand->get_init_state());
345
346
347
  }

  tgba_succ_iterator*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
348
  tgba_gspn_ssp::succ_iter(const state* state_,
349
350
			   const state* global_state,
			   const tgba* global_automaton) const
351
  {
352
    const state_gspn_ssp* s = down_cast<const state_gspn_ssp*>(state_);
353
354
355
    assert(s);
    (void) global_state;
    (void) global_automaton;
356
357
358
359
360
361
362
363
364
365
366
367

    bdd all_conds_;
    bdd outside_;
    bdd cond;

    Props_* props_ = 0;
    int nb_arc_props = 0;
    bdd* bdd_array = 0;
    int size_bdd = 0;
    state** state_array = 0;
    size_t size_states = 0;

368
    tgba_succ_iterator* i = data_->operand->succ_iter(s->right());
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387

    for (i->first(); !i->done(); i->next())
      {
	all_conds_ = i->current_condition();
	outside_ = !all_conds_;

	if (all_conds_ != bddfalse)
	  {
	    props_ = (Props_*) realloc(props_,
				       (nb_arc_props + 1) * sizeof(Props_));

	    props_[nb_arc_props].nb_conj = 0;
	    props_[nb_arc_props].prop = 0;
	    props_[nb_arc_props].arc =
	      (Arc_Ident_*) malloc(sizeof(Arc_Ident_));

	    bdd_array = bdd_realloc(bdd_array, size_bdd, size_bdd + 1);
	    bdd_array[size_bdd] = i->current_acceptance_conditions();
	    props_[nb_arc_props].arc->curr_acc_conds = size_bdd;
388
	    ++size_bdd;
389

390
391
392
            state_array =
	      (state**) realloc(state_array,
				(size_states + 1) * sizeof(state*));
393
	    state_array[size_states] = i->current_state();
394
	    props_[nb_arc_props].arc->curr_state = size_states;
395
            ++size_states;
396

397
	    while (all_conds_ != bddfalse)
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
	      {
		cond = bdd_satone(all_conds_);
		cond = bdd_simplify(cond, cond | outside_);
		all_conds_ -= cond;

		props_[nb_arc_props].prop =
		  (signed char **) realloc(props_[nb_arc_props].prop,
					   (props_[nb_arc_props].nb_conj + 1)
					   * sizeof(signed char *));

		props_[nb_arc_props].prop[props_[nb_arc_props].nb_conj]
		  = (signed char*) calloc(data_->prop_count,
					  sizeof(signed char));
		memset(props_[nb_arc_props].prop[props_[nb_arc_props].nb_conj],
		       -1, data_->prop_count);

		while (cond != bddtrue)
		  {
		    int var = bdd_var(cond);
		    bdd high = bdd_high(cond);
		    int res;

		    if (high == bddfalse)
		      {
			cond = bdd_low(cond);
			res = 0;
		      }
		    else
		      {
			cond = high;
			res = 1;
		      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
431
		    tgba_gspn_ssp_private_::prop_map::iterator k
432
433
434
435
436
437
438
439
440
441
442
443
444
		      = data_->prop_dict.find(var);

		    if (k != data_->prop_dict.end())
		      props_[nb_arc_props]
			.prop[props_[nb_arc_props].nb_conj][k->second] = res;

		    assert(cond != bddfalse);
		  }
		++props_[nb_arc_props].nb_conj;
	      }
	    ++nb_arc_props;
	  }
      }
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
    Succ_* succ_tgba_ = 0;
    size_t size_tgba_ = 0;
    int j, conj;

    succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_);

    for (j = 0; j < nb_arc_props; j++)
      {
	for (conj = 0; conj < props_[j].nb_conj; conj++)
	  free(props_[j].prop[conj]);
	free(props_[j].prop);
      }

    delete i;
    return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_,
					   bdd_array, state_array,
					   size_states, props_,
					   nb_arc_props);
463
464
465
  }

  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
466
  tgba_gspn_ssp::compute_support_conditions(const spot::state* state) const
467
468
469
470
471
472
  {
    (void) state;
    return bddtrue;
  }

  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
473
  tgba_gspn_ssp::compute_support_variables(const spot::state* state) const
474
475
476
477
478
479
  {
    (void) state;
    return bddtrue;
  }

  bdd_dict*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
480
  tgba_gspn_ssp::get_dict() const
481
482
483
484
485
  {
    return data_->dict;
  }

  std::string
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
486
  tgba_gspn_ssp::format_state(const state* state) const
487
  {
488
    const state_gspn_ssp* s = down_cast<const state_gspn_ssp*>(state);
489
490
    assert(s);
    char* str;
491
492
493
494
495
    State gs = s->left();
    if (gs)
      {
	int err = print_state(gs, &str);
	if (err)
496
	  throw gspn_exception("print_state()", err);
497
498
499
500
	// Strip trailing \n...
	unsigned len = strlen(str);
	while (str[--len] == '\n')
	  str[len] = 0;
501
502
503
504
505
      }
    else
      {
	str = strdup("-1");
      }
506

507
    std::string res(str);
508
    free(str);
509
    return res + " * " + data_->operand->format_state(s->right());
510
511
  }

512
  state*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
513
  tgba_gspn_ssp::project_state(const state* s, const tgba* t) const
514
  {
515
    const state_gspn_ssp* s2 = down_cast<const state_gspn_ssp*>(s);
516
517
518
519
520
521
    assert(s2);
    if (t == this)
      return s2->clone();
    return data_->operand->project_state(s2->right(), t);
  }

522
  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
523
  tgba_gspn_ssp::all_acceptance_conditions() const
524
  {
525
526
527
    // There is no acceptance conditions in GSPN systems, they all
    // come from the operand automaton.
    return data_->operand->all_acceptance_conditions();
528
529
530
  }

  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
531
  tgba_gspn_ssp::neg_acceptance_conditions() const
532
  {
533
534
535
    // There is no acceptance conditions in GSPN systems, they all
    // come from the operand automaton.
    return data_->operand->neg_acceptance_conditions();
536
537
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
538
  // gspn_ssp_interface
539
540
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
541
  gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv,
542
					 bdd_dict* dict,
543
544
					 const
					 ltl::declarative_environment& env,
545
					 bool inclusion,
546
547
					 bool doublehash_,
					 bool pushfront_)
548
549
    : dict_(dict), env_(env)
  {
550
    doublehash = doublehash_;
551
    pushfront = pushfront_;
552
553
554
    if (inclusion)
      inclusion_version();

555
556
    int res = initialize(argc, argv);
    if (res)
557
      throw gspn_exception("initialize()", res);
558
559
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
560
  gspn_ssp_interface::~gspn_ssp_interface()
561
562
563
  {
    int res = finalize();
    if (res)
564
      throw gspn_exception("finalize()", res);
565
566
567
  }

  tgba*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
568
  gspn_ssp_interface::automaton(const tgba* operand) const
569
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
570
    return new tgba_gspn_ssp(dict_, env_, operand);
571
572
  }

573
574
575

  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
576
  class connected_component_ssp: public explicit_connected_component
577
578
579
  {
  public:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
580
    ~connected_component_ssp()
581
582
583
584
585
586
    {
    }

    virtual const state*
    has_state(const state* s) const
    {
587
      set_type::const_iterator i;
588

589
      for (i = states.begin(); i != states.end(); ++i)
590
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
591
592
	  const state_gspn_ssp* old_state = (const state_gspn_ssp*)(*i);
	  const state_gspn_ssp* new_state = (const state_gspn_ssp*)(s);
593
594
595
596
597

	  if ((old_state->right())->compare(new_state->right()) == 0
	      && old_state->left()
	      && new_state->left())
	    if (spot_inclusion(new_state->left(), old_state->left()))
598
599
	      {
		if (*i != s)
600
		  s->destroy();
601
602
		return *i;
	      }
603
604
605
606
607
608
609
610
611
612
613
	}
      return 0;
    }

    virtual void
    insert(const state* s)
    {
      states.insert(s);
    }

  protected:
614
615
    typedef std::unordered_set<const state*,
			       state_ptr_hash, state_ptr_equal> set_type;
616
617
618
    set_type states;
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
619
  class connected_component_ssp_factory :
620
621
622
    public explicit_connected_component_factory
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
623
    virtual connected_component_ssp*
624
625
    build() const
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
626
      return new connected_component_ssp();
627
628
629
    }

    /// Get the unique instance of this class.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
630
    static const connected_component_ssp_factory*
631
632
    instance()
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
633
      static connected_component_ssp_factory f;
634
635
636
637
638
      return &f;
    }

  protected:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
639
    ~connected_component_ssp_factory()
640
641
642
    {
    }
    /// Construction is forbiden.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
643
    connected_component_ssp_factory()
644
645
646
647
648
649
    {
    }
  };

  //////////////////////////////////////////////////////////////////////

650
651
652
653
654
655
656
657
  namespace
  {
    inline void*
    container_(const State s)
    {
      return doublehash ? container(s) : 0;
    }
  }
658

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
659
  class numbered_state_heap_ssp_semi : public numbered_state_heap
660
661
  {
  public:
662
663
664
665
666
    numbered_state_heap_ssp_semi()
      : numbered_state_heap(), inclusions(0)
    {
    }

667
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
668
    ~numbered_state_heap_ssp_semi()
669
670
671
672
673
674
675
676
    {
      // Free keys in H.
      hash_type::iterator i = h.begin();
      while (i != h.end())
	{
	  // Advance the iterator before deleting the key.
	  const state* s = i->first;
	  ++i;
677
	  s->destroy();
678
679
680
	}
    }

681
    virtual numbered_state_heap::state_index
682
683
    find(const state* s) const
    {
684
      const state_gspn_ssp* s_ = down_cast<const state_gspn_ssp*>(s);
685
      const void* cont = container_(s_->left());
686
687
      contained_map::const_iterator i = contained.find(cont);
      if (i != contained.end())
688
	{
689
690
	  f_map::const_iterator k = i->second.find(s_->right());
	  if (k != i->second.end())
691
	    {
692
693
694
695
	      const state_list& l = k->second;

	      state_list::const_iterator j;
	      for (j = l.begin(); j != l.end(); ++j)
696
		{
697
		  const state_gspn_ssp* old_state =
698
		    down_cast<const state_gspn_ssp*>(*j);
699
		  const state_gspn_ssp* new_state =
700
		    down_cast<const state_gspn_ssp*>(s);
701
702
703
		  assert(old_state);
		  assert(new_state);

704
705
		  if (old_state->left() == new_state->left())
		    break;
706

707
708
709
		  if (old_state->left()
		      && new_state->left()
		      && spot_inclusion(new_state->left(), old_state->left()))
710
711
712
713
		    {
		      ++inclusions;
		      break;
		    }
714
		}
715
	      if (j != l.end())
716
		{
717
718
		  if (s != *j)
		    {
719
		      s->destroy();
720
721
722
723
724
725
		      s = *j;
		    }
		}
	      else
		{
		  s = 0;
726
727
728
729
730
731
732
733
734
735
		}
	    }
	  else
	    {
	      s = 0;
	    }
	}
      else
	{
	  s = 0;
736
737
	}

738
739
740
      state_index res;

      if (s == 0)
741
742
743
744
745
746
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
747
748
749
	  hash_type::const_iterator i = h.find(s);
	  assert(i != h.end());
	  assert(s == i->first);
750
751
752
753
	  res.first = i->first;
	  res.second = i->second;
	}
      return res;
754
755
    }

756
757
    virtual numbered_state_heap::state_index_p
    find(const state* s)
758
    {
759
      const state_gspn_ssp* s_ = down_cast<const state_gspn_ssp*>(s);
760
      const void* cont = container_(s_->left());
761
762
      contained_map::const_iterator i = contained.find(cont);
      if (i != contained.end())
763
	{
764
765
	  f_map::const_iterator k = i->second.find(s_->right());
	  if (k != i->second.end())
766
	    {
767
768
769
770
	      const state_list& l = k->second;

	      state_list::const_iterator j;
	      for (j = l.begin(); j != l.end(); ++j)
771
		{
772
		  const state_gspn_ssp* old_state =
773
		    down_cast<const state_gspn_ssp*>(*j);
774
		  const state_gspn_ssp* new_state =
775
		    down_cast<const state_gspn_ssp*>(s);
776
777
778
		  assert(old_state);
		  assert(new_state);

779
780
		  if (old_state->left() == new_state->left())
		    break;
781

782
783
784
		  if (old_state->left()
		      && new_state->left()
		      && spot_inclusion(new_state->left(), old_state->left()))
785
786
787
788
		    {
		      ++inclusions;
		      break;
		    }
789
		}
790
	      if (j != l.end())
791
		{
792
793
		  if (s != *j)
		    {
794
		      s->destroy();
795
796
797
798
799
800
		      s = *j;
		    }
		}
	      else
		{
		  s = 0;
801
802
803
804
805
		}
	    }
	  else
	    {
	      s = 0;
806
807
	    }
	}
808
809
810
811
      else
	{
	  s = 0;
	}
812

813
814
815
      state_index_p res;

      if (s == 0)
816
817
818
819
820
821
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
822
823
824
	  hash_type::iterator i = h.find(s);
	  assert(i != h.end());
	  assert(s == i->first);
825
826
827
828
	  res.first = i->first;
	  res.second = &i->second;
	}
      return res;
829
830
    }

831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
    virtual numbered_state_heap::state_index
    index(const state* s) const
    {
      state_index res;
      hash_type::const_iterator i = h.find(s);
      if (i == h.end())
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
	  res.first = i->first;
	  res.second = i->second;

	  if (s != i->first)
847
	    s->destroy();
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
	}
      return res;
    }

    virtual numbered_state_heap::state_index_p
    index(const state* s)
    {
      state_index_p res;
      hash_type::iterator i = h.find(s);
      if (i == h.end())
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
	  res.first = i->first;
	  res.second = &i->second;

	  if (s != i->first)
868
	    s->destroy();
869
870
871
872
873
874
875
876
	}
      return res;
    }

    virtual void
    insert(const state* s, int index)
    {
      h[s] = index;
877

878
      const state_gspn_ssp* s_ = down_cast<const state_gspn_ssp*>(s);
879
      State sg = s_->left();
880
881
882
      if (sg)
	{
	  const void* cont = container_(sg);
883
884
885
886
	  if (pushfront)
	    contained[cont][s_->right()].push_front(s);
	  else
	    contained[cont][s_->right()].push_back(s);
887
	}
888
889
890
891
892
893
894
895
896
897
    }

    virtual int
    size() const
    {
      return h.size();
    }

    virtual numbered_state_heap_const_iterator* iterator() const;

898
  protected:
899
900
    typedef std::unordered_map<const state*, int,
			       state_ptr_hash, state_ptr_equal> hash_type;
901
902
    hash_type h;		///< Map of visited states.

903
    typedef std::list<const state*> state_list;
904
905
906
907
    typedef std::unordered_map<const state*, state_list,
			       state_ptr_hash, state_ptr_equal> f_map;
    typedef std::unordered_map<const void*, f_map,
			       ptr_hash<void> > contained_map;
908
909
    contained_map contained;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
910
    friend class numbered_state_heap_ssp_const_iterator;
911
    friend class couvreur99_check_shy_ssp;
912
    friend class couvreur99_check_shy_semi_ssp;
913
914

    mutable unsigned inclusions;
915
916
917
  };


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
918
  class numbered_state_heap_ssp_const_iterator :
919
920
921
    public numbered_state_heap_const_iterator
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
922
    numbered_state_heap_ssp_const_iterator
923
924
    (const numbered_state_heap_ssp_semi::hash_type& h)
      : numbered_state_heap_const_iterator(), h(h)
925
926
927
    {
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
928
    ~numbered_state_heap_ssp_const_iterator()
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
    {
    }

    virtual void
    first()
    {
      i = h.begin();
    }

    virtual void
    next()
    {
      ++i;
    }

    virtual bool
    done() const
    {
      return i == h.end();
    }

    virtual const state*
    get_state() const
    {
      return i->first;
    }

    virtual int
    get_index() const
    {
      return i->second;
    }

  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
963
964
    numbered_state_heap_ssp_semi::hash_type::const_iterator i;
    const numbered_state_heap_ssp_semi::hash_type& h;
965
966
  };

967

968
  numbered_state_heap_const_iterator*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
969
  numbered_state_heap_ssp_semi::iterator() const
970
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
971
    return new numbered_state_heap_ssp_const_iterator(h);
972
973
974
  }


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
975
  /// \brief Factory for numbered_state_heap_ssp_semi
976
977
  ///
  /// This class is a singleton.  Retrieve the instance using instance().
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
978
  class numbered_state_heap_ssp_factory_semi:
979
980
981
    public numbered_state_heap_factory
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
982
    virtual numbered_state_heap_ssp_semi*
983
984
    build() const
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
985
      return new numbered_state_heap_ssp_semi();
986
987
988
    }

    /// Get the unique instance of this class.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
989
    static const numbered_state_heap_ssp_factory_semi*
990
991
    instance()
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
992
      static numbered_state_heap_ssp_factory_semi f;
993
994
995
996
997
      return &f;
    }

  protected:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
998
    ~numbered_state_heap_ssp_factory_semi()
999
1000
1001
    {
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1002
    numbered_state_heap_ssp_factory_semi()
1003
1004
1005
1006
1007
    {
    }
  };


1008
  class couvreur99_check_shy_ssp : public couvreur99_check_shy
1009
1010
  {
  public:
1011
    couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion,
1012
1013
1014
			     bool double_inclusion,
			     bool reversed_double_inclusion,
			     bool no_decomp)
1015
      : couvreur99_check_shy(a,
1016
			     option_map(),
1017
1018
			     numbered_state_heap_ssp_factory_semi::instance()),
	inclusion_count_heap(0),
1019
	inclusion_count_stack(0),
1020
1021
	stack_inclusion(stack_inclusion),
	double_inclusion(double_inclusion),
1022
	reversed_double_inclusion(reversed_double_inclusion),
1023
	no_decomp(no_decomp)
1024
    {
1025
1026
      onepass_ = true;

1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
      stats["inclusion count heap"] =
	static_cast<spot::unsigned_statistics::unsigned_fun>
	(&couvreur99_check_shy_ssp::get_inclusion_count_heap);
      stats["inclusion count stack"] =
	static_cast<spot::unsigned_statistics::unsigned_fun>
	(&couvreur99_check_shy_ssp::get_inclusion_count_stack);
      stats["contained map size"] =
	static_cast<spot::unsigned_statistics::unsigned_fun>
	(&couvreur99_check_shy_ssp::get_contained_map_size);
    }
1037

1038
1039
1040
  private:
    unsigned inclusion_count_heap;
    unsigned inclusion_count_stack;
1041
    bool stack_inclusion;
1042
    bool double_inclusion;
1043
    bool reversed_double_inclusion;
1044
    bool no_decomp;
1045

1046
  protected:
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
    unsigned
    get_inclusion_count_heap() const
    {
      return inclusion_count_heap;
    };
    unsigned
    get_inclusion_count_stack() const
    {
      return inclusion_count_stack;
    };
1057
1058
1059
1060
    unsigned
    get_contained_map_size() const
    {
      return
1061
	down_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->contained.size();
1062
    }
1063
1064
1065
1066
1067

    // If a new state includes an older state, we may have to add new
    // children to the list of children of that older state.  We cannot
    // to this by sub-classing numbered_state_heap since TODO is not
    // available.  So we override find_state() instead.
1068
    virtual numbered_state_heap::state_index_p
1069
1070
    find_state(const state* s)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1071
      typedef numbered_state_heap_ssp_semi::hash_type hash_type;
1072
      hash_type& h = down_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->h;
1073
      typedef numbered_state_heap_ssp_semi::contained_map contained_map;
1074
      typedef numbered_state_heap_ssp_semi::f_map f_map;
1075
1076
      typedef numbered_state_heap_ssp_semi::state_list state_list;
      const contained_map& contained =
1077
	down_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->contained;
1078

1079
      const state_gspn_ssp* s_ = down_cast<const state_gspn_ssp*>(s);
1080
      const void* cont = container_(s_->left());
1081
      contained_map::const_iterator i = contained.find(cont);
1082

1083
      if (i != contained.end())
1084
	{
1085
1086
	  f_map::const_iterator k = i->second.find(s_->right());
	  if (k != i->second.end())
1087
	    {
1088
1089
1090
	      const state_list& l = k->second;
	      state_list::const_iterator j;

1091
	      // Make a first pass looking for identical states.
1092
	      for (j = l.begin(); j != l.end(); ++j)
1093
		{
1094
		  const state_gspn_ssp* old_state =
1095
		    down_cast<const state_gspn_ssp*>(*j);
1096
		  const state_gspn_ssp* new_state =
1097
		    down_cast<const state_gspn_ssp*>(s);
1098
1099
1100
		  assert(old_state);
		  assert(new_state);

1101
		  if (old_state->left() == new_state->left())
1102
1103
1104
1105
1106
1107
1108
		    goto found_match;
		}

	      // Now, check for inclusions.
	      for (j = l.begin(); j != l.end(); ++j)
		{
		  const state_gspn_ssp* old_state =
1109
		    down_cast<const state_gspn_ssp*>(*j);
1110
		  const state_gspn_ssp* new_state =
1111
		    down_cast<const state_gspn_ssp*>(s);
1112
1113
		  assert(old_state);
		  assert(new_state);
1114
1115

		  if (old_state->left() && new_state->left())
1116
		    {
1117
1118
1119
		      hash_type::const_iterator i = h.find(*j);
		      assert(i != h.end());
		      if (i->second == -1)
1120
			{
1121
1122
1123
1124
1125
1126
			  if (spot_inclusion(new_state->left(),
					     old_state->left()))
			    {
			      ++inclusion_count_heap;
			      break;
			    }
1127
			}
1128
		      else
1129
			{
1130
1131
			  if (stack_inclusion
			      && double_inclusion
1132
			      && !reversed_double_inclusion