postproc.cc 15.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// 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
23
24
25
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/stripacc.hh>
26
#include <cstdlib>
27
28
29
30
31
32
33
34
35
#include <spot/misc/optionmap.hh>
#include <spot/twaalgos/powerset.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/dtbasat.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sepsets.hh>
36
#include <spot/twaalgos/determinize.hh>
37
#include <spot/twaalgos/alternation.hh>
38
39
40

namespace spot
{
41
42
  namespace
  {
43
44
    static twa_graph_ptr
    ensure_ba(twa_graph_ptr& a)
45
    {
46
      if (a->num_sets() == 0)
47
48
49
50
51
        {
          auto m = a->set_buchi();
          for (auto& t: a->edges())
            t.acc = m;
        }
52
53
54
      return a;
    }
  }
55

56
57
58
59
  postprocessor::postprocessor(const option_map* opt)
  {
    if (opt)
      {
60
61
62
63
64
65
66
67
68
69
70
71
        degen_order_ = opt->get("degen-order", 0);
        degen_reset_ = opt->get("degen-reset", 1);
        degen_cache_ = opt->get("degen-lcache", 1);
        degen_lskip_ = opt->get("degen-lskip", 1);
        degen_lowinit_ = opt->get("degen-lowinit", 0);
        det_scc_ = opt->get("det-scc", 1);
        det_simul_ = opt->get("det-simul", 1);
        det_stutter_ = opt->get("det-stutter", 1);
        simul_ = opt->get("simul", -1);
        scc_filter_ = opt->get("scc-filter", -1);
        ba_simul_ = opt->get("ba-simul", -1);
        tba_determinisation_ = opt->get("tba-det", 0);
72
        incr_ = opt->get("incr", 0);
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
        sat_minimize_ = opt->get("sat-minimize", 0);
        sat_acc_ = opt->get("sat-acc", 0);
        sat_states_ = opt->get("sat-states", 0);
        state_based_ = opt->get("state-based", 0);
        wdba_minimize_ = opt->get("wdba-minimize", 1);

        if (sat_acc_ && sat_minimize_ == 0)
          sat_minimize_ = 1;        // 2?
        if (sat_states_ && sat_minimize_ == 0)
          sat_minimize_ = 1;
        if (sat_minimize_)
          {
            tba_determinisation_ = 1;
            if (sat_acc_ <= 0)
              sat_acc_ = -1;
            if (sat_states_ <= 0)
              sat_states_ = -1;
          }
91
92
93
      }
  }

94
95
  twa_graph_ptr
  postprocessor::do_simul(const twa_graph_ptr& a, int opt)
96
  {
97
98
    if (!has_separate_sets(a))
      return a;
99
    switch (opt)
100
101
      {
      case 0:
102
        return a;
103
      case 1:
104
        return simulation(a);
105
      case 2:
106
        return cosimulation(a);
107
108
      case 3:
      default:
109
        return iterated_simulations(a);
110
111
112
      }
  }

113
  twa_graph_ptr
114
  postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt)
115
  {
116
117
    if (ba_simul_ <= 0)
      return a;
118
119
120
    switch (opt)
      {
      case 0:
121
        return a;
122
      case 1:
123
        return simulation_sba(a);
124
      case 2:
125
        return cosimulation_sba(a);
126
127
      case 3:
      default:
128
        return iterated_simulations_sba(a);
129
130
131
      }
  }

132
133
  twa_graph_ptr
  postprocessor::do_degen(const twa_graph_ptr& a)
134
  {
135
    auto d = degeneralize(a,
136
137
138
                          degen_reset_, degen_order_,
                          degen_cache_, degen_lskip_,
                          degen_lowinit_);
139
    return do_sba_simul(d, ba_simul_);
140
141
  }

142
143
144
145
146
  twa_graph_ptr
  postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg)
  {
    if (scc_filter_ == 0)
      return a;
147
148
    // If the automaton is weak, using transition-based acceptance
    // won't help, so let's preserve it.
149
    if ((state_based_ || a->prop_inherently_weak().is_true())
150
        && a->prop_state_acc().is_true())
151
      return scc_filter_states(a, arg);
152
153
154
155
156
157
158
159
160
161
    else
      return scc_filter(a, arg);
  }

  twa_graph_ptr
  postprocessor::do_scc_filter(const twa_graph_ptr& a)
  {
    return do_scc_filter(a, scc_filter_ > 1);
  }

162
163
#define PREF_ (pref_ & (Small | Deterministic))
#define COMP_ (pref_ & Complete)
164
#define SBACC_ (pref_ & SBAcc)
165

166
  twa_graph_ptr
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
167
  postprocessor::run(twa_graph_ptr a, formula f)
168
  {
169
170
171
172
173
174
175
176
177
    if (simul_ < 0)
      simul_ = (level_ == Low) ? 1 : 3;
    if (ba_simul_ < 0)
      ba_simul_ = (level_ == High) ? 3 : 0;
    if (scc_filter_ < 0)
      scc_filter_ = 1;
    if (type_ == BA || SBACC_)
      state_based_ = true;

178
179
180
181
182
183
184
185
    if (a->is_alternating() &&
        // We will probably have to revisit this condition later.
        // Currently, the intent is that postprocessor should never
        // return an alternating automaton, unless it is called with
        // its laxest settings.
        !(type_ == Generic && PREF_ == Any && level_ == Low))
      a = remove_alternation(a);

186
    if (type_ != Generic && !a->acc().is_generalized_buchi())
187
      {
188
189
190
        a = to_generalized_buchi(a);
        if (PREF_ == Any && level_ == Low)
          a = do_scc_filter(a, true);
191
      }
192

193
    if (PREF_ == Any && level_ == Low
194
195
196
197
        && (type_ == Generic
            || type_ == TGBA
            || (type_ == BA && a->is_sba())
            || (type_ == Monitor && a->num_sets() == 0)))
198
      {
199
200
201
202
203
        if (COMP_)
          a = complete(a);
        if (SBACC_)
          a = sbacc(a);
        return a;
204
      }
205

206
    int original_acc = a->num_sets();
207

208
    // Remove useless SCCs.
209
    if (type_ == Monitor)
210
211
212
      // Do not bother about acceptance conditions, they will be
      // ignored.
      a = scc_filter_states(a);
213
    else
214
      a = do_scc_filter(a, (PREF_ == Any));
215

216
217
    if (type_ == Monitor)
      {
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
        if (PREF_ == Deterministic)
          a = minimize_monitor(a);
        else
          strip_acceptance_here(a);

        if (PREF_ == Any)
          return a;

        a = do_simul(a, simul_);

        // For Small,High we return the smallest between the output of
        // the simulation, and that of the deterministic minimization.
        if (PREF_ == Small && level_ == High && simul_)
          {
            auto m = minimize_monitor(a);
            if (m->num_states() < a->num_states())
              a = m;
          }
236
        a->remove_unused_ap();
237
238
239
        if (COMP_)
          a = complete(a);
        return a;
240
241
      }

242
    if (PREF_ == Any)
243
      {
244
245
246
247
248
249
250
        if (type_ == BA)
          a = do_degen(a);
        if (COMP_)
          a = complete(a);
        if (SBACC_)
          a = sbacc(a);
        return a;
251
252
      }

253
    bool dba_is_wdba = false;
254
    bool dba_is_minimal = false;
255
256
    twa_graph_ptr dba = nullptr;
    twa_graph_ptr sim = nullptr;
257
258
259

    // (Small,Low) is the only configuration where we do not run
    // WDBA-minimization.
260
    if ((PREF_ != Small || level_ != Low) && wdba_minimize_)
261
      {
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
        bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
        dba = minimize_obligation(a, f, nullptr, reject_bigger);
        if (dba
            && dba->prop_inherently_weak().is_true()
            && dba->prop_deterministic().is_true())
          {
            // The WDBA is a BA, so no degeneralization is required.
            // We just need to add an acceptance set if there is none.
            dba_is_minimal = dba_is_wdba = true;
            if (type_ == BA)
              ensure_ba(dba);
          }
        else
          {
            // Minimization failed.
            dba = nullptr;
          }
279
280
281
282
      }

    // Run a simulation when wdba failed (or was not run), or
    // at hard levels if we want a small output.
283
    if (!dba || (level_ == High && PREF_ == Small))
284
      {
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
        if (((SBACC_ && a->prop_state_acc().is_true())
             || (type_ == BA && a->is_sba()))
            && !tba_determinisation_)
          {
            sim = do_sba_simul(a, ba_simul_);
          }
        else
          {
            sim = do_simul(a, simul_);
            // Degeneralize the result of the simulation if needed.
            // No need to do that if tba_determinisation_ will be used.
            if (type_ == BA && !tba_determinisation_)
              sim = do_degen(sim);
            else if (SBACC_ && !tba_determinisation_)
              sim = sbacc(sim);
          }
301
302
      }

303
304
305
306
    // If WDBA failed, but the simulation returned a deterministic
    // automaton, use it as dba.
    assert(dba || sim);
    if (!dba && is_deterministic(sim))
307
      {
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
        std::swap(sim, dba);
        // We postponed degeneralization above i case we would need
        // to perform TBA-determinisation, but now it is clear
        // that we won't perform it.  So do degeneralize.
        if (tba_determinisation_)
          {
            if (type_ == BA)
              {
                dba = do_degen(dba);
                assert(is_deterministic(dba));
              }
            else if (SBACC_)
              {
                dba = sbacc(dba);
                assert(is_deterministic(dba));
              }
          }
325
      }
326
327
328

    // If we don't have a DBA, attempt tba-determinization if requested.
    if (tba_determinisation_ && !dba)
329
      {
330
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
359
360
361
362
363
364
365
366
367
368
369
370
371
372
        twa_graph_ptr tmpd = nullptr;
        if (PREF_ == Deterministic
            && f
            && f.is_syntactic_recurrence()
            && sim->num_sets() > 1)
          tmpd = degeneralize_tba(sim);

        auto in = tmpd ? tmpd : sim;

        // These thresholds are arbitrary.
        //
        // For producing Small automata, we assume that a
        // deterministic automaton that is twice the size of the
        // original will never get reduced to a smaller one.  We also
        // do not want more than 2^13 cycles in an SCC.
        //
        // For Deterministic automata, we accept automata that
        // are 8 times bigger, with no more that 2^15 cycle per SCC.
        // The cycle threshold is the most important limit here.  You
        // may up it if you want to try producing larger automata.
        auto tmp =
          tba_determinize_check(in,
                                (PREF_ == Small) ? 2 : 8,
                                1 << ((PREF_ == Small) ? 13 : 15),
                                f);
        if (tmp && tmp != in)
          {
            // There is no point in running the reverse simulation on
            // a deterministic automaton, since all prefixes are
            // unique.
            dba = simulation(tmp);
          }
        if (dba && PREF_ == Deterministic)
          {
            // disregard the result of the simulation.
            sim = nullptr;
          }
        else
          {
            // degeneralize sim, because we did not do it earlier
            if (type_ == BA)
              sim = do_degen(sim);
          }
373
374
      }

375
376
    if (PREF_ == Deterministic && type_ == Generic && !dba)
      {
377
378
379
380
381
        dba = tgba_determinize(to_generalized_buchi(sim),
                               false, det_scc_, det_simul_, det_stutter_);
        if (level_ != Low)
          dba = simulation(dba);
        sim = nullptr;
382
383
      }

384
385
386
    // Now dba contains either the result of WDBA-minimization (in
    // that case dba_is_wdba=true), or some deterministic automaton
    // that is either the result of the simulation or of the
387
388
389
390
    // TBA-determinization (dba_is_wdba=false in both cases), or a
    // parity automaton coming from tgba_determinize().  If the dba is
    // a WDBA, we do not have to run SAT-minimization.  A negative
    // value in sat_minimize_ can force its use for debugging.
391
    if (sat_minimize_ && dba && (!dba_is_wdba || sat_minimize_ < 0))
392
      {
393
394
        if (type_ == Generic)
          throw std::runtime_error
395
            ("postproc() not yet updated to mix sat-minimize and Generic");
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
        unsigned target_acc;
        if (type_ == BA)
          target_acc = 1;
        else if (sat_acc_ != -1)
          target_acc = sat_acc_;
        else
          // Take the number of acceptance conditions from the input
          // automaton, not from dba, because dba often has been
          // degeneralized by tba_determinize_check().  Make sure it
          // is at least 1.
          target_acc = original_acc > 0 ? original_acc : 1;

        const_twa_graph_ptr in = nullptr;
        if (target_acc == 1)
          {
            // If we are seeking a minimal DBA with unknown number of
            // states, then we should start from the degeneralized,
            // because the input TBA might be smaller.
            if (state_based_)
              in = degeneralize(dba);
            else
              in = degeneralize_tba(dba);
          }
        else
          {
            in = dba;
          }

        twa_graph_ptr res = complete(in);
        if (target_acc == 1)
          {
            if (sat_states_ != -1)
              res = dtba_sat_synthetize(res, sat_states_, state_based_);
            else if (sat_minimize_ == 1 || sat_minimize_ == -1)
              res = dtba_sat_minimize(res, state_based_);
431
            else if (sat_minimize_ == 2)
432
              res = dtba_sat_minimize_dichotomy(res, state_based_);
433
434
            else // sat_minimize_ = 3
              res = dtba_sat_minimize_incr(res, state_based_, -1, incr_);
435
436
437
438
439
440
441
442
443
444
445
446
447
          }
        else
          {
            if (sat_states_ != -1)
              res = dtwa_sat_synthetize
                (res, target_acc,
                 acc_cond::acc_code::generalized_buchi(target_acc),
                 sat_states_, state_based_);
            else if (sat_minimize_ == 1 || sat_minimize_ == -1)
              res = dtwa_sat_minimize
                (res, target_acc,
                 acc_cond::acc_code::generalized_buchi(target_acc),
                 state_based_);
448
            else if (sat_minimize_ == 2)
449
450
451
452
              res = dtwa_sat_minimize_dichotomy
                (res, target_acc,
                 acc_cond::acc_code::generalized_buchi(target_acc),
                 state_based_);
453
454
455
456
457
458
            else // sat_minimize_ = 3
              res = dtwa_sat_minimize_incr
                (res, target_acc,
                 acc_cond::acc_code::generalized_buchi(target_acc),
                 state_based_, -1, false, incr_);
        }
459
460
461
462
463
464

        if (res)
          {
            dba = do_scc_filter(res, true);
            dba_is_minimal = true;
          }
465
466
      }

467
468
469
    // Degeneralize the dba resulting from tba-determinization or
    // sat-minimization (which is a TBA) if requested and needed.
    if (dba && !dba_is_wdba && type_ == BA
470
        && !(dba_is_minimal && state_based_ && dba->num_sets() == 1))
471
      dba = degeneralize(dba);
472
473
474

    if (dba && sim)
      {
475
476
477
478
        if (dba->num_states() > sim->num_states())
          dba = nullptr;
        else
          sim = nullptr;
479
480
      }

481
    if (level_ == High && scc_filter_ != 0)
482
      {
483
484
485
486
487
488
489
490
491
492
493
494
        if (dba)
          {
            // Do that even for WDBA, to remove marks from transitions
            // leaving trivial SCCs.
            dba = do_scc_filter(dba, true);
            assert(!sim);
          }
        else if (sim)
          {
            sim = do_scc_filter(sim, true);
            assert(!dba);
          }
495
      }
496
497
498

    sim = dba ? dba : sim;

499
500
    sim->remove_unused_ap();

501
    if (COMP_)
502
      sim = complete(sim);
503
504
    if (SBACC_)
      sim = sbacc(sim);
505

506
    return sim;
507
508
  }
}