sabacomplementtgba.cc 13.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
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
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/>.
19
20
21
22
23

#include <vector>
#include <cassert>
#include <sstream>
#include "bdd.h"
24
#include "tgba/bddprint.hh"
25
#include "tgba/tgba.hh"
26
#include "misc/hash.hh"
27
#include "misc/bddlt.hh"
28
#include "tgbaalgos/degen.hh"
29
30
31
32
#include "tgbaalgos/bfssteps.hh"
#include "misc/hashfunc.hh"
#include "ltlast/formula.hh"
#include "ltlast/constant.hh"
33
#include "priv/countstates.hh"
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153

#include "sabacomplementtgba.hh"
#include "explicitstateconjunction.hh"

namespace spot
{
  namespace
  {

    // typedefs.
    typedef int rank_t;

    ////////////////////////////////////////
    // saba_state_complement_tgba

    /// States used by spot::saba_complement_tgba.
    /// A state gather a spot::state* and a rank.
    /// \ingroup saba_representation
    class saba_state_complement_tgba : public saba_state
    {
    public:
      saba_state_complement_tgba();
      saba_state_complement_tgba(const saba_state_complement_tgba* state_taa);
      saba_state_complement_tgba(shared_state state, rank_t rank,
                                 bdd condition);
      virtual ~saba_state_complement_tgba() {}

      virtual int compare(const saba_state* other) const;
      virtual size_t hash() const;
      virtual saba_state_complement_tgba* clone() const;

      virtual bdd acceptance_conditions() const;
      const state* get_state() const;
      rank_t get_rank() const;
    private:
      shared_state state_;
      rank_t rank_;
      bdd condition_;
    };

    saba_state_complement_tgba::saba_state_complement_tgba(shared_state state,
                                                           rank_t rank,
                                                           bdd condition)
      : state_(state), rank_(rank), condition_(condition)
    {
    }

    saba_state_complement_tgba::
    saba_state_complement_tgba(const saba_state_complement_tgba* state_taa)
      : state_(state_taa->state_), rank_(state_taa->rank_),
        condition_(state_taa->condition_)
    {
    }

    int
    saba_state_complement_tgba::compare(const saba_state* o) const
    {
      const saba_state_complement_tgba* other =
        dynamic_cast<const saba_state_complement_tgba*>(o);

      int compare_value = get_state()->compare(other->get_state());
      if (compare_value != 0)
        return compare_value;

      if (get_rank() != other->get_rank())
        return get_rank() - other->get_rank();

      return acceptance_conditions().id() -
        other->acceptance_conditions().id();
    }

    size_t
    saba_state_complement_tgba::hash() const
    {
      size_t hash = get_state()->hash() ^ wang32_hash(get_rank());
      hash ^= wang32_hash(acceptance_conditions().id());
      return hash;
    }

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

    bdd
    saba_state_complement_tgba::acceptance_conditions() const
    {
      if ((get_rank() & 1) == 1)
        return condition_;
      else
        return bddfalse;
    }

    const state*
    saba_state_complement_tgba::get_state() const
    {
      return state_.get();
    }

    rank_t
    saba_state_complement_tgba::get_rank() const
    {
      return rank_;
    }


    /// Successor iterators used by spot::saba_complement_tgba.
    /// \ingroup saba_representation
    ///
    /// Since the algorithm works on-the-fly, the key components of the
    /// algorithm are implemented in this class.
    ///
    class saba_complement_tgba_succ_iterator: public saba_succ_iterator
    {
    public:
      typedef std::list<saba_state_conjunction*> state_conjunction_list_t;
      typedef std::map<bdd, state_conjunction_list_t, bdd_less_than>
      bdd_list_t;

154
155
      saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr&
					 automaton,
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
                                         bdd the_acceptance_cond,
                                         const saba_state_complement_tgba*
                                         origin);
      virtual ~saba_complement_tgba_succ_iterator();

      virtual void first();
      virtual void next();
      virtual bool done() const;
      virtual saba_state_conjunction* current_conjunction() const;
      virtual bdd current_condition() const;
    private:
      void get_atomics(std::set<int>& list, bdd c);
      void get_conj_list();
      void state_conjunction();
      void delete_condition_list();

172
      const_tgba_digraph_ptr automaton_;
173
174
175
176
177
178
179
180
181
      bdd the_acceptance_cond_;
      const saba_state_complement_tgba* origin_;
      bdd_list_t condition_list_;
      bdd_list_t::const_iterator current_condition_;
      state_conjunction_list_t::const_iterator current_conjunction_;
      state_conjunction_list_t::const_iterator current_end_conjunction_;
    };

    saba_complement_tgba_succ_iterator::
182
    saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr& automaton,
183
184
185
186
187
                                      bdd the_acceptance_cond,
                                      const saba_state_complement_tgba* origin)
      : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
        origin_(origin)
    {
188
      assert(automaton->is_sba());
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
214
215
      // If state not accepting or rank is even
      if (((origin_->get_rank() & 1) == 0) ||
          !automaton_->state_is_accepting(origin_->get_state()))
      {
        get_conj_list();
        state_conjunction();
      }
    }

    saba_complement_tgba_succ_iterator::
    ~saba_complement_tgba_succ_iterator()
    {
      delete_condition_list();
    }

    void
    saba_complement_tgba_succ_iterator::state_conjunction()
    {
      int max_rank = origin_->get_rank();

      for (bdd_list_t::iterator it = condition_list_.begin();
           it != condition_list_.end();
           ++it)
      {
        // Get successors states.
        bdd condition = it->first;
        std::vector<shared_state> state_list;
216
217
218
219
220
221
222
	for (auto iterator: automaton_->succ(origin_->get_state()))
	  {
	    bdd c = iterator->current_condition();
	    if ((c & condition) != bddfalse)
	      state_list.push_back(shared_state(iterator->current_state(),
						shared_state_deleter));
	  }
223
224
225
226

        // Make the conjunction with ranks.
        std::vector<int> current_ranks(state_list.size(), max_rank);

227
228
229
        if (state_list.empty())
          return;

230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
        do
        {
          explicit_state_conjunction* conj = new explicit_state_conjunction();
          for (unsigned i = 0; i < state_list.size(); ++i)
          {
            conj->add(new saba_state_complement_tgba(state_list[i],
                                                     current_ranks[i],
                                                     the_acceptance_cond_));
          }
          it->second.push_back(conj);

          if (current_ranks[0] <= 0)
            break;

          unsigned order = state_list.size() - 1;
          while (current_ranks[order] == 0)
          {
            current_ranks[order] = max_rank;
            --order;
          }
          --current_ranks[order];
        }
        while (1);
      }
    }

    /// Insert in \a list atomic properties of the formula \a c.
    void
    saba_complement_tgba_succ_iterator::get_atomics(std::set<int>& list, bdd c)
    {
      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;
      }
    }

    /// Free the conjunctions in the condition map.
    void
    saba_complement_tgba_succ_iterator::delete_condition_list()
    {
      for (bdd_list_t::iterator i = condition_list_.begin();
           i != condition_list_.end();
           ++i)
      {
        for (state_conjunction_list_t::iterator j = i->second.begin();
             j != i->second.end();
             ++j)
          delete *j;
      }
      condition_list_.clear();
    }

    /// Create the conjunction of all the atomic properties from
    /// the successors of the current state.
    void
    saba_complement_tgba_succ_iterator::get_conj_list()
    {
      std::set<int> atomics;
      delete_condition_list();

296
      for (auto iterator: automaton_->succ(origin_->get_state()))
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
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
366
367
368
369
      {
        bdd c = iterator->current_condition();
        get_atomics(atomics, c);
      }

      // 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_[result] = state_conjunction_list_t();
      }
    }

    void
    saba_complement_tgba_succ_iterator::first()
    {
      current_condition_ = condition_list_.begin();
      if (current_condition_ != condition_list_.end())
      {
        current_conjunction_ = current_condition_->second.begin();
        current_end_conjunction_ = current_condition_->second.end();
      }
    }

    void
    saba_complement_tgba_succ_iterator::next()
    {
      if (++current_conjunction_ == current_end_conjunction_)
      {
        ++current_condition_;
        if (current_condition_ != condition_list_.end())
        {
          current_conjunction_ = current_condition_->second.begin();
          current_end_conjunction_ = current_condition_->second.end();
        }
      }
    }

    bool
    saba_complement_tgba_succ_iterator::done() const
    {
      return (current_condition_ == condition_list_.end());
    }

    saba_state_conjunction*
    saba_complement_tgba_succ_iterator::current_conjunction() const
    {
      return (*current_conjunction_)->clone();
    }

    bdd
    saba_complement_tgba_succ_iterator::current_condition() const
    {
      return current_condition_->first;
    }

  } // end namespace anonymous.

370
  saba_complement_tgba::saba_complement_tgba(const const_tgba_ptr& a)
371
    : automaton_(degeneralize(a))
372
373
374
375
376
  {
    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);
377
    nb_states_ = automaton_->num_states();
378
379
380
381
382
383
384
385
386
387
388
389
390
391
  }

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

  saba_state*
  saba_complement_tgba::get_init_state() const
  {
    state* original_init_state = automaton_->get_init_state();
    saba_state_complement_tgba* new_init;
    if (automaton_->state_is_accepting(original_init_state))
      new_init =
392
393
        new saba_state_complement_tgba(shared_state(original_init_state,
						    shared_state_deleter),
394
395
396
397
                                       2 * nb_states_,
                                       the_acceptance_cond_);
    else
      new_init =
398
399
        new saba_state_complement_tgba(shared_state(original_init_state,
						    shared_state_deleter),
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
                                       2 * nb_states_,
                                       bddfalse);

    return new_init;
  }

  saba_succ_iterator*
  saba_complement_tgba::succ_iter(const saba_state* local_state) const
  {
    const saba_state_complement_tgba* state =
      dynamic_cast<const saba_state_complement_tgba*>(local_state);
    assert(state);

    return new saba_complement_tgba_succ_iterator(automaton_,
                                                  the_acceptance_cond_,
                                                  state);
  }

418
  bdd_dict_ptr
419
420
421
422
423
424
425
426
427
428
429
430
  saba_complement_tgba::get_dict() const
  {
    return automaton_->get_dict();
  }

  std::string
  saba_complement_tgba::format_state(const saba_state* state) const
  {
    const saba_state_complement_tgba* s =
      dynamic_cast<const saba_state_complement_tgba*>(state);
    assert(s);
    std::ostringstream ss;
431
432
433
434
435
    ss << "{ original: " << automaton_->format_state(s->get_state())
       << "\n  rank: " << s->get_rank()
       << "\n  acc: " << bdd_format_accset(get_dict(),
					   s->acceptance_conditions())
       << " }";
436
437
438
439
440
441
442
443
444
445
    return ss.str();
  }

  bdd
  saba_complement_tgba::all_acceptance_conditions() const
  {
    return the_acceptance_cond_;
  }

} // end namespace spot.