sccfilter.cc 15.2 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
    //                      give replacement values for cond/acc
    struct id_filter
    {
      scc_info* si;
      id_filter(scc_info* si)
45
        : si(si)
46
47
48
49
50
51
      {
      }

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

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
        return filtered_trans{true, cond, acc};
64
65
66
67
      }
    };

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

      bool state(unsigned s)
      {
79
        return this->next_filter::state(s) && this->si->is_useful_state(s);
80
81
82
83
84
85
86
87
88
89
90
91
92
      }
    };

    // 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,
93
94
95
96
97
98
                  bdd suspvars, bdd ignoredvars, bool early_susp,
                  Args&&... args)
        : next_filter(si, std::forward<Args>(args)...),
          suspvars(suspvars),
          ignoredvars(ignoredvars),
          early_susp(early_susp)
99
100
101
102
      {
      }

      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
115
116
117
118
119
120
121
122
123
        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
            // the destination in a rejecting SCC,
            // or if we are between SCC with early_susp unset.
            unsigned u = this->si->scc_of(dst);
            if (this->si->is_rejecting_scc(u)
                || (!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
156
157
158
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
199
200
        bool keep;
        std::tie(keep, cond, acc) =
          this->next_filter::trans(src, dst, cond, acc);

        if (keep)
          {
            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;
              }
          }
        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
      template<typename... Args>
      acc_filter_simplify(scc_info* si, Args&&... args)
213
        : next_filter(si, std::forward<Args>(args)...)
214
215
216
      {
      }

217
      void fix_acceptance(const twa_graph_ptr& out)
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
        auto& acc = this->si->get_aut()->acc();
        if (!acc.is_generalized_buchi())
          throw std::runtime_error
            ("simplification of SCC acceptance works only with "
             "generalized Büchi acceptance");

        unsigned scc_count = this->si->scc_count();
        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
        for (unsigned n = 0; n < scc_count; ++n)
          {
            if (this->si->is_rejecting_scc(n))
              continue;
            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];
          }
        // 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)
          {
            if (this->si->is_rejecting_scc(n))
              continue;
            if (cnt[n] < max)
              strip_[n].remove_some(max - cnt[n]);
          }

        out->set_generalized_buchi(max);
252
253
      }

254
      filtered_trans trans(unsigned src, unsigned dst, bdd cond,
255
                           acc_cond::mark_t acc)
256
      {
257
258
259
260
261
262
263
264
265
266
267
268
269
270
        bool keep;
        std::tie(keep, cond, acc) =
          this->next_filter::trans(src, dst, cond, acc);

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

            if (this->si->is_rejecting_scc(u))
              acc = 0U;
            else
              acc = acc.strip(strip_[u]);
          }
        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
      unsigned in_n = aut->num_states();

281
      twa_graph_ptr filtered = make_twa_graph(aut->get_dict());
282
      filtered->copy_ap_of(aut);
283

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

290
      F filter(si, std::forward<Args>(args)...);
291
292

      // Renumber all useful states.
293
      unsigned out_n = 0;          // Number of output states.
294
295
296
      std::vector<unsigned> inout; // Associate old states to new ones.
      inout.reserve(in_n);
      for (unsigned i = 0; i < in_n; ++i)
297
        if (filter.state(i))
298
          inout.emplace_back(out_n++);
299
        else
300
          inout.emplace_back(-1U);
301

302
      filter.fix_acceptance(filtered);
303
      filtered->new_states(out_n);
304
      for (unsigned isrc = 0; isrc < in_n; ++isrc)
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
        {
          unsigned osrc = inout[isrc];
          if (osrc >= out_n)
            continue;
          for (auto& t: aut->out(isrc))
            {
              unsigned odst = inout[t.dst];
              if (odst >= out_n)
                continue;
              bool want;
              bdd cond;
              acc_cond::mark_t acc;
              std::tie(want, cond, acc) =
                filter.trans(isrc, t.dst, t.cond, t.acc);
              if (want)
                filtered->new_edge(osrc, odst, cond, acc);
            }
        }
323
      if (!given_si)
324
        delete si;
325
326
327
328
      // 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).
329
      auto init = inout[aut->get_init_state_number()];
330
      filtered->set_init_state(init < out_n ? init : filtered->new_state());
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358

      if (auto* names =
          aut->get_named_prop<std::vector<std::string>>("state-names"))
        {
          unsigned size = names->size();
          if (size > in_n)
            size = in_n;
          auto* new_names = new std::vector<std::string>(out_n);
          filtered->set_named_prop("state-names", new_names);
          for (unsigned s = 0; s < size; ++s)
            {
              unsigned new_s = inout[s];
              if (new_s != -1U)
                (*new_names)[new_s] = (*names)[s];
            }
        }
      if (auto hs =
          aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states"))
        {
          auto* new_hs = new std::map<unsigned, unsigned>;
          filtered->set_named_prop("highlight-states", new_hs);
          for (auto p: *hs)
            {
              unsigned new_s = inout[p.first];
              if (new_s != -1U)
                new_hs->emplace(new_s, p.second);
            }
        }
359
360
361
362
      return filtered;
    }
  }

363
  twa_graph_ptr
364
  scc_filter_states(const const_twa_graph_ptr& aut, bool remove_all_useless,
365
                    scc_info* given_si)
366
  {
367
368
369
    twa_graph_ptr res;
    if (remove_all_useless)
      res = scc_filter_apply<state_filter
370
                             <acc_filter_mask<true, true>>>(aut, given_si);
371
372
    else
      res = scc_filter_apply<state_filter
373
                             <acc_filter_mask<false, true>>>(aut, given_si);
374
    res->prop_copy(aut, { true, true, true, true });
375
    return res;
376
377
  }

378
379
  twa_graph_ptr
  scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless,
380
             scc_info* given_si)
381
  {
382
    twa_graph_ptr res;
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
383
    // acc_filter_simplify only works for generalized Büchi
384
385
    if (aut->acc().is_generalized_buchi())
      {
386
387
388
389
390
391
392
393
394
395
396
397
        if (remove_all_useless)
          res =
            scc_filter_apply<state_filter
                             <acc_filter_mask
                              <true, false,
                               acc_filter_simplify<>>>>(aut, given_si);
        else
          res =
            scc_filter_apply<state_filter
                             <acc_filter_mask
                              <false, false,
                               acc_filter_simplify<>>>>(aut, given_si);
398
      }
399
    else
400
      {
401
402
403
404
405
406
407
408
        if (remove_all_useless)
          res = scc_filter_apply<state_filter
                                 <acc_filter_mask
                                  <true, false>>>(aut, given_si);
        else
          res = scc_filter_apply<state_filter
                                 <acc_filter_mask
                                  <false, false>>>(aut, given_si);
409
      }
410
    res->merge_edges();
411
    res->prop_copy(aut,
412
413
414
415
416
                   { false,  // state-based acceptance is not preserved
                     true,
                     true,
                     true,
                   });
417
    return res;
418
419
  }

420
421
  twa_graph_ptr
  scc_filter_susp(const const_twa_graph_ptr& aut, bool remove_all_useless,
422
423
                  bdd suspvars, bdd ignoredvars, bool early_susp,
                  scc_info* given_si)
424
  {
425
    twa_graph_ptr res;
426
    if (remove_all_useless)
427
      res = scc_filter_apply<susp_filter
428
429
430
431
432
433
434
                             <state_filter
                              <acc_filter_mask
                               <true, false,
                                acc_filter_simplify<>>>>>(aut, given_si,
                                                          suspvars,
                                                          ignoredvars,
                                                          early_susp);
435
    else
436
      res = scc_filter_apply<susp_filter
437
438
439
440
441
442
443
                             <state_filter
                              <acc_filter_mask
                               <false, false,
                                acc_filter_simplify<>>>>>(aut, given_si,
                                                          suspvars,
                                                          ignoredvars,
                                                          early_susp);
444
    res->merge_edges();
445
    res->prop_copy(aut,
446
447
448
449
450
                   { false,  // state-based acceptance is not preserved
                     true,
                     false,  // determinism may not be preserved
                     false,  // stutter inv. of suspvars probably altered
                   });
451
    return res;
452
453
  }

454
}