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
}