ssp.cc 22.3 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
// dpartement Systmes Rpartis Coopratifs (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
#include <cstring>
#include <map>
#include <cassert>
#include <gspnlib.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
26
#include "ssp.hh"
27
28
#include "misc/bddlt.hh"
#include <bdd.h>
29
30
#include "tgbaalgos/gtec/explscc.hh"
#include "tgbaalgos/gtec/nsheap.hh"
31
32
33
34

namespace spot
{

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

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

      delete[] t;
      return tmp;
    }
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
51
  // state_gspn_ssp
52
53
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
54
  class state_gspn_ssp: public state
55
56
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
57
    state_gspn_ssp(State left, const state* right)
58
59
60
61
62
      : left_(left), right_(right)
    {
    }

    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
    ~state_gspn_ssp()
64
65
66
67
68
69
70
    {
      delete right_;
    }

    virtual int
    compare(const state* other) const
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
71
      const state_gspn_ssp* o = dynamic_cast<const state_gspn_ssp*>(other);
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
      assert(o);
      int res = (reinterpret_cast<char*>(o->left())
		 - reinterpret_cast<char*>(left()));
      if (res != 0)
	return res;
      return right_->compare(o->right());
    }

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
    virtual state_gspn_ssp* clone() const
88
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
89
      return new state_gspn_ssp(left(), right()->clone());
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
    }

    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
107
  }; // state_gspn_ssp
108

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
  // tgba_gspn_ssp_private_
110
111
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
112
  struct tgba_gspn_ssp_private_
113
114
115
116
117
118
119
120
121
122
123
124
  {
    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;

125
126
127
    tgba_gspn_ssp_private_(bdd_dict* dict,
			   const ltl::declarative_environment& env,
			   const tgba* operand)
128
129
130
      : refs(1), dict(dict), all_props(0),
	operand(operand)
    {
131
      const ltl::declarative_environment::prop_map& p = env.get_prop_map();
132
133
134
135
136

      try
	{
	  AtomicProp max_prop = 0;

137
138
	  for (ltl::declarative_environment::prop_map::const_iterator i
		 = p.begin(); i != p.end(); ++i)
139
140
141
142
143
	    {
	      int var = dict->register_proposition(i->second, this);
	      AtomicProp index;
	      int err = prop_index(i->first.c_str(), &index);
	      if (err)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
144
		throw gspn_exeption("prop_index(" + i->first + ")", err);
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

	      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;
	}
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
162
    tgba_gspn_ssp_private_::~tgba_gspn_ssp_private_()
163
164
165
166
167
168
169
170
    {
      dict->unregister_all_my_variables(this);
      if (all_props)
	delete[] all_props;
    }
  };


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
171
  // tgba_succ_iterator_gspn_ssp
172
173
  //////////////////////////////////////////////////////////////////////

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

    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
196
    ~tgba_succ_iterator_gspn_ssp()
197
198
    {

199
      for (size_t i = 0; i < size_states_; i++)
200
      	delete state_array_[i];
201

202
203
      delete[] bdd_array_;
      free(state_array_);
204

205
206
207
208
209
210
      if (props_)
	{
	  for (int i = 0; i < size_prop_; i++)
	    free(props_[i].arc);
	  free(props_);
	}
211

212
213
      if (size_succ_ != 0)
	succ_free(successors_);
214

215
216
217
218
219
    }

    virtual void
    first()
    {
220
221
      if (!successors_)
	return;
222
      current_succ_=0;
223
224
225
226
227
    }

    virtual void
    next()
    {
228
      current_succ_++;
229
230
231
232
233
    }

    virtual bool
    done() const
    {
234
      return current_succ_ + 1 > size_succ_;
235
236
237
238
239
    }

    virtual state*
    current_state() const
    {
240
      return
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
241
	new state_gspn_ssp(successors_[current_succ_].succ_,
242
243
			     (state_array_[successors_[current_succ_]
					   .arc->curr_state])->clone());
244
245
246
247
248
249
250
251
252
    }

    virtual bdd
    current_condition() const
    {
      return bddtrue;
    }

    virtual bdd
253
    current_acceptance_conditions() const
254
255
256
    {
      // There is no acceptance conditions in GSPN systems, so we just
      // return those from OPERAND_.
257
258
259
260
      // return operand_->current_acceptance_conditions();
      // bdd * ac=(bdd *)successors_[current_succ_].arc->curr_acc_conds;
      //return (*ac);
      return bdd_array_[successors_[current_succ_].arc->curr_acc_conds];
261
262
    }
  private:
263

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

    bdd * bdd_array_;
    state** state_array_;
    size_t size_states_;
    Props_* props_;
    int size_prop_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
275
  }; // tgba_succ_iterator_gspn_ssp
276
277


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
278
  // tgba_gspn_ssp
279
280
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
281
  class tgba_gspn_ssp: public tgba
282
283
  {
  public:
284
285
    tgba_gspn_ssp(bdd_dict* dict, const ltl::declarative_environment& env,
		  const tgba* operand);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
286
287
288
    tgba_gspn_ssp(const tgba_gspn_ssp& other);
    tgba_gspn_ssp& operator=(const tgba_gspn_ssp& other);
    virtual ~tgba_gspn_ssp();
289
290
291
292
293
294
295
296
297
298
299
300
301
302
    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
303
    tgba_gspn_ssp_private_* data_;
304
  };
305

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

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

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

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

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

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

    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;

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

    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;
	    size_bdd++;

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

393
	    while (all_conds_ != bddfalse)
394
395
396
397
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
	      {
		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
427
		    tgba_gspn_ssp_private_::prop_map::iterator k
428
429
430
431
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;
	  }
      }
     Succ_* succ_tgba_ = 0;
     size_t size_tgba_ = 0;
     int j, conj;

445
     succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_);
446
447
448

     for (j = 0; j < nb_arc_props; j++)
       {
449
	 for (conj = 0; conj < props_[j].nb_conj; conj++)
450
451
452
453
454
	   free(props_[j].prop[conj]);
	 free(props_[j].prop);
       }

     delete i;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
455
     return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_,
456
457
458
					    bdd_array, state_array,
					    size_states, props_,
					    nb_arc_props);
459
460
461
  }

  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
462
  tgba_gspn_ssp::compute_support_conditions(const spot::state* state) const
463
464
465
466
467
468
  {
    (void) state;
    return bddtrue;
  }

  bdd
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
469
  tgba_gspn_ssp::compute_support_variables(const spot::state* state) const
470
471
472
473
474
475
  {
    (void) state;
    return bddtrue;
  }

  bdd_dict*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
476
  tgba_gspn_ssp::get_dict() const
477
478
479
480
481
  {
    return data_->dict;
  }

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

503
    std::string res(str);
504
    free(str);
505
    return res + " * " + data_->operand->format_state(s->right());
506
507
  }

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
534
  // gspn_ssp_interface
535
536
  //////////////////////////////////////////////////////////////////////

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
537
  gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv,
538
					 bdd_dict* dict,
539
540
					 const
					 ltl::declarative_environment& env,
541
					 bool inclusion)
542
543
    : dict_(dict), env_(env)
  {
544
545
546
    if (inclusion)
      inclusion_version();

547
548
549
550
551
    int res = initialize(argc, argv);
    if (res)
      throw gspn_exeption("initialize()", res);
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
552
  gspn_ssp_interface::~gspn_ssp_interface()
553
554
555
556
557
558
559
  {
    int res = finalize();
    if (res)
      throw gspn_exeption("finalize()", res);
  }

  tgba*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
560
  gspn_ssp_interface::automaton(const tgba* operand) const
561
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
562
    return new tgba_gspn_ssp(dict_, env_, operand);
563
564
  }

565
566
567

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
568
  class connected_component_ssp: public explicit_connected_component
569
570
571
  {
  public:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
572
    ~connected_component_ssp()
573
574
575
576
577
578
579
580
581
582
    {
    }

    virtual const state*
    has_state(const state* s) const
    {
      set_type::iterator i;

      for (i = states.begin(); i !=states.end(); i++)
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
583
584
	  const state_gspn_ssp* old_state = (const state_gspn_ssp*)(*i);
	  const state_gspn_ssp* new_state = (const state_gspn_ssp*)(s);
585
586
587
588
589

	  if ((old_state->right())->compare(new_state->right()) == 0
	      && old_state->left()
	      && new_state->left())
	    if (spot_inclusion(new_state->left(), old_state->left()))
590
591
592
593
594
	      {
		if (*i != s)
		  delete s;
		return *i;
	      }
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
	}
      return 0;
    }

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

  protected:
    typedef Sgi::hash_set<const state*,
			  state_ptr_hash, state_ptr_equal> set_type;
    set_type states;
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
611
  class connected_component_ssp_factory :
612
613
614
    public explicit_connected_component_factory
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
615
    virtual connected_component_ssp*
616
617
    build() const
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
618
      return new connected_component_ssp();
619
620
621
    }

    /// Get the unique instance of this class.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
622
    static const connected_component_ssp_factory*
623
624
    instance()
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
625
      static connected_component_ssp_factory f;
626
627
628
629
630
      return &f;
    }

  protected:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
631
    ~connected_component_ssp_factory()
632
633
634
    {
    }
    /// Construction is forbiden.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
635
    connected_component_ssp_factory()
636
637
638
639
640
641
642
    {
    }
  };

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


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
643
  class numbered_state_heap_ssp_semi : public numbered_state_heap
644
645
646
  {
  public:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
647
    ~numbered_state_heap_ssp_semi()
648
649
650
651
652
653
654
655
656
657
658
659
    {
      // 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;
	  delete s;
	}
    }

660
    virtual numbered_state_heap::state_index
661
662
    find(const state* s) const
    {
663
664
      state_index res;

665
666
667
      hash_type::const_iterator i;
      for (i = h.begin(); i != h.end(); ++i)
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
668
669
670
671
	  const state_gspn_ssp* old_state =
	    dynamic_cast<const state_gspn_ssp*>(i->first);
	  const state_gspn_ssp* new_state =
	    dynamic_cast<const state_gspn_ssp*>(s);
672
673
674
675
676
677
678
679
680
681
	  assert(old_state);
	  assert(new_state);

	  if ((old_state->right())->compare(new_state->right()) == 0)
	    {
	      if (old_state->left() == new_state->left())
		break;

	      if (old_state->left()
		  && new_state->left()
682
		  && spot_inclusion(new_state->left(), old_state->left()))
683
684
685
686
		break;
	    }
	}

687
688
689
690
691
692
693
694
695
      if (i == h.end())
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
	  res.first = i->first;
	  res.second = i->second;
696

697
698
699
700
	  if (s != i->first)
	    delete s;
	}
      return res;
701
702
    }

703
704
    virtual numbered_state_heap::state_index_p
    find(const state* s)
705
    {
706
      state_index_p res;
707

708
      hash_type::iterator i;
709
710
      for (i = h.begin(); i != h.end(); ++i)
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
711
712
713
714
	  const state_gspn_ssp* old_state =
	    dynamic_cast<const state_gspn_ssp*>(i->first);
	  const state_gspn_ssp* new_state =
	    dynamic_cast<const state_gspn_ssp*>(s);
715
716
717
718
719
720
721
722
723
724
	  assert(old_state);
	  assert(new_state);

	  if ((old_state->right())->compare(new_state->right()) == 0)
	    {
	      if (old_state->left() == new_state->left())
		break;

	      if (old_state->left()
		  && new_state->left()
725
		  && spot_inclusion(new_state->left(), old_state->left()))
726
727
728
		break;
	    }
	}
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743

      if (i == h.end())
	{
	  res.first = 0;
	  res.second = 0;
	}
      else
	{
	  res.first = i->first;
	  res.second = &i->second;

	  if (s != i->first)
	    delete s;
	}
      return res;
744
745
    }

746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
    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)
	    delete s;
	}
      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)
	    delete s;
	}
      return res;
    }

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

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

    virtual numbered_state_heap_const_iterator* iterator() const;

802
803
804
805
806
  protected:
    typedef Sgi::hash_map<const state*, int,
			  state_ptr_hash, state_ptr_equal> hash_type;
    hash_type h;		///< Map of visited states.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
807
808
    friend class numbered_state_heap_ssp_const_iterator;
    friend class emptiness_check_shy_ssp;
809
810
811
  };


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
812
  class numbered_state_heap_ssp_const_iterator :
813
814
815
    public numbered_state_heap_const_iterator
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
816
817
    numbered_state_heap_ssp_const_iterator
      (const numbered_state_heap_ssp_semi::hash_type& h)
818
819
820
821
	: numbered_state_heap_const_iterator(), h(h)
    {
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
822
    ~numbered_state_heap_ssp_const_iterator()
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
    {
    }

    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
857
858
    numbered_state_heap_ssp_semi::hash_type::const_iterator i;
    const numbered_state_heap_ssp_semi::hash_type& h;
859
860
  };

861

862
  numbered_state_heap_const_iterator*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
863
  numbered_state_heap_ssp_semi::iterator() const
864
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
865
    return new numbered_state_heap_ssp_const_iterator(h);
866
867
868
  }


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
869
  /// \brief Factory for numbered_state_heap_ssp_semi
870
871
  ///
  /// This class is a singleton.  Retrieve the instance using instance().
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
872
  class numbered_state_heap_ssp_factory_semi:
873
874
875
    public numbered_state_heap_factory
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
876
    virtual numbered_state_heap_ssp_semi*
877
878
    build() const
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
879
      return new numbered_state_heap_ssp_semi();
880
881
882
    }

    /// Get the unique instance of this class.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
883
    static const numbered_state_heap_ssp_factory_semi*
884
885
    instance()
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
886
      static numbered_state_heap_ssp_factory_semi f;
887
888
889
890
891
      return &f;
    }

  protected:
    virtual
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
892
    ~numbered_state_heap_ssp_factory_semi()
893
894
895
    {
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
896
    numbered_state_heap_ssp_factory_semi()
897
898
899
900
901
    {
    }
  };


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
  class emptiness_check_shy_ssp : public emptiness_check_shy
903
904
  {
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905
    emptiness_check_shy_ssp(const tgba* a)
906
      : emptiness_check_shy(a,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
907
			    numbered_state_heap_ssp_factory_semi::instance())
908
909
910
911
912
913
914
    {
    }

  protected:
    virtual int*
    find_state(const state* s)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
915
916
      typedef numbered_state_heap_ssp_semi::hash_type hash_type;
      hash_type& h = dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->h;
917
918
919
920

      hash_type::iterator i;
      for (i = h.begin(); i != h.end(); ++i)
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
921
922
923
924
	  const state_gspn_ssp* old_state =
	    dynamic_cast<const state_gspn_ssp*>(i->first);
	  const state_gspn_ssp* new_state =
	    dynamic_cast<const state_gspn_ssp*>(s);
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
	  assert(old_state);
	  assert(new_state);

	  if ((old_state->right())->compare(new_state->right()) == 0)
	    {
	      if (old_state->left() == new_state->left())
		break;

	      if (old_state->left() && new_state->left())
		{
		  if (i->second == -1)
		    {
		      if (spot_inclusion(new_state->left(), old_state->left()))
			break;
		    }
		  else
		    {
		      if (spot_inclusion(old_state->left(), new_state->left()))
			{
944
			  State* succ_tgba_ = 0;
945
946
947
948
949
950
951
952
			  size_t size_tgba_ = 0;
			  succ_queue& queue = todo.top().second;

			  Diff_succ(old_state->left(), new_state->left(),
				    &succ_tgba_, &size_tgba_);

			  for (size_t i = 0; i < size_tgba_; i++)
			    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
953
954
			      state_gspn_ssp* s =
				new state_gspn_ssp
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
				  (succ_tgba_[i],
				   old_state->right()->clone());
			      queue.push_back(successor(queue.begin()->acc, s));
			    }
			  if (size_tgba_ != 0)
			    diff_succ_free(succ_tgba_);
			  break;
			}
		    }
		}
	    }
	}
      if (i == h.end())
	return 0;
      return &i->second;
    }
  };



975
  emptiness_check*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
976
  emptiness_check_ssp_semi(const tgba* ssp_automata)
977
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
978
    assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
979
    return
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
980
981
      new emptiness_check(ssp_automata,
			  numbered_state_heap_ssp_factory_semi::instance());
982
983
984
  }

  emptiness_check*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
985
  emptiness_check_ssp_shy_semi(const tgba* ssp_automata)
986
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
987
    assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
988
989
    return
      new emptiness_check_shy
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
990
991
        (ssp_automata,
	 numbered_state_heap_ssp_factory_semi::instance());
992
993
  }

994
  emptiness_check*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
995
  emptiness_check_ssp_shy(const tgba* ssp_automata)
996
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
997
998
    assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
    return new emptiness_check_shy_ssp(ssp_automata);
999
1000
  }

1001
  counter_example*
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1002
  counter_example_ssp(const emptiness_check_status* status)
1003
1004
  {
    return new counter_example(status,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1005
			       connected_component_ssp_factory::instance());
1006
  }
1007
}