powerset.cc 10.5 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2013, 2014 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
24

#include <set>
#include <deque>
25
26
#include <iterator>
#include <vector>
27
#include "powerset.hh"
28
29
30
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
#include "bdd.h"
31
32
33
34
35
36
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/cycles.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
37
38
39
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
40
#include "tgbaalgos/dtgbacomp.hh"
41
#include "ltlast/unop.hh"
42
43
44

namespace spot
{
45
  tgba_explicit_number*
46
  tgba_powerset(const tgba* aut, power_map& pm, bool merge)
47
  {
48
49
50
    typedef power_map::power_state power_state;
    typedef std::map<power_map::power_state, int> power_set;
    typedef std::deque<power_map::power_state> todo_list;
51
52
53

    power_set seen;
    todo_list todo;
54
    tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict());
55
56
57

    {
      power_state ps;
58
      const state* s = pm.canonicalize(aut->get_init_state());
59
60
      ps.insert(s);
      todo.push_back(ps);
61
      seen[ps] = 1;
62
      pm.map_[1] = ps;
63
64
65
66
    }

    unsigned state_num = 1;

67
    while (!todo.empty())
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
      {
	power_state src = todo.front();
	todo.pop_front();
	// Compute all variables occurring on outgoing arcs.
	bdd all_vars = bddtrue;
	power_state::const_iterator i;

	for (i = src.begin(); i != src.end(); ++i)
	  all_vars &= aut->support_variables(*i);

	// Compute all possible combinations of these variables.
	bdd all_conds = bddtrue;
	while (all_conds != bddfalse)
	  {
	    bdd cond = bdd_satoneset(all_conds, all_vars, bddtrue);
	    all_conds -= cond;

	    // Construct the set of all states reachable via COND.
	    power_state dest;
	    for (i = src.begin(); i != src.end(); ++i)
	      {
		tgba_succ_iterator *si = aut->succ_iter(*i);
90
		for (si->first(); !si->done(); si->next())
91
92
		  if ((cond >> si->current_condition()) == bddtrue)
		    {
93
		      const state* s = pm.canonicalize(si->current_state());
94
95
96
97
98
99
100
101
		      dest.insert(s);
		    }
		delete si;
	      }
	    if (dest.empty())
	      continue;
	    // Add that transition.
	    power_set::const_iterator i = seen.find(dest);
102
	    int dest_num;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
103
	    state_explicit_number::transition* t;
104
105
	    if (i != seen.end())
	      {
106
107
		dest_num = i->second;
                t = res->create_transition(seen[src], dest_num);
108
109
110
	      }
	    else
	      {
111
112
		dest_num = ++state_num;
		seen[dest] = dest_num;
113
		pm.map_[dest_num] = dest;
114
		todo.push_back(dest);
115
                t = res->create_transition(seen[src], dest_num);
116
117
118
119
	      }
	    res->add_conditions(t, cond);
	  }
      }
120
121
    if (merge)
      res->merge_transitions();
122
123
    return res;
  }
124
125
126
127
128
129
130

  tgba_explicit_number*
  tgba_powerset(const tgba* aut)
  {
    power_map pm;
    return tgba_powerset(aut, pm);
  }
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145


  namespace
  {

    class fix_scc_acceptance: protected enumerate_cycles
    {
    public:
      typedef dfs_stack::const_iterator cycle_iter;
      typedef state_explicit_number::transition trans;
      typedef std::set<trans*> trans_set;
      typedef std::vector<trans_set> set_set;
    protected:
      const tgba* ref_;
      power_map& refmap_;
146
147
148
149
150
      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
151
152

    public:
153
154
155
156
      fix_scc_acceptance(const scc_map& sm, const tgba* ref, power_map& refmap,
			 unsigned threshold)
	: enumerate_cycles(sm), ref_(ref), refmap_(refmap),
	  threshold_(threshold)
157
158
159
      {
      }

160
      bool fix_scc(const int m)
161
162
163
      {
	reject_.clear();
	accept_.clear();
164
	cycles_left_ = threshold_;
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
	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";
//	  }

	bdd acc = aut_->all_acceptance_conditions();
	for (trans_set::iterator i = all_.begin(); i != all_.end(); ++i)
	  {
	    (*i)->acceptance_conditions = acc;
	  }
184
	return threshold_ != 0 && cycles_left_ == 0;
185
186
187
188
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
216
217
218
219
220
221
222
223
224
225
226
227
228
229
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
      }

      bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
      {
	tgba_explicit_number* a =
	  down_cast<tgba_explicit_number*>(const_cast<tgba*>(aut_));
	// Build an automaton representing this loop.
	tgba_explicit_number loop_a(aut_->get_dict());
	int loop_size = std::distance(begin, dfs_.end());
	int n;
	cycle_iter i;
	for (n = 1, i = begin; n <= loop_size; ++n, ++i)
	  {
	    trans* t = a->get_transition(i->succ);
	    loop_a.create_transition(n - 1, n % loop_size)->condition =
	      t->condition;
	    if (reject_.find(t) == reject_.end())
	      ts.insert(t);
	  }
	assert(i == dfs_.end());

	const state* loop_a_init = loop_a.get_init_state();
	assert(loop_a.get_label(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.
	const power_map::power_state& ps =
	  refmap_.states_of(a->get_label(begin->ts->first));
	for (power_map::power_state::const_iterator it = ps.begin();
	     it != ps.end() && !accepting; ++it)
	  {
	    // Construct a product between
	    // LOOP_A, and ORIG_A starting in *IT.

	    tgba* p = new tgba_product_init(&loop_a, ref_,
					    loop_a_init, *it);

	    //spot::dotty_reachable(std::cout, p);

	    couvreur99_check* ec = down_cast<couvreur99_check*>(couvreur99(p));
	    assert(ec);
	    emptiness_check_result* res = ec->check();
	    if (res)
	      accepting = true;
	    delete res;
	    delete ec;
	    delete p;
	  }

	loop_a_init->destroy();
	return accepting;
      }

      std::ostream&
      print_set(std::ostream& o, const trans_set& s) const
      {
	o << "{ ";
	for (trans_set::const_iterator i = s.begin(); i != s.end(); ++i)
	  o << *i << " ";
	o << "}";
	return o;
      }

      virtual bool
      cycle_found(const state* start)
      {
	cycle_iter i = dfs_.begin();
	while (i->ts->first != start)
	  ++i;
	trans_set ts;
	bool is_acc = is_cycle_accepting(i, ts);
	do
	  {
	    //	    std::cerr << aut_->format_state(i->ts->first) << " ";
	    ++i;
	  }
	while (i != dfs_.end());
	//	std::cerr << "  acc=" << is_acc << "  (";
	//	bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") ";
	//	print_set(std::cerr, ts) << "\n";
	if (is_acc)
	  {
	    accept_.push_back(ts);
	    all_.insert(ts.begin(), ts.end());
	  }
	else
	  {
	    for (trans_set::const_iterator i = ts.begin(); i != ts.end(); ++i)
	      {
		trans* t = *i;
		reject_.insert(t);
		for (set_set::iterator j = accept_.begin();
		     j != accept_.end(); ++j)
		  {
		    j->erase(t);
		  }
		all_.erase(t);
	      }
	  }

288
289
290
291
	// 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_;
292
293
294
      }
    };

295
    static bool
296
    fix_dba_acceptance(tgba_explicit_number* det,
297
298
		       const tgba* ref, power_map& refmap,
		       unsigned threshold)
299
300
301
302
303
304
305
306
    {
      det->copy_acceptance_conditions_of(ref);

      scc_map sm(det);
      sm.build_map();

      unsigned scc_count = sm.scc_count();

307
      fix_scc_acceptance fsa(sm, ref, refmap, threshold);
308
309

      for (unsigned m = 0; m < scc_count; ++m)
310
311
312
313
	if (!sm.trivial(m))
	  if (fsa.fix_scc(m))
	    return true;
      return false;
314
315
316
317
    }
  }

  tgba_explicit_number*
318
319
  tba_determinize(const tgba* aut,
		  unsigned threshold_states, unsigned threshold_cycles)
320
321
322
323
324
325
  {
    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.
    tgba_explicit_number* det = tgba_powerset(aut, pm, false);
326
327

    if ((threshold_states > 0)
328
	&& (pm.map_.size() > pm.states_.size() * threshold_states))
329
330
331
332
333
      {
	delete det;
	return 0;
      }
    if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
334
335
336
337
      {
	delete det;
	return 0;
      }
338
339
340
    det->merge_transitions();
    return det;
  }
341
342
343

  tgba*
  tba_determinize_check(const tgba* aut,
344
345
			unsigned threshold_states,
			unsigned threshold_cycles,
346
347
348
349
350
351
352
353
354
			const ltl::formula* f,
			const tgba* neg_aut)
  {
    const tgba* built = 0;
    if (f == 0 && neg_aut == 0)
      return 0;
    if (aut->number_of_acceptance_conditions() > 1)
      return 0;

355
356
    tgba_explicit_number* det =
      tba_determinize(aut, threshold_states, threshold_cycles);
357
358
359

    if (!det)
      return 0;
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384

    if (neg_aut == 0)
      {
	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.
	const tgba* tmp = scc_filter(neg_aut, true);
	delete neg_aut;
	built = neg_aut = tmp;
      }

    bool ok = false;

    tgba* p = new tgba_product(det, neg_aut);
    emptiness_check* ec = couvreur99(p);
    emptiness_check_result* res = ec->check();
    if (!res)
      {
	delete ec;
	delete p;

	// Complement the DBA.
385
	tgba* neg_det = dtgba_complement(det);
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415

	tgba* p = new tgba_product(aut, neg_det);
	emptiness_check* ec = couvreur99(p);
	res = ec->check();

	if (!res)
	  {
	    // Finally, we are now sure that it was safe
	    // to determinize the automaton.
	    ok = true;
	  }

	delete res;
	delete ec;
	delete p;
	delete neg_det;
      }
    else
      {
	delete res;
	delete ec;
	delete p;
      }
    delete built;

    if (ok)
      return det;
    delete det;
    return const_cast<tgba*>(aut);
  }
416
}