powerset.cc 10.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 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
#include "powerset.hh"
27
28
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
29
#include "tgbaalgos/sccinfo.hh"
30
31
#include "tgbaalgos/cycles.hh"
#include "tgbaalgos/gtec/gtec.hh"
32
#include "tgbaalgos/product.hh"
33
#include "tgba/bddprint.hh"
34
35
36
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
37
#include "tgbaalgos/dtgbacomp.hh"
38
#include "ltlast/unop.hh"
39
40
#include "misc/bitvect.hh"
#include "misc/bddlt.hh"
41
42
43

namespace spot
{
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
  namespace
  {

    static unsigned
    number_of_variables(bdd vin)
    {
      unsigned nap = 0;
      int v = vin.id();
      while (v != 1)
	{
	  v = bdd_high(v);
	  ++nap;
	}
      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)
	if (in->get(pos))
	  ps.insert(pos);
      return ps;
    }

    struct bv_hash
    {
      size_t operator()(const bitvect* bv) const
      {
	return bv->hash();
      }
    };

    struct bv_equal
    {
      bool operator()(const bitvect* bvl, const bitvect* bvr) const
      {
	return *bvl == *bvr;
      }
    };
  }

88
89
  twa_graph_ptr
  tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge)
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
    bdd allap = bddtrue;
    {
      typedef std::set<bdd, bdd_less_than> sup_map;
      sup_map sup;
      // Record occurrences of all guards
      for (auto& t: aut->transitions())
	sup.emplace(t.cond);
      for (auto& i: sup)
	allap &= bdd_support(i);
    }

    unsigned nap = number_of_variables(allap);

    // Call this before aut->num_states(), since it might add a state.
    unsigned init_num = aut->get_init_state_number();

    unsigned ns = aut->num_states();
    assert(ns > 0);

    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)
      {
	bdd one = bdd_satoneset(all, allap, bddfalse);
	all -= one;
	bdd2num.emplace(one, num2bdd.size());
	num2bdd.push_back(one);
      }

    size_t nc = num2bdd.size();	// number of conditions
    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)
      {
	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);
	      }
	  }
      }

151
    typedef power_map::power_state power_state;
152

153
    typedef std::unordered_map<bitvect*, int, bv_hash, bv_equal> power_set;
154
    power_set seen;
155
156
157

    std::vector<const bitvect*>toclean;

158
    auto res = make_twa_graph(aut->get_dict());
159
    res->copy_ap_of(aut);
160
161

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

173
174
175
176
    // 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)
177
      {
178
	om->clear_all();
179

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

	for (auto s: src)
183
	  {
184
185
186
187
188
189
190
191
	    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())
192
	      continue;
193
194
	    auto i = seen.find(dst);
	    unsigned dst_num;
195
196
	    if (i != seen.end())
	      {
197
		dst_num = i->second;
198
199
200
	      }
	    else
	      {
201
202
203
204
205
206
207
		dst_num = res->new_state();
		auto dst2 = dst->clone();
		seen[dst2] = dst_num;
		toclean.push_back(dst2);
		auto ps = bv_to_ps(dst);
		assert(pm.map_.size() == dst_num);
		pm.map_.emplace_back(std::move(ps));
208
	      }
209
	    res->new_transition(src_num, dst_num, num2bdd[c]);
210
211
	  }
      }
212
213
214

    for (auto v: toclean)
      delete v;
215
216
    if (merge)
      res->merge_transitions();
217
218
    return res;
  }
219

220
221
  twa_graph_ptr
  tgba_powerset(const const_twa_graph_ptr& aut)
222
223
224
225
  {
    power_map pm;
    return tgba_powerset(aut, pm);
  }
226
227
228
229
230


  namespace
  {

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

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

255
      bool fix_scc(const int m)
256
257
258
      {
	reject_.clear();
	accept_.clear();
259
	cycles_left_ = threshold_;
260
261
	run(m);

262
//	std::cerr << "SCC #" << m << '\n';
263
//	std::cerr << "REJECT: ";
264
//	print_set(std::cerr, reject_) << '\n';
265
//	std::cerr << "ALL: ";
266
//	print_set(std::cerr, all_) << '\n';
267
268
269
270
//	for (set_set::const_iterator j = accept_.begin();
//	     j != accept_.end(); ++j)
//	  {
//	    std::cerr << "ACCEPT: ";
271
//	    print_set(std::cerr, *j) << '\n';
272
273
//	  }

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

      bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
      {
282
	auto a = std::const_pointer_cast<twa_graph>(aut_);
283

284
	// Build an automaton representing this loop.
285
	auto loop_a = make_twa_graph(aut_->get_dict());
286
	int loop_size = std::distance(begin, dfs_.end());
287
	loop_a->new_states(loop_size);
288
289
290
291
	int n;
	cycle_iter i;
	for (n = 1, i = begin; n <= loop_size; ++n, ++i)
	  {
292
	    trans* t = &a->trans_data(i->succ);
293
	    loop_a->new_transition(n - 1, n % loop_size, t->cond);
294
295
296
297
298
	    if (reject_.find(t) == reject_.end())
	      ts.insert(t);
	  }
	assert(i == dfs_.end());

299
300
	unsigned loop_a_init = loop_a->get_init_state_number();
	assert(loop_a_init == 0);
301
302
303
304
305
306

	// 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.
307
	for (auto s: refmap_.states_of(begin->s))
308
	  {
309
310
	    // Check the product between LOOP_A, and ORIG_A starting
	    // in S.
311
	    if (!product(loop_a, ref_, loop_a_init, s)->is_empty())
312
313
314
315
	      {
		accepting = true;
		break;
	      }
316
317
318
319
320
321
322
323
	  }
	return accepting;
      }

      std::ostream&
      print_set(std::ostream& o, const trans_set& s) const
      {
	o << "{ ";
324
	for (auto i: s)
325
326
	  o << i << ' ';
	o << '}';
327
328
329
330
	return o;
      }

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

357
358
359
360
	// 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_;
361
362
363
      }
    };

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

371
      scc_info sm(det);
372
373
374

      unsigned scc_count = sm.scc_count();

375
      fix_scc_acceptance fsa(sm, ref, refmap, threshold);
376
377

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

385
386
  twa_graph_ptr
  tba_determinize(const const_twa_graph_ptr& aut,
387
		  unsigned threshold_states, unsigned threshold_cycles)
388
389
390
391
392
  {
    power_map pm;
    // Do not merge transitions in the deterministic automaton.  If we
    // 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.
393
    auto det = tgba_powerset(aut, pm, false);
394
395

    if ((threshold_states > 0)
396
	&& (pm.map_.size() > aut->num_states() * threshold_states))
397
      return nullptr;
398
    if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
399
      return nullptr;
400
401
402
    det->merge_transitions();
    return det;
  }
403

404
405
  twa_graph_ptr
  tba_determinize_check(const twa_graph_ptr& aut,
406
407
			unsigned threshold_states,
			unsigned threshold_cycles,
408
			const ltl::formula* f,
409
			const_twa_graph_ptr neg_aut)
410
411
412
  {
    if (f == 0 && neg_aut == 0)
      return 0;
413
    if (aut->acc().num_sets() > 1)
414
415
      return 0;

416
    auto det = tba_determinize(aut, threshold_states, threshold_cycles);
417
418

    if (!det)
419
      return nullptr;
420

421
    if (neg_aut == nullptr)
422
423
424
425
426
427
428
      {
	const ltl::formula* neg_f =
	  ltl::unop::instance(ltl::unop::Not, f->clone());
	neg_aut = ltl_to_tgba_fm(neg_f, aut->get_dict());
	neg_f->destroy();

	// Remove useless SCCs.
429
	neg_aut = scc_filter(neg_aut, true);
430
431
      }

432
433
434
435
436
437
    if (product(det, neg_aut)->is_empty())
      // Complement the DBA.
      if (product(aut, dtgba_complement(det))->is_empty())
	// Finally, we are now sure that it was safe
	// to determinize the automaton.
	return det;
438

439
    return aut;
440
  }
441
}