sccfilter.cc 12.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// 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
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/reachiter.hh>
#include <spot/twaalgos/sccinfo.hh>
23
24
25
26
27

namespace spot
{
  namespace
  {
28
29
30
31
    // BDD.id -> Acc number
    typedef std::map<int, unsigned> accremap_t;
    typedef std::vector<accremap_t> remap_table_t;

32
    typedef std::tuple<bool, bdd, acc_cond::mark_t> filtered_trans;
33

34

35
36
37
38
    // SCC filters are objects with two methods:
    //  state(src) return true iff s should be kept
    //  trans(src, dst, cond, acc) returns a triplet
    //     (keep, cond2, acc2) where keep is a Boolean stating if the
39
    //                      edge should be kept, and cond2/acc2
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
    //                      give replacement values for cond/acc
    struct id_filter
    {
      scc_info* si;
      id_filter(scc_info* si)
	: si(si)
      {
      }

      // Accept all states
      bool state(unsigned)
      {
	return true;
      }

55
      void fix_acceptance(const twa_graph_ptr& out)
56
      {
57
	out->copy_acceptance_of(this->si->get_aut());
58
59
      }

60
      // Accept all edges, unmodified
61
      filtered_trans trans(unsigned, unsigned, bdd cond, acc_cond::mark_t acc)
62
63
64
65
66
67
      {
	return filtered_trans{true, cond, acc};
      }
    };

    // Remove useless states.
68
69
    template <class next_filter = id_filter>
    struct state_filter: next_filter
70
    {
71
72
73
      template<typename... Args>
      state_filter(scc_info* si, Args&&... args)
	: next_filter(si, std::forward<Args>(args)...)
74
75
      {
      }
76
77
78

      bool state(unsigned s)
      {
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
	return this->next_filter::state(s) && this->si->is_useful_state(s);
      }
    };

    // Suspension filter, used only by compsusp.cc
    template <class next_filter = id_filter>
    struct susp_filter: next_filter
    {
      bdd suspvars;
      bdd ignoredvars;
      bool early_susp;

      template<typename... Args>
      susp_filter(scc_info* si,
		  bdd suspvars, bdd ignoredvars, bool early_susp,
		  Args&&... args)
	: next_filter(si, std::forward<Args>(args)...),
	  suspvars(suspvars),
	  ignoredvars(ignoredvars),
	  early_susp(early_susp)
      {
      }

      filtered_trans trans(unsigned src, unsigned dst,
103
			   bdd cond, acc_cond::mark_t acc)
104
105
106
107
108
109
110
111
112
113
114
      {
	bool keep;
	std::tie(keep, cond, acc) =
	  this->next_filter::trans(src, dst, cond, acc);

	if (keep)
	  {
	    // Always remove ignored variables
	    cond = bdd_exist(cond, ignoredvars);

	    // Remove the suspension variables only if
115
	    // the destination in a rejecting SCC,
116
117
	    // or if we are between SCC with early_susp unset.
	    unsigned u = this->si->scc_of(dst);
118
	    if (this->si->is_rejecting_scc(u)
119
120
121
122
123
		|| (!early_susp && (u != this->si->scc_of(src))))
	      cond = bdd_exist(cond, suspvars);
	  }

	return filtered_trans(keep, cond, acc);
124
125
126
      }
    };

127
    // Remove acceptance conditions from all edges outside of
128
    // non-accepting SCCs.  If "RemoveAll" is false, keep those on
129
130
131
132
    // transitions entering accepting SCCs.  If "PreserveSBA", is set
    // only touch a transition if all its neighbor siblings can be
    // touched as well.
    template <bool RemoveAll, bool PreserveSBA, class next_filter = id_filter>
133
    struct acc_filter_mask: next_filter
134
    {
135
136
      acc_cond::mark_t accmask;

137
      template<typename... Args>
138
      acc_filter_mask(scc_info* si, Args&&... args)
139
	: next_filter(si, std::forward<Args>(args)...)
140
      {
141
142
143
144
145
146
147
	acc_cond::mark_t fin;
	acc_cond::mark_t inf;
	std::tie(inf, fin) =
	  si->get_aut()->acc().get_acceptance().used_inf_fin_sets();
	// If an SCC is rejecting, we can mask all the sets that are
	// used only as Inf in the acceptance.
	accmask = ~(inf - fin);
148
149
150
      }

      filtered_trans trans(unsigned src, unsigned dst,
151
			   bdd cond, acc_cond::mark_t acc)
152
      {
153
154
155
	bool keep;
	std::tie(keep, cond, acc) =
	  this->next_filter::trans(src, dst, cond, acc);
156

157
158
	if (keep)
	  {
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
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
	    unsigned u = this->si->scc_of(src);
	    unsigned v = this->si->scc_of(dst);
	    // The basic rules are as follows:
	    //
	    // - If an edge is between two SCCs, is OK to remove
	    //   all acceptance sets, as this edge cannot be part
	    //   of any loop.
	    // - If an edge is in an non-accepting SCC, we can only
	    //   remove the Inf sets, as removinf the Fin sets
	    //   might make the SCC accepting.
	    //
	    // The above rules are made more complex with two flags:
	    //
	    // - If PreserveSBA is set, we have to tree a transition
	    //   leaving an SCC as other transitions inside the SCC,
	    //   otherwise we will break the property that all
	    //   transitions leaving the same state have identical set
	    //   membership.
	    // - If RemoveAll is false, we like to keep the membership
	    //   of transitions entering an SCC.  This can only be
	    //   done if PreserveSBA is unset, unfortunately.
	    if (u == v)
	      {
		if (this->si->is_rejecting_scc(u))
		  acc &= accmask;
	      }
	    else if (PreserveSBA && this->si->is_rejecting_scc(u))
	      {
		if (!this->si->is_trivial(u))
		  acc &= accmask; // No choice.
		else if (RemoveAll)
		  acc = 0U;
	      }
	    else if (!PreserveSBA)
	      {
		if (RemoveAll)
		  acc = 0U;
		else if (this->si->is_rejecting_scc(v))
		  acc &= accmask;
	      }
199
200
	  }
	return filtered_trans(keep, cond, acc);
201
202
203
      }
    };

204
205
206
    // Simplify redundant acceptance sets used in each SCCs.
    template <class next_filter = id_filter>
    struct acc_filter_simplify: next_filter
207
    {
208
209
      // Acceptance sets to strip in each SCC.
      std::vector<acc_cond::mark_t> strip_;
210

211
212
213
      template<typename... Args>
      acc_filter_simplify(scc_info* si, Args&&... args)
	: next_filter(si, std::forward<Args>(args)...)
214
215
216
      {
      }

217
      void fix_acceptance(const twa_graph_ptr& out)
218
      {
219
	auto& acc = this->si->get_aut()->acc();
220
221
	if (!acc.is_generalized_buchi())
	  throw std::runtime_error
222
	    ("simplification of SCC acceptance works only with "
223
	     "generalized Büchi acceptance");
224

225
	unsigned scc_count = this->si->scc_count();
226
227
228
229
230
	auto used_acc = this->si->used_acc();
	assert(used_acc.size() == scc_count);
	strip_.resize(scc_count);
	std::vector<unsigned> cnt(scc_count); // # of useful sets in each SCC
	unsigned max = 0;		      // Max number of useful sets
231
232
	for (unsigned n = 0; n < scc_count; ++n)
	  {
233
	    if (this->si->is_rejecting_scc(n))
234
	      continue;
235
236
237
238
	    strip_[n] = acc.useless(used_acc[n].begin(), used_acc[n].end());
	    cnt[n] = acc.num_sets() - strip_[n].count();
	    if (cnt[n] > max)
	      max = cnt[n];
239
240
241
242
243
244
	  }
	// Now that we know about the max number of acceptance
	// conditions, add extra acceptance conditions to those SCC
	// that do not have enough.
	for (unsigned n = 0; n < scc_count; ++n)
	  {
245
	    if (this->si->is_rejecting_scc(n))
246
	      continue;
247
248
	    if (cnt[n] < max)
	      strip_[n].remove_some(max - cnt[n]);
249
	  }
250
251

	out->set_generalized_buchi(max);
252
253
      }

254
255
      filtered_trans trans(unsigned src, unsigned dst, bdd cond,
			   acc_cond::mark_t acc)
256
      {
257
258
259
260
	bool keep;
	std::tie(keep, cond, acc) =
	  this->next_filter::trans(src, dst, cond, acc);

261
	if (keep && acc)
262
	  {
263
264
	    unsigned u = this->si->scc_of(dst);

265
	    if (this->si->is_rejecting_scc(u))
266
	      acc = 0U;
267
	    else
268
	      acc = acc.strip(strip_[u]);
269
	  }
270
	return filtered_trans{keep, cond, acc};
271
272
273
274
      }
    };


275
    template<class F, typename... Args>
276
    twa_graph_ptr scc_filter_apply(const_twa_graph_ptr aut,
277
				   scc_info* given_si, Args&&... args)
278
    {
279
280
281
282
      unsigned in_n = aut->num_states();
      if (in_n == 0)			 // nothing to filter.
	return make_twa_graph(aut, twa::prop_set::all());

283
      twa_graph_ptr filtered = make_twa_graph(aut->get_dict());
284
      filtered->copy_ap_of(aut);
285

286
287
288
289
      // Compute scc_info if not supplied.
      scc_info* si = given_si;
      if (!si)
	si = new scc_info(aut);
290
      si->determine_unknown_acceptance();
291

292
      F filter(si, std::forward<Args>(args)...);
293
294
295
296
297
298
299
300
301
302
303

      // Renumber all useful states.
      unsigned out_n = 0;		 // Number of output states.
      std::vector<unsigned> inout; // Associate old states to new ones.
      inout.reserve(in_n);
      for (unsigned i = 0; i < in_n; ++i)
	if (filter.state(i))
	  inout.push_back(out_n++);
	else
	  inout.push_back(-1U);

304
      filter.fix_acceptance(filtered);
305
      filtered->new_states(out_n);
306
307
308
309
310
      for (unsigned isrc = 0; isrc < in_n; ++isrc)
	{
	  unsigned osrc = inout[isrc];
	  if (osrc >= out_n)
	    continue;
311
	  for (auto& t: aut->out(isrc))
312
313
314
315
316
317
	    {
	      unsigned odst = inout[t.dst];
	      if (odst >= out_n)
		continue;
	      bool want;
	      bdd cond;
318
	      acc_cond::mark_t acc;
319
320
321
	      std::tie(want, cond, acc) =
		filter.trans(isrc, t.dst, t.cond, t.acc);
	      if (want)
322
		filtered->new_edge(osrc, odst, cond, acc);
323
324
325
326
	    }
	}
      if (!given_si)
	delete si;
327
328
329
330
      // If the initial state has been filtered out, we have to create
      // a new one (not doing so may cause empty automata, which in turn
      // cause all sort of issue with algorithms assuming an automaton
      // has one initial state).
331
      auto init = inout[aut->get_init_state_number()];
332
      filtered->set_init_state(init < out_n ? init : filtered->new_state());
333
334
335
336
337
338
      return filtered;
    }


  }

339
  twa_graph_ptr
340
341
  scc_filter_states(const const_twa_graph_ptr& aut, bool remove_all_useless,
		    scc_info* given_si)
342
  {
343
344
345
346
347
348
349
    twa_graph_ptr res;
    if (remove_all_useless)
      res = scc_filter_apply<state_filter
			     <acc_filter_mask<true, true>>>(aut, given_si);
    else
      res = scc_filter_apply<state_filter
			     <acc_filter_mask<false, true>>>(aut, given_si);
350
    res->prop_copy(aut, { true, true, true, true });
351
    return res;
352
353
  }

354
355
  twa_graph_ptr
  scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless,
356
357
	     scc_info* given_si)
  {
358
    twa_graph_ptr res;
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
359
    // acc_filter_simplify only works for generalized Büchi
360
361
362
    if (aut->acc().is_generalized_buchi())
      {
	if (remove_all_useless)
363
364
365
	  res =
	    scc_filter_apply<state_filter
			     <acc_filter_mask
366
367
			      <true, false,
			       acc_filter_simplify<>>>>(aut, given_si);
368
	else
369
370
371
	  res =
	    scc_filter_apply<state_filter
			     <acc_filter_mask
372
373
			      <false, false,
			       acc_filter_simplify<>>>>(aut, given_si);
374
      }
375
    else
376
377
378
      {
	if (remove_all_useless)
	  res = scc_filter_apply<state_filter
379
380
				 <acc_filter_mask
				  <true, false>>>(aut, given_si);
381
382
	else
	  res = scc_filter_apply<state_filter
383
384
				 <acc_filter_mask
				  <false, false>>>(aut, given_si);
385
      }
386
    res->merge_edges();
387
    res->prop_copy(aut,
388
389
390
391
392
		   { false,  // state-based acceptance is not preserved
		     true,
		     true,
		     true,
		   });
393
    return res;
394
395
  }

396
397
  twa_graph_ptr
  scc_filter_susp(const const_twa_graph_ptr& aut, bool remove_all_useless,
398
399
400
		  bdd suspvars, bdd ignoredvars, bool early_susp,
		  scc_info* given_si)
  {
401
    twa_graph_ptr res;
402
    if (remove_all_useless)
403
404
      res = scc_filter_apply<susp_filter
			     <state_filter
405
			      <acc_filter_mask
406
407
408
409
410
			       <true, false,
				acc_filter_simplify<>>>>>(aut, given_si,
							  suspvars,
							  ignoredvars,
							  early_susp);
411
    else
412
413
      res = scc_filter_apply<susp_filter
			     <state_filter
414
			      <acc_filter_mask
415
416
417
418
419
			       <false, false,
				acc_filter_simplify<>>>>>(aut, given_si,
							  suspvars,
							  ignoredvars,
							  early_susp);
420
    res->merge_edges();
421
    res->prop_copy(aut,
422
423
424
		   { false,  // state-based acceptance is not preserved
		     true,
		     false,	// determinism may not be preserved
425
		     false,  	// stutter inv. of suspvars probably altered
426
		   });
427
    return res;
428
429
  }

430
}