tgbakvcomplement.cc 19.5 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Damien Lefortier's avatar
Damien Lefortier committed
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
Damien Lefortier's avatar
Damien Lefortier committed
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/>.
Damien Lefortier's avatar
Damien Lefortier committed
19

20
21
22
23
#include <vector>
#include <cassert>
#include <sstream>
#include "bdd.h"
24
#include "bddprint.hh"
25
#include "state.hh"
26
#include "tgbakvcomplement.hh"
27
28
29
30
31
#include "misc/hash.hh"
#include "tgbaalgos/bfssteps.hh"
#include "misc/hashfunc.hh"
#include "ltlast/formula.hh"
#include "ltlast/constant.hh"
32
#include "tgbaalgos/stats.hh"
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

namespace spot
{
  namespace
  {
    ////////////////////////////////////////
    // rank

    /// \brief A rank structure, one of the main structure of the algorithm.
    ///
    /// A rank has a number (\a rank) that refers to the depth in the DAG of
    /// the current word. When the rank is odd, a \a condition is associated
    /// to this rank.
    struct rank_t
    {
      mutable unsigned rank;
      mutable bdd_ordered condition;

      bool operator<(const rank_t& other) const
      {
        return rank < other.rank ||
          condition.order() < other.condition.order();
      }

      unsigned get_rank() const
      {
        return rank;
      }

      bdd_ordered get_condition() const
      {
        return condition;
      }

      size_t hash() const
      {
        size_t hash = wang32_hash(rank);
        if (rank & 1)
          hash ^= wang32_hash(condition.order());
        return hash;
      }

75
      std::string format(const tgba* a) const
76
77
78
79
80
      {
        std::ostringstream ss;
        ss << "{rank: " << rank;
        if (rank & 1)
        {
81
82
83
          ss << ", bdd: {" << condition.order() << ", "
             << bdd_format_accset(a->get_dict(), condition.get_bdd())
             << "} ";
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
        }
        ss << "}";
        return ss.str();
      }
    };

    // typedefs.
    typedef Sgi::hash_map<shared_state, rank_t,
                          state_shared_ptr_hash,
                          state_shared_ptr_equal> state_rank_map;
    typedef Sgi::hash_set<shared_state,
                          state_shared_ptr_hash,
                          state_shared_ptr_equal> state_set;

    ////////////////////////////////////////
99
    // state_kv_complement
100

101
    /// States used by spot::tgba_kv_complement.
102
103
104
    /// A state has a map of states associated to ranks, and a set
    /// of filtered states.
    /// \ingroup tgba_representation
105
    class state_kv_complement : public state
106
107
    {
    public:
108
109
110
      state_kv_complement();
      state_kv_complement(state_rank_map state_map, state_set state_filter);
      virtual ~state_kv_complement() {}
111
112
113

      virtual int compare(const state* other) const;
      virtual size_t hash() const;
114
      virtual state_kv_complement* clone() const;
115
116
117
118
119
120
121
122
123
124

      void add(shared_state state, const rank_t& rank);
      const state_rank_map& get_state_map() const;
      const state_set& get_filter_set() const;
      bool accepting() const;
    private:
      state_rank_map state_map_;
      state_set state_filter_;
    };

125
    state_kv_complement::state_kv_complement()
126
127
128
    {
    }

129
    state_kv_complement::state_kv_complement(state_rank_map state_map,
130
131
132
133
134
135
                                       state_set state_filter)
      : state_map_(state_map), state_filter_(state_filter)
    {
    }

    int
136
    state_kv_complement::compare(const state* o) const
137
    {
138
      const state_kv_complement* other =
139
	down_cast<const state_kv_complement*>(o);
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

      if (other == 0)
        return 1;

      if (state_map_.size() < other->state_map_.size())
        return -1;
      else if (state_map_.size() > other->state_map_.size())
        return 1;

      if (state_filter_.size() < other->state_filter_.size())
        return -1;
      else if (state_filter_.size() > other->state_filter_.size())
        return 1;

      {
        state_rank_map::const_iterator i = state_map_.begin();
        state_rank_map::const_iterator j = other->state_map_.begin();
        while (i != state_map_.end() && j != other->state_map_.end())
        {
          int result = i->first->compare(j->first.get());
          if (result != 0)
            return result;
          if (i->second < j->second)
            return -1;
          if (j->second < i->second)
            return 1;
          ++i;
          ++j;
        }
      }

      {
        state_set::const_iterator i = state_filter_.begin();
        state_set::const_iterator j = other->state_filter_.begin();
        while (i != state_filter_.end() && j != other->state_filter_.end())
        {
          int result = (*i)->compare(j->get());
          if (result != 0)
            return result;
          ++i;
          ++j;
        }
      }

      return 0;
    }

    size_t
188
    state_kv_complement::hash() const
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
    {
      size_t hash = 0;

      {
        state_rank_map::const_iterator i = state_map_.begin();
        while (i != state_map_.end())
        {
          hash ^= i->first->hash();
          hash ^= i->second.hash();
          ++i;
        }
      }

      {
        state_set::const_iterator i = state_filter_.begin();
        while (i != state_filter_.end())
        {
          hash ^= (*i)->hash();
          ++i;
        }
      }

      return hash;
    }

214
215
    state_kv_complement*
    state_kv_complement::clone() const
216
    {
217
      return new state_kv_complement(*this);
218
219
220
    }

    void
221
    state_kv_complement::add(shared_state state,
222
223
224
225
226
227
                          const rank_t& rank)
    {
      state_map_[state] = rank;
    }

    const state_rank_map&
228
    state_kv_complement::get_state_map() const
229
230
231
232
233
    {
      return state_map_;
    }

    const state_set&
234
    state_kv_complement::get_filter_set() const
235
236
237
238
239
    {
      return state_filter_;
    }

    bool
240
    state_kv_complement::accepting() const
241
242
243
244
    {
      return state_filter_.empty();
    }

245
    /// Successor iterators used by spot::tgba_kv_complement.
246
247
248
249
250
251
    /// \ingroup tgba_representation
    ///
    /// Since the algorithm works on-the-fly, the key components of the
    /// algorithm are implemented in this class.
    ///
    ///
252
    class tgba_kv_complement_succ_iterator: public tgba_succ_iterator
253
254
255
256
    {
    public:
      typedef std::list<bdd> bdd_list_t;

257
258
259
260
261
      tgba_kv_complement_succ_iterator(const tgba_sgba_proxy* automaton,
				       bdd the_acceptance_cond,
				       const acc_list_t& acc_list,
				       const state_kv_complement* origin);
      virtual ~tgba_kv_complement_succ_iterator() {};
262
263
264
265

      virtual void first();
      virtual void next();
      virtual bool done() const;
266
      virtual state_kv_complement* current_state() const;
267
268
269
270
271
272
273
274
275
276
277
278
279
280
      virtual bdd current_condition() const;
      virtual bdd current_acceptance_conditions() const;
    private:
      /// \brief Create the highest rank of \a origin_ as origin and
      /// \a condition as successor condition.
      void successor_highest_rank(bdd condition);
      void get_atomics(std::set<int>& list, bdd c);
      void get_conj_list();
      bool is_valid_rank() const;
      bool next_valid_rank();

      const tgba_sgba_proxy* automaton_;
      bdd the_acceptance_cond_;
      const acc_list_t& acc_list_;
281
      const state_kv_complement* origin_;
282
283
284
285
286
287
288
      bdd_list_t condition_list_;
      bdd_list_t::const_iterator current_condition_;
      state_rank_map highest_current_ranks_;
      state_rank_map current_ranks_;
      state_set highest_state_set_;
    };

289
290
291
292
293
    tgba_kv_complement_succ_iterator::
    tgba_kv_complement_succ_iterator(const tgba_sgba_proxy* automaton,
				     bdd the_acceptance_cond,
				     const acc_list_t& acc_list,
				     const state_kv_complement* origin)
294
295
296
297
298
299
300
301
      : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
        acc_list_(acc_list), origin_(origin)
    {
      get_conj_list();
    }

    /// Insert in \a list atomic properties of the formula \a c.
    void
302
    tgba_kv_complement_succ_iterator::get_atomics(std::set<int>& list, bdd c)
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
    {
      bdd current = bdd_satone(c);
      while (current != bddtrue && current != bddfalse)
      {
        list.insert(bdd_var(current));
        bdd high = bdd_high(current);
        if (high == bddfalse)
          current = bdd_low(current);
        else
          current = high;
      }
    }

    /// Create the conjunction of all the atomic properties from
    /// the successors of the current state.
    void
319
    tgba_kv_complement_succ_iterator::get_conj_list()
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
    {
      std::set<int> atomics;
      condition_list_.clear();
      state_rank_map sr_map = origin_->get_state_map();

      // Retrieve all the atomics in acceptance conditions.
      for (state_rank_map::const_iterator i = sr_map.begin();
           i != sr_map.end();
           ++i)
      {
        tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
        for (iterator->first(); !iterator->done(); iterator->next())
        {
          bdd c = iterator->current_condition();
          get_atomics(atomics, c);
        }
        delete iterator;
      }

      // Compute the conjunction of all those atomic properties.
      unsigned atomics_size = atomics.size();

      assert(atomics_size < 32);
      for (unsigned i = 1; i <= static_cast<unsigned>(1 << atomics_size); ++i)
      {
        bdd result = bddtrue;
        unsigned position = 1;
        for (std::set<int>::const_iterator a_it = atomics.begin();
             a_it != atomics.end();
             ++a_it, position <<= 1)
        {
          bdd this_atomic;
          if (position & i)
            this_atomic = bdd_ithvar(*a_it);
          else
            this_atomic = bdd_nithvar(*a_it);
          result = bdd_apply(result, this_atomic, bddop_and);
        }
        condition_list_.push_back(result);
      }
    }

    /// Check whether \a current_ranks_ is a valid rank.
    /// For each odd rank, its condition associated must not
    /// be present in its tracked state.
    bool
366
    tgba_kv_complement_succ_iterator::is_valid_rank() const
367
368
369
370
371
372
    {
      for (state_rank_map::const_iterator i = current_ranks_.begin();
           i != current_ranks_.end();
           ++i)
      {
        if (i->second.rank & 1)
373
	  {
374
375
376
          if ((automaton_->state_acceptance_conditions(i->first.get()) &
               i->second.condition.get_bdd()) != bddfalse)
            return false;
377
	  }
378
      }
379

380
381
382
383
384
385
386
387
388
389
      return true;
    }

    /// \brief Decrease \a current_ranks_ and produces a valid rank.
    /// \a current_ranks_ is a map of states to a rank.
    /// A rank for a state is valid if it is inferior than the rank of its
    /// predecessor.
    /// When the rank is odd, its has an acceptance condition associated that
    /// must not be in its associated state.
    /// \return false if there is not valid rank as successor.
390
    bool tgba_kv_complement_succ_iterator::next_valid_rank()
391
392
    {
      state_rank_map::const_iterator i;
393
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
      do
	{
	  for (i = current_ranks_.begin(); i != current_ranks_.end(); ++i)
	    {
	      if (i->second.rank != 0)
		{
		  if (i->second.rank & 1)
		    {
		      if (i->second.condition.order() == 0)
			--i->second.rank;
		      else
			i->second.condition =
			  acc_list_[i->second.condition.order() - 1];
		    }
		  else
		    {
		      --i->second.rank;
		      i->second.condition = acc_list_[acc_list_.size() - 1];
		    }
		  break;
		}
	      else
		{
		  current_ranks_[i->first] = highest_current_ranks_[i->first];
		}
	    }
	}
420
421
422
423
424
425
426
427
      while ((i != current_ranks_.end()) && !is_valid_rank());

      return i != current_ranks_.end();
    }

    /// \brief Create the highest rank of \a origin_ as origin and
    /// \a condition as successor condition.
    void
428
    tgba_kv_complement_succ_iterator::successor_highest_rank(bdd condition)
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
    {
      // Highest rank for bdd.
      state_rank_map sr_map = origin_->get_state_map();
      highest_current_ranks_.clear();

      for (state_rank_map::const_iterator i = sr_map.begin();
           i != sr_map.end();
           ++i)
      {
        tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
        for (iterator->first(); !iterator->done(); iterator->next())
        {
          bdd c = iterator->current_condition();
          if ((c & condition) != bddfalse)
          {
444
            shared_state s(iterator->current_state(), shared_state_deleter);
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
            if (highest_current_ranks_.find(s) != highest_current_ranks_.end())
            {
              if (i->second < highest_current_ranks_[s])
                highest_current_ranks_[s] = i->second;
            }
            else
              highest_current_ranks_[s] = i->second;
          }
        }
        delete iterator;
      }

      // Highest $O$ set of the algorithm.
      state_set s_set = origin_->get_filter_set();
      highest_state_set_.clear();

      for (state_set::const_iterator i = s_set.begin();
           i != s_set.end();
           ++i)
      {
        tgba_succ_iterator* iterator = automaton_->succ_iter(i->get());
        for (iterator->first(); !iterator->done(); iterator->next())
        {
          bdd c = iterator->current_condition();
          if ((c & condition) != bddfalse)
          {
471
            shared_state s(iterator->current_state(), shared_state_deleter);
472
473
474
475
476
477
478
479
480
481
            highest_state_set_.insert(s);
          }
        }
        delete iterator;
      }

      current_ranks_ = highest_current_ranks_;
    }

    void
482
    tgba_kv_complement_succ_iterator::first()
483
484
485
486
487
488
489
490
491
492
493
494
    {
      current_condition_ = condition_list_.begin();
      if (done())
        return;

      successor_highest_rank(*current_condition_);

      if (!is_valid_rank())
        next_valid_rank();
    }

    void
495
    tgba_kv_complement_succ_iterator::next()
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
    {
      if (done())
        return;

      if (!next_valid_rank())
      {
        ++current_condition_;
        if (!done())
        {
          successor_highest_rank(*current_condition_);
          if (!is_valid_rank())
            next_valid_rank();
        }
      }
    }

    bool
513
    tgba_kv_complement_succ_iterator::done() const
514
515
516
517
    {
      return (current_condition_ == condition_list_.end());
    }

518
519
    state_kv_complement*
    tgba_kv_complement_succ_iterator::current_state() const
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
    {
      if (done())
        return 0;

      // If the filter set is empty, all the states of the map
      // that are associated to an even rank create the new filter set.
      state_set filter;
      if (origin_->get_filter_set().empty())
      {
        for (state_rank_map::const_iterator i = current_ranks_.begin();
             i != current_ranks_.end();
             ++i)
          if (!(i->second.rank & 1))
            filter.insert(i->first);
      }
      else
      {
        // It the filter set is non-empty, we delete from this set states
        // that are now associated to an odd rank.
        for (state_set::const_iterator i = highest_state_set_.begin();
             i != highest_state_set_.end();
             ++i)
        {
          state_rank_map::const_iterator s(current_ranks_.find(*i));
          assert(s != current_ranks_.end());

          if (!(s->second.get_rank() & 1))
            filter.insert(*i);
        }
      }

551
      return new state_kv_complement(current_ranks_, filter);
552
553
554
    }

    bdd
555
    tgba_kv_complement_succ_iterator::current_condition() const
556
557
558
559
560
561
562
    {
      if (done())
        return bddfalse;
      return *current_condition_;
    }

    bdd
563
    tgba_kv_complement_succ_iterator::current_acceptance_conditions() const
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
    {
      if (done())
        return bddfalse;

      // This algorithm doesn't generalized acceptance conditions.
      if (origin_->accepting())
        return the_acceptance_cond_;
      else
        return bddfalse;
    }

  } // end namespace anonymous.

  /// Retrieve all the atomic acceptance conditions of the automaton.
  /// They are inserted into \a acc_list_.
  void
580
  tgba_kv_complement::get_acc_list()
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
  {
    bdd c = automaton_->all_acceptance_conditions();
    bdd current = bdd_satone(c);
    unsigned i = 0;
    while (current != bddtrue && current != bddfalse)
    {
      acc_list_.push_back(bdd_ordered(bdd_var(current), i));
      ++i;
      bdd high = bdd_high(current);
      if (high == bddfalse)
        current = bdd_low(current);
      else
        current = high;
    }
  }

597
  tgba_kv_complement::tgba_kv_complement(const tgba* a)
598
599
600
601
602
603
604
    : automaton_(new tgba_sgba_proxy(a))
  {
    get_dict()->register_all_variables_of(automaton_, this);
    int v = get_dict()
      ->register_acceptance_variable(ltl::constant::true_instance(), this);
    the_acceptance_cond_ = bdd_ithvar(v);
    {
605
606
      spot::tgba_statistics a_size =  spot::stats_reachable(automaton_);
      nb_states_ = a_size.states;
607
608
609
610
    }
    get_acc_list();
  }

611
  tgba_kv_complement::~tgba_kv_complement()
612
613
614
615
616
617
  {
    get_dict()->unregister_all_my_variables(this);
    delete automaton_;
  }

  state*
618
  tgba_kv_complement::get_init_state() const
619
  {
620
    state_kv_complement* init = new state_kv_complement();
621
    rank_t r = {2 * nb_states_, bdd_ordered()};
622
623
    init->add(shared_state(automaton_->get_init_state(), shared_state_deleter),
	      r);
624
625
626
627
    return init;
  }

  tgba_succ_iterator*
628
  tgba_kv_complement::succ_iter(const state* local_state,
629
630
631
                             const state*,
                             const tgba*) const
  {
632
    const state_kv_complement* state =
633
      down_cast<const state_kv_complement*>(local_state);
634
635
    assert(state);

636
    return new tgba_kv_complement_succ_iterator(automaton_,
637
638
639
640
641
                                             the_acceptance_cond_,
                                             acc_list_, state);
  }

  bdd_dict*
642
  tgba_kv_complement::get_dict() const
643
644
645
646
647
  {
    return automaton_->get_dict();
  }

  std::string
648
  tgba_kv_complement::format_state(const state* state) const
649
  {
650
    const state_kv_complement* s =
651
      down_cast<const state_kv_complement*>(state);
652
653
654
655
656
657
658
659
660
661
662
663
    assert(s);
    std::ostringstream ss;
    ss << "{ set: {" << std::endl;

    const state_rank_map& state_map = s->get_state_map();
    const state_set& state_filter = s->get_filter_set();

    for (state_rank_map::const_iterator i = state_map.begin();
         i != state_map.end();
         ++i)
    {
      ss << "  {" << automaton_->format_state(i->first.get())
664
         << ", " << i->second.format(this) << "}" << std::endl;
665
666
667
668
669
670
671
672
673
674
675
676
    }
    ss << "} odd-less: {";

    for (state_set::const_iterator i = state_filter.begin();
         i != state_filter.end();
         ++i)
      ss << "  " << automaton_->format_state(i->get()) << std::endl;
    ss << "} }";
    return ss.str();
  }

  bdd
677
  tgba_kv_complement::all_acceptance_conditions() const
678
679
680
681
682
  {
    return the_acceptance_cond_;
  }

  bdd
683
  tgba_kv_complement::neg_acceptance_conditions() const
684
685
686
687
688
  {
    return !the_acceptance_cond_;
  }

  bdd
689
  tgba_kv_complement::compute_support_conditions(const state* state) const
690
691
692
693
694
695
696
697
698
699
  {
    tgba_succ_iterator* i = succ_iter(state);
    bdd result = bddtrue;
    for (i->first(); !i->done(); i->next())
      result |= i->current_condition();
    delete i;
    return result;
  }

  bdd
700
  tgba_kv_complement::compute_support_variables(const state* state) const
701
702
703
704
705
706
707
708
709
710
  {
    tgba_succ_iterator* i = succ_iter(state);
    bdd result = bddtrue;
    for (i->first(); !i->done(); i->next())
      result &= bdd_support(i->current_condition());
    delete i;
    return result;
  }

} // end namespace spot.