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
  }
}