powerset.cc 8.85 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
34
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
35
36
37
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
38
#include "tgbaalgos/dtgbacomp.hh"
39
#include "ltlast/unop.hh"
40
41
42

namespace spot
{
43
  tgba_digraph_ptr
44
  tgba_powerset(const const_tgba_digraph_ptr& aut, power_map& pm, bool merge)
45
  {
46
47
    typedef power_map::power_state power_state;
    typedef std::map<power_map::power_state, int> power_set;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
    typedef std::vector<power_map::power_state> todo_list;
49
50
51

    power_set seen;
    todo_list todo;
52
    auto res = make_tgba_digraph(aut->get_dict());
53
    res->copy_ap_of(aut);
54
55

    {
56
      power_state ps{aut->get_init_state_number()};
57
      todo.push_back(ps);
58
      unsigned num = res->new_state();
59
60
      seen[ps] = num;
      pm.map_[num] = ps;
61
62
    }

63
    while (!todo.empty())
64
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
66
	power_state src = todo.back();
	todo.pop_back();
67
68
	// Compute all variables occurring on outgoing arcs.
	bdd all_vars = bddtrue;
69
	for (auto s: src)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
70
	  for (auto& i: aut->out(s))
71
	    all_vars &= bdd_support(i.cond);
72
73

	bdd all_conds = bddtrue;
74
	// Iterate over all possible conditions
75
76
77
78
79
80
81
	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;
82
	    for (auto s: src)
83
84
	      for (auto& si: aut->out(s))
		if (bdd_implies(cond, si.cond))
85
		  dest.insert(si.dst);
86
87
88
	    if (dest.empty())
	      continue;
	    // Add that transition.
89
	    auto i = seen.find(dest);
90
	    int dest_num;
91
92
	    if (i != seen.end())
	      {
93
		dest_num = i->second;
94
95
96
	      }
	    else
	      {
97
		dest_num = res->new_state();
98
		seen[dest] = dest_num;
99
		pm.map_[dest_num] = dest;
100
101
		todo.push_back(dest);
	      }
102
	    res->new_transition(seen[src], dest_num, cond);
103
104
	  }
      }
105
106
    if (merge)
      res->merge_transitions();
107
108
    return res;
  }
109

110
  tgba_digraph_ptr
111
  tgba_powerset(const const_tgba_digraph_ptr& aut)
112
113
114
115
  {
    power_map pm;
    return tgba_powerset(aut, pm);
  }
116
117
118
119
120
121
122
123
124


  namespace
  {

    class fix_scc_acceptance: protected enumerate_cycles
    {
    public:
      typedef dfs_stack::const_iterator cycle_iter;
125
      typedef tgba_graph_trans_data trans;
126
127
128
      typedef std::set<trans*> trans_set;
      typedef std::vector<trans_set> set_set;
    protected:
129
      const_tgba_digraph_ptr ref_;
130
      power_map& refmap_;
131
132
133
134
135
      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
136
137

    public:
138
      fix_scc_acceptance(const scc_info& sm, const_tgba_digraph_ptr ref,
139
			 power_map& refmap, unsigned threshold)
140
141
	: enumerate_cycles(sm), ref_(ref), refmap_(refmap),
	  threshold_(threshold)
142
143
144
      {
      }

145
      bool fix_scc(const int m)
146
147
148
      {
	reject_.clear();
	accept_.clear();
149
	cycles_left_ = threshold_;
150
151
	run(m);

152
//	std::cerr << "SCC #" << m << '\n';
153
//	std::cerr << "REJECT: ";
154
//	print_set(std::cerr, reject_) << '\n';
155
//	std::cerr << "ALL: ";
156
//	print_set(std::cerr, all_) << '\n';
157
158
159
160
//	for (set_set::const_iterator j = accept_.begin();
//	     j != accept_.end(); ++j)
//	  {
//	    std::cerr << "ACCEPT: ";
161
//	    print_set(std::cerr, *j) << '\n';
162
163
//	  }

164
	auto acc = aut_->acc().all_sets();
165
	for (auto i: all_)
166
	  i->acc = acc;
167
	return threshold_ != 0 && cycles_left_ == 0;
168
169
170
171
      }

      bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
      {
172
	auto a = std::const_pointer_cast<tgba_digraph>(aut_);
173

174
	// Build an automaton representing this loop.
175
	auto loop_a = make_tgba_digraph(aut_->get_dict());
176
	int loop_size = std::distance(begin, dfs_.end());
177
	loop_a->new_states(loop_size);
178
179
180
181
	int n;
	cycle_iter i;
	for (n = 1, i = begin; n <= loop_size; ++n, ++i)
	  {
182
	    trans* t = &a->trans_data(i->succ);
183
	    loop_a->new_transition(n - 1, n % loop_size, t->cond);
184
185
186
187
188
	    if (reject_.find(t) == reject_.end())
	      ts.insert(t);
	  }
	assert(i == dfs_.end());

189
190
	unsigned loop_a_init = loop_a->get_init_state_number();
	assert(loop_a_init == 0);
191
192
193
194
195
196
197

	// 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 =
198
	  refmap_.states_of(a->state_number(begin->ts->first));
199
	for (auto s: ps)
200
	  {
201
202
	    // Check the product between LOOP_A, and ORIG_A starting
	    // in S.
203
	    if (!product(loop_a, ref_, loop_a_init, s)->is_empty())
204
205
206
207
	      {
		accepting = true;
		break;
	      }
208
209
210
211
212
213
214
215
	  }
	return accepting;
      }

      std::ostream&
      print_set(std::ostream& o, const trans_set& s) const
      {
	o << "{ ";
216
	for (auto i: s)
217
218
	  o << i << ' ';
	o << '}';
219
220
221
222
223
224
225
226
227
228
229
230
231
	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
	  {
232
	    //	    std::cerr << aut_->format_state(i->ts->first) << ' ';
233
234
235
236
237
	    ++i;
	  }
	while (i != dfs_.end());
	//	std::cerr << "  acc=" << is_acc << "  (";
	//	bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") ";
238
	//	print_set(std::cerr, ts) << '\n';
239
240
241
242
243
244
245
	if (is_acc)
	  {
	    accept_.push_back(ts);
	    all_.insert(ts.begin(), ts.end());
	  }
	else
	  {
246
	    for (auto t: ts)
247
248
	      {
		reject_.insert(t);
249
250
		for (auto& j: accept_)
		  j.erase(t);
251
252
253
254
		all_.erase(t);
	      }
	  }

255
256
257
258
	// 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_;
259
260
261
      }
    };

262
    static bool
263
    fix_dba_acceptance(tgba_digraph_ptr det,
264
		       const_tgba_digraph_ptr ref, power_map& refmap,
265
		       unsigned threshold)
266
267
268
    {
      det->copy_acceptance_conditions_of(ref);

269
      scc_info sm(det);
270
271
272

      unsigned scc_count = sm.scc_count();

273
      fix_scc_acceptance fsa(sm, ref, refmap, threshold);
274
275

      for (unsigned m = 0; m < scc_count; ++m)
276
	if (!sm.is_trivial(m))
277
278
279
	  if (fsa.fix_scc(m))
	    return true;
      return false;
280
281
282
    }
  }

283
  tgba_digraph_ptr
284
  tba_determinize(const const_tgba_digraph_ptr& aut,
285
		  unsigned threshold_states, unsigned threshold_cycles)
286
287
288
289
290
  {
    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.
291
    auto det = tgba_powerset(aut, pm, false);
292
293

    if ((threshold_states > 0)
294
	&& (pm.map_.size() > aut->num_states() * threshold_states))
295
      return nullptr;
296
    if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
297
      return nullptr;
298
299
300
    det->merge_transitions();
    return det;
  }
301

302
303
  tgba_digraph_ptr
  tba_determinize_check(const tgba_digraph_ptr& aut,
304
305
			unsigned threshold_states,
			unsigned threshold_cycles,
306
			const ltl::formula* f,
307
			const_tgba_digraph_ptr neg_aut)
308
309
310
  {
    if (f == 0 && neg_aut == 0)
      return 0;
311
    if (aut->acc().num_sets() > 1)
312
313
      return 0;

314
    auto det = tba_determinize(aut, threshold_states, threshold_cycles);
315
316

    if (!det)
317
      return nullptr;
318

319
    if (neg_aut == nullptr)
320
321
322
323
324
325
326
      {
	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.
327
	neg_aut = scc_filter(neg_aut, true);
328
329
      }

330
331
332
333
334
335
    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;
336

337
    return aut;
338
  }
339
}