powerset.cc 12.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009-2011, 2013-2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// 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
12
// the Free Software Foundation; either version 3 of the License, or
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/>.
22
23

#include <set>
24
25
#include <iterator>
#include <vector>
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
#include <spot/twaalgos/powerset.hh>
#include <spot/misc/hash.hh>
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/cycles.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/misc/bitvect.hh>
#include <spot/misc/bddlt.hh>
41
42
43

namespace spot
{
44
45
46
47
48
49
50
51
52
  namespace
  {

    static unsigned
    number_of_variables(bdd vin)
    {
      unsigned nap = 0;
      int v = vin.id();
      while (v != 1)
53
54
55
56
        {
          v = bdd_high(v);
          ++nap;
        }
57
58
59
60
61
62
63
64
65
      return nap;
    }

    static power_map::power_state
    bv_to_ps(const bitvect* in)
    {
      power_map::power_state ps;
      unsigned ns = in->size();
      for (unsigned pos = 0; pos < ns; ++pos)
66
67
        if (in->get(pos))
          ps.insert(pos);
68
69
70
71
72
73
74
      return ps;
    }

    struct bv_hash
    {
      size_t operator()(const bitvect* bv) const
      {
75
        return bv->hash();
76
77
78
79
80
81
82
      }
    };

    struct bv_equal
    {
      bool operator()(const bitvect* bvl, const bitvect* bvr) const
      {
83
        return *bvl == *bvr;
84
85
86
87
      }
    };
  }

88
89
  twa_graph_ptr
  tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge)
90
  {
91
92
93
94
95
    bdd allap = bddtrue;
    {
      typedef std::set<bdd, bdd_less_than> sup_map;
      sup_map sup;
      // Record occurrences of all guards
96
      for (auto& t: aut->edges())
97
        sup.emplace(t.cond);
98
      for (auto& i: sup)
99
        allap &= bdd_support(i);
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
    }

    unsigned nap = number_of_variables(allap);

    unsigned init_num = aut->get_init_state_number();
    unsigned ns = aut->num_states();

    if ((-1UL / ns) >> nap == 0)
      throw std::runtime_error("too many atomic propositions (or states)");

    // Build a correspondence between conjunctions of APs and unsigned
    // indexes.
    std::vector<bdd> num2bdd;
    num2bdd.reserve(1UL << nap);
    std::map<bdd, unsigned, bdd_less_than> bdd2num;
    bdd all = bddtrue;
    while (all != bddfalse)
      {
118
119
120
        bdd one = bdd_satoneset(all, allap, bddfalse);
        all -= one;
        bdd2num.emplace(one, num2bdd.size());
121
        num2bdd.emplace_back(one);
122
123
      }

124
    size_t nc = num2bdd.size();        // number of conditions
125
126
127
128
129
130
131
132
133
    assert(nc == (1UL << nap));

    // An array of bit vectors of size 'ns'.  Each original state is
    // represented by 'nc' bitvectors representing the possible
    // destinations for each condition.
    auto bv = std::unique_ptr<bitvect_array>(make_bitvect_array(ns, ns * nc));

    for (unsigned src = 0; src < ns; ++src)
      {
134
135
136
137
138
139
140
141
142
143
144
145
        size_t base = src * nc;
        for (auto& t: aut->out(src))
          {
            bdd all = t.cond;
            while (all != bddfalse)
              {
                bdd one = bdd_satoneset(all, allap, bddfalse);
                all -= one;
                unsigned num = bdd2num[one];
                bv->at(base + num).set(t.dst);
              }
          }
146
147
      }

148
    typedef power_map::power_state power_state;
149

150
    typedef std::unordered_map<bitvect*, int, bv_hash, bv_equal> power_set;
151
    power_set seen;
152
153
154

    std::vector<const bitvect*>toclean;

155
    auto res = make_twa_graph(aut->get_dict());
156
    res->copy_ap_of(aut);
157
158

    {
159
160
161
      auto bvi = make_bitvect(ns);
      bvi->set(init_num);
      power_state ps{init_num};
162
      unsigned num = res->new_state();
163
164
165
166
      res->set_init_state(num);
      seen[bvi] = num;
      assert(pm.map_.size() == num);
      pm.map_.emplace_back(std::move(ps));
167
      toclean.emplace_back(bvi);
168
169
    }

170
171
172
173
    // outgoing map
    auto om = std::unique_ptr<bitvect_array>(make_bitvect_array(ns, nc));

    for (unsigned src_num = 0; src_num < res->num_states(); ++src_num)
174
      {
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
        om->clear_all();

        const power_state& src = pm.states_of(src_num);

        for (auto s: src)
          {
            size_t base = s * nc;
            for (unsigned c = 0; c < nc; ++c)
              om->at(c) |= bv->at(base + c);
          }
        for (unsigned c = 0; c < nc; ++c)
          {
            auto dst = &om->at(c);
            if (dst->is_fully_clear())
              continue;
            auto i = seen.find(dst);
            unsigned dst_num;
            if (i != seen.end())
              {
                dst_num = i->second;
              }
            else
              {
                dst_num = res->new_state();
                auto dst2 = dst->clone();
                seen[dst2] = dst_num;
201
                toclean.emplace_back(dst2);
202
203
204
205
206
207
                auto ps = bv_to_ps(dst);
                assert(pm.map_.size() == dst_num);
                pm.map_.emplace_back(std::move(ps));
              }
            res->new_edge(src_num, dst_num, num2bdd[c]);
          }
208
      }
209
210
211

    for (auto v: toclean)
      delete v;
212
    if (merge)
213
      res->merge_edges();
214
215
    return res;
  }
216

217
218
  twa_graph_ptr
  tgba_powerset(const const_twa_graph_ptr& aut)
219
220
221
222
  {
    power_map pm;
    return tgba_powerset(aut, pm);
  }
223
224
225
226
227


  namespace
  {

228
    class fix_scc_acceptance final: protected enumerate_cycles
229
230
231
    {
    public:
      typedef dfs_stack::const_iterator cycle_iter;
232
233
234
      typedef twa_graph_edge_data trans;
      typedef std::set<trans*> edge_set;
      typedef std::vector<edge_set> set_set;
235
    protected:
236
      const_twa_graph_ptr ref_;
237
      power_map& refmap_;
238
239
240
241
242
      edge_set reject_;        // set of rejecting edges
      set_set accept_;                // set of cycles that are accepting
      edge_set all_;                // all non rejecting edges
      unsigned threshold_;        // maximum count of enumerated cycles
      unsigned cycles_left_;         // count of cycles left to explore
243
244

    public:
245
      fix_scc_acceptance(const scc_info& sm, const_twa_graph_ptr ref,
246
247
248
                         power_map& refmap, unsigned threshold)
        : enumerate_cycles(sm), ref_(ref), refmap_(refmap),
          threshold_(threshold)
249
250
251
      {
      }

252
      bool fix_scc(const int m)
253
      {
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
        reject_.clear();
        accept_.clear();
        cycles_left_ = threshold_;
        run(m);

//        std::cerr << "SCC #" << m << '\n';
//        std::cerr << "REJECT: ";
//        print_set(std::cerr, reject_) << '\n';
//        std::cerr << "ALL: ";
//        print_set(std::cerr, all_) << '\n';
//        for (set_set::const_iterator j = accept_.begin();
//             j != accept_.end(); ++j)
//          {
//            std::cerr << "ACCEPT: ";
//            print_set(std::cerr, *j) << '\n';
//          }

        auto acc = aut_->acc().all_sets();
        for (auto i: all_)
          i->acc = acc;
        return threshold_ != 0 && cycles_left_ == 0;
275
276
      }

277
      bool is_cycle_accepting(cycle_iter begin, edge_set& ts) const
278
      {
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
        auto a = std::const_pointer_cast<twa_graph>(aut_);

        // Build an automaton representing this loop.
        auto loop_a = make_twa_graph(aut_->get_dict());
        int loop_size = std::distance(begin, dfs_.end());
        loop_a->new_states(loop_size);
        int n;
        cycle_iter i;
        for (n = 1, i = begin; n <= loop_size; ++n, ++i)
          {
            trans* t = &a->edge_data(i->succ);
            loop_a->new_edge(n - 1, n % loop_size, t->cond);
            if (reject_.find(t) == reject_.end())
              ts.insert(t);
          }
        assert(i == dfs_.end());

        unsigned loop_a_init = loop_a->get_init_state_number();
        assert(loop_a_init == 0);

        // Check if the loop is accepting in the original automaton.
        bool accepting = false;

        // Iterate on each original state corresponding to the
        // start of the loop in the determinized automaton.
        for (auto s: refmap_.states_of(begin->s))
          {
            // Check the product between LOOP_A, and ORIG_A starting
            // in S.
            if (!product(loop_a, ref_, loop_a_init, s)->is_empty())
              {
                accepting = true;
                break;
              }
          }
        return accepting;
315
316
317
      }

      std::ostream&
318
      print_set(std::ostream& o, const edge_set& s) const
319
      {
320
321
322
323
324
        o << "{ ";
        for (auto i: s)
          o << i << ' ';
        o << '}';
        return o;
325
326
327
      }

      virtual bool
328
      cycle_found(unsigned start) override
329
      {
330
331
332
333
334
335
336
337
338
339
        cycle_iter i = dfs_.begin();
        while (i->s != start)
          ++i;
        edge_set ts;
        bool is_acc = is_cycle_accepting(i, ts);
        do
          ++i;
        while (i != dfs_.end());
        if (is_acc)
          {
340
            accept_.emplace_back(ts);
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
            all_.insert(ts.begin(), ts.end());
          }
        else
          {
            for (auto t: ts)
              {
                reject_.insert(t);
                for (auto& j: accept_)
                  j.erase(t);
                all_.erase(t);
              }
          }

        // Abort this algorithm if we have seen too much cycles, i.e.,
        // when cycle_left_ *reaches* 0.  (If cycle_left_ == 0, that
        // means we had no limit.)
        return (cycles_left_ == 0) || --cycles_left_;
358
359
360
      }
    };

361
    static bool
362
    fix_dba_acceptance(twa_graph_ptr det,
363
364
                       const_twa_graph_ptr ref, power_map& refmap,
                       unsigned threshold)
365
    {
366
      det->copy_acceptance_of(ref);
367

368
      scc_info sm(det);
369
370
371

      unsigned scc_count = sm.scc_count();

372
      fix_scc_acceptance fsa(sm, ref, refmap, threshold);
373
374

      for (unsigned m = 0; m < scc_count; ++m)
375
376
377
        if (!sm.is_trivial(m))
          if (fsa.fix_scc(m))
            return true;
378
      return false;
379
380
381
    }
  }

382
383
  twa_graph_ptr
  tba_determinize(const const_twa_graph_ptr& aut,
384
                  unsigned threshold_states, unsigned threshold_cycles)
385
386
  {
    power_map pm;
387
    // Do not merge edges in the deterministic automaton.  If we
388
389
    // add two self-loops labeled by "a" and "!a", we do not want
    // these to be merged as "1" before the acceptance has been fixed.
390
    auto det = tgba_powerset(aut, pm, false);
391
392

    if ((threshold_states > 0)
393
        && (pm.map_.size() > aut->num_states() * threshold_states))
394
      return nullptr;
395
    if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
396
      return nullptr;
397
    det->merge_edges();
398
399
    return det;
  }
400

401
402
  twa_graph_ptr
  tba_determinize_check(const twa_graph_ptr& aut,
403
404
405
406
                        unsigned threshold_states,
                        unsigned threshold_cycles,
                        formula f,
                        const_twa_graph_ptr neg_aut)
407
  {
408
409
    if (f == nullptr && neg_aut == nullptr)
      return nullptr;
410
    if (aut->num_sets() > 1)
411
      return nullptr;
412

413
    auto det = tba_determinize(aut, threshold_states, threshold_cycles);
414
415

    if (!det)
416
      return nullptr;
417

418
    if (neg_aut == nullptr)
419
      {
420
421
422
        neg_aut = ltl_to_tgba_fm(formula::Not(f), aut->get_dict());
        // Remove useless SCCs.
        neg_aut = scc_filter(neg_aut, true);
423
424
      }

425
426
    if (product(det, neg_aut)->is_empty())
      // Complement the DBA.
427
      if (product(aut, remove_fin(dtwa_complement(det)))->is_empty())
428
429
430
        // Finally, we are now sure that it was safe
        // to determinize the automaton.
        return det;
431

432
    return aut;
433
  }
434
}