postproc.cc 12.6 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
38
39

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

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

	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;
	  }
89
90
91
      }
  }

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

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

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

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

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

164
  twa_graph_ptr
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
165
  postprocessor::run(twa_graph_ptr a, formula f)
166
  {
167
168
169
170
171
172
173
174
175
    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;

176
    if (type_ != Generic && !a->acc().is_generalized_buchi())
177
178
      {
	a = to_generalized_buchi(a);
179
180
	if (PREF_ == Any && level_ == Low)
	  a = do_scc_filter(a, true);
181
      }
182

183
184
185
186
187
188
189
190
191
192
193
194
    if (PREF_ == Any && level_ == Low
	&& (type_ == Generic
	    || type_ == TGBA
	    || (type_ == BA && a->is_sba())
	    || (type_ == Monitor && a->num_sets() == 0)))
      {
	if (COMP_)
	  a = complete(a);
	if (SBACC_)
	  a = sbacc(a);
	return a;
      }
195

196
    int original_acc = a->num_sets();
197

198
    // Remove useless SCCs.
199
    if (type_ == Monitor)
200
201
202
      // Do not bother about acceptance conditions, they will be
      // ignored.
      a = scc_filter_states(a);
203
    else
204
      a = do_scc_filter(a, (PREF_ == Any));
205

206
207
    if (type_ == Monitor)
      {
208
	if (PREF_ == Deterministic)
209
	  a = minimize_monitor(a);
210
	else
211
212
	  strip_acceptance_here(a);

213
	if (PREF_ == Any)
214
215
	  return a;

216
217
	a = do_simul(a, simul_);

218
219
	// For Small,High we return the smallest between the output of
	// the simulation, and that of the deterministic minimization.
220
	if (PREF_ == Small && level_ == High && simul_)
221
	  {
222
223
224
	    auto m = minimize_monitor(a);
	    if (m->num_states() < a->num_states())
	      a = m;
225
	  }
226
	if (COMP_)
227
	  a = complete(a);
228
	return a;
229
230
      }

231
    if (PREF_ == Any)
232
233
      {
	if (type_ == BA)
234
	  a = do_degen(a);
235
	if (COMP_)
236
	  a = complete(a);
237
238
	if (SBACC_)
	  a = sbacc(a);
239
240
241
	return a;
      }

242
    bool dba_is_wdba = false;
243
    bool dba_is_minimal = false;
244
245
    twa_graph_ptr dba = nullptr;
    twa_graph_ptr sim = nullptr;
246
247
248

    // (Small,Low) is the only configuration where we do not run
    // WDBA-minimization.
249
    if ((PREF_ != Small || level_ != Low) && wdba_minimize_)
250
      {
251
	bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
252
	dba = minimize_obligation(a, f, nullptr, reject_bigger);
253
254
255
	if (dba
	    && dba->prop_inherently_weak().is_true()
	    && dba->prop_deterministic().is_true())
256
257
258
259
260
261
262
	  {
	    // 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);
	  }
263
	else
264
265
266
267
	  {
	    // Minimization failed.
	    dba = nullptr;
	  }
268
269
270
271
      }

    // Run a simulation when wdba failed (or was not run), or
    // at hard levels if we want a small output.
272
    if (!dba || (level_ == High && PREF_ == Small))
273
      {
274
	if (((SBACC_ && a->prop_state_acc().is_true())
275
276
	     || (type_ == BA && a->is_sba()))
	    && !tba_determinisation_)
277
	  {
278
	    sim = do_sba_simul(a, ba_simul_);
279
280
281
282
283
284
285
286
	  }
	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);
287
288
	    else if (SBACC_ && !tba_determinisation_)
	      sim = sbacc(sim);
289
	  }
290
291
      }

292
293
294
295
    // If WDBA failed, but the simulation returned a deterministic
    // automaton, use it as dba.
    assert(dba || sim);
    if (!dba && is_deterministic(sim))
296
297
298
299
300
      {
	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.
301
	if (tba_determinisation_)
302
	  {
303
304
305
306
307
308
309
310
311
312
	    if (type_ == BA)
	      {
		dba = do_degen(dba);
		assert(is_deterministic(dba));
	      }
	    else if (SBACC_)
	      {
		dba = sbacc(dba);
		assert(is_deterministic(dba));
	      }
313
314
	  }
      }
315
316
317

    // If we don't have a DBA, attempt tba-determinization if requested.
    if (tba_determinisation_ && !dba)
318
      {
319
	twa_graph_ptr tmpd = nullptr;
320
	if (PREF_ == Deterministic
321
	    && f
322
	    && f.is_syntactic_recurrence()
323
	    && sim->num_sets() > 1)
324
	  tmpd = degeneralize_tba(sim);
325

326
	auto in = tmpd ? tmpd : sim;
327

328
	// These thresholds are arbitrary.
329
330
331
332
333
334
335
336
337
338
	//
	// 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.
339
	auto tmp =
340
	  tba_determinize_check(in,
341
342
				(PREF_ == Small) ? 2 : 8,
				1 << ((PREF_ == Small) ? 13 : 15),
343
				f);
344
	if (tmp && tmp != in)
345
346
347
348
	  {
	    // There is no point in running the reverse simulation on
	    // a deterministic automaton, since all prefixes are
	    // unique.
349
	    dba = simulation(tmp);
350
	  }
351
	if (dba && PREF_ == Deterministic)
352
353
	  {
	    // disregard the result of the simulation.
354
	    sim = nullptr;
355
	  }
356
357
358
359
360
361
	else
	  {
	    // degeneralize sim, because we did not do it earlier
	    if (type_ == BA)
	      sim = do_degen(sim);
	  }
362
363
      }

364
365
    if (PREF_ == Deterministic && type_ == Generic && !dba)
      {
366
367
	dba = tgba_determinize(to_generalized_buchi(sim),
			       false, det_scc_, det_simul_, det_stutter_);
368
369
370
371
372
	if (level_ != Low)
	  dba = simulation(dba);
	sim = nullptr;
      }

373
374
375
    // 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
376
377
378
379
    // 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.
380
    if (sat_minimize_ && dba && (!dba_is_wdba || sat_minimize_ < 0))
381
      {
382
383
384
	if (type_ == Generic)
	  throw std::runtime_error
	    ("postproc() no yet updated to mix sat-minimize and Generic");
385
386
387
388
389
390
391
	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
392
	  // automaton, not from dba, because dba often has been
393
394
	  // degeneralized by tba_determinize_check().  Make sure it
	  // is at least 1.
395
	  target_acc = original_acc > 0 ? original_acc : 1;
396

397
	const_twa_graph_ptr in = nullptr;
398
	if (target_acc == 1)
399
400
401
402
	  {
	    // 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.
403
	    if (state_based_)
404
	      in = degeneralize(dba);
405
	    else
406
	      in = degeneralize_tba(dba);
407
408
409
410
	  }
	else
	  {
	    in = dba;
411
	  }
412

413
	twa_graph_ptr res = complete(in);
414
	if (target_acc == 1)
415
	  {
416
	    if (sat_states_ != -1)
417
	      res = dtba_sat_synthetize(res, sat_states_, state_based_);
418
	    else if (sat_minimize_ == 1 || sat_minimize_ == -1)
419
	      res = dtba_sat_minimize(res, state_based_);
420
	    else  // sat_minimize_ == 2
421
	      res = dtba_sat_minimize_dichotomy(res, state_based_);
422
423
424
425
	  }
	else
	  {
	    if (sat_states_ != -1)
426
	      res = dtwa_sat_synthetize
427
428
		(res, target_acc,
		 acc_cond::acc_code::generalized_buchi(target_acc),
429
		 sat_states_, state_based_);
430
	    else if (sat_minimize_ == 1 || sat_minimize_ == -1)
431
	      res = dtwa_sat_minimize
432
433
		(res, target_acc,
		 acc_cond::acc_code::generalized_buchi(target_acc),
434
		 state_based_);
435
	    else  // sat_minimize_ == 2
436
	      res = dtwa_sat_minimize_dichotomy
437
438
		(res, target_acc,
		 acc_cond::acc_code::generalized_buchi(target_acc),
439
		 state_based_);
440
	  }
441
442

	if (res)
443
	  {
444
	    dba = do_scc_filter(res, true);
445
	    dba_is_minimal = true;
446
447
448
	  }
      }

449
450
451
    // 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
452
	&& !(dba_is_minimal && state_based_ && dba->num_sets() == 1))
453
      dba = degeneralize(dba);
454
455
456

    if (dba && sim)
      {
457
	if (dba->num_states() > sim->num_states())
458
	  dba = nullptr;
459
	else
460
	  sim = nullptr;
461
462
      }

463
    if (level_ == High && scc_filter_ != 0)
464
      {
465
	if (dba)
466
	  {
467
468
	    // Do that even for WDBA, to remove marks from transitions
	    // leaving trivial SCCs.
469
	    dba = do_scc_filter(dba, true);
470
	    assert(!sim);
471
472
473
	  }
	else if (sim)
	  {
474
	    sim = do_scc_filter(sim, true);
475
	    assert(!dba);
476
	  }
477
      }
478
479
480

    sim = dba ? dba : sim;

481
    if (COMP_)
482
      sim = complete(sim);
483
484
    if (SBACC_)
      sim = sbacc(sim);
485

486
    return sim;
487
488
  }
}