ltlfilt.cc 19.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 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
#include "common_sys.hh"
21
22
23
24
25
26

#include <cstdlib>
#include <string>
#include <iostream>
#include <fstream>
#include <argp.h>
27
#include <cstring>
28
#include "error.h"
29

30
#include "common_setup.hh"
31
#include "common_finput.hh"
32
#include "common_output.hh"
33
#include "common_cout.hh"
34
#include "common_conv.hh"
35
#include "common_r.hh"
36

37
#include "misc/hash.hh"
38
39
40
41
42
43
44
45
#include "tl/simplify.hh"
#include "tl/length.hh"
#include "tl/relabel.hh"
#include "tl/unabbrev.hh"
#include "tl/remove_x.hh"
#include "tl/apcollect.hh"
#include "tl/exclusive.hh"
#include "tl/print.hh"
46
47
48
49
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/minimize.hh"
#include "twaalgos/safety.hh"
#include "twaalgos/stutter.hh"
50
51

const char argp_program_doc[] ="\
52
53
54
Read a list of formulas and output them back after some optional processing.\v\
Exit status:\n\
  0  if some formulas were output (skipped syntax errors do not count)\n\
55
  1  if no formulas were output (no match)\n\
56
  2  if any error has been reported";
57

58
enum {
59
  OPT_AP_N = 256,
60
61
62
63
  OPT_BOOLEAN,
  OPT_BOOLEAN_TO_ISOP,
  OPT_BSIZE_MAX,
  OPT_BSIZE_MIN,
64
  OPT_DEFINE,
65
66
  OPT_DROP_ERRORS,
  OPT_EQUIVALENT_TO,
67
  OPT_EXCLUSIVE_AP,
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
  OPT_EVENTUAL,
  OPT_GUARANTEE,
  OPT_IGNORE_ERRORS,
  OPT_IMPLIED_BY,
  OPT_IMPLY,
  OPT_LTL,
  OPT_NEGATE,
  OPT_NNF,
  OPT_OBLIGATION,
  OPT_RELABEL,
  OPT_RELABEL_BOOL,
  OPT_REMOVE_WM,
  OPT_REMOVE_X,
  OPT_SAFETY,
  OPT_SIZE_MAX,
  OPT_SIZE_MIN,
  OPT_SKIP_ERRORS,
  OPT_STUTTER_INSENSITIVE,
  OPT_SYNTACTIC_GUARANTEE,
  OPT_SYNTACTIC_OBLIGATION,
  OPT_SYNTACTIC_PERSISTENCE,
  OPT_SYNTACTIC_RECURRENCE,
  OPT_SYNTACTIC_SAFETY,
  OPT_SYNTACTIC_SI,
92
  OPT_UNABBREVIATE,
93
94
  OPT_UNIVERSAL,
};
95
96
97
98

static const argp_option options[] =
  {
    /**************************************************/
99
100
    { nullptr, 0, nullptr, 0, "Error handling:", 2 },
    { "skip-errors", OPT_SKIP_ERRORS, nullptr, 0,
101
      "output erroneous lines as-is without processing", 0 },
102
    { "drop-errors", OPT_DROP_ERRORS, nullptr, 0,
103
      "discard erroneous lines (default)", 0 },
104
    { "ignore-errors", OPT_IGNORE_ERRORS, nullptr, 0,
105
      "do not report syntax errors", 0 },
106
    /**************************************************/
107
108
109
110
    { nullptr, 0, nullptr, 0, "Transformation options:", 3 },
    { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 0 },
    { "nnf", OPT_NNF, nullptr, 0,
      "rewrite formulas in negative normal form", 0 },
111
112
113
    { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL,
      "relabel all atomic propositions, alphabetically unless " \
      "specified otherwise", 0 },
114
115
116
    { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL,
      "relabel Boolean subexpressions, alphabetically unless " \
      "specified otherwise", 0 },
117
    { "define", OPT_DEFINE, "FILENAME", OPTION_ARG_OPTIONAL,
118
119
      "when used with --relabel or --relabel-bool, output the relabeling map "
      "using #define statements", 0 },
120
    { "remove-wm", OPT_REMOVE_WM, nullptr, 0,
121
122
      "rewrite operators W and M using U and R (this is an alias for "
      "--unabbreviate=WM)", 0 },
123
    { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, nullptr, 0,
124
125
      "rewrite Boolean subformulas as irredundant sum of products "
      "(implies at least -r1)", 0 },
126
    { "remove-x", OPT_REMOVE_X, nullptr, 0,
127
128
      "remove X operators (valid only for stutter-insensitive properties)",
      0 },
129
130
    { "unabbreviate", OPT_UNABBREVIATE, "STR", OPTION_ARG_OPTIONAL,
      "remove all occurrences of the operators specified by STR, which "
131
132
133
      "must be a substring of \"eFGiMRW^\", where 'e', 'i', and '^' stand "
      "respectively for <->, ->, and xor.  If no argument is passed, "
      "the subset \"eFGiMW^\" is used.", 0 },
134
135
136
137
138
    { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
      "if any of those APs occur in the formula, add a term ensuring "
      "two of them may not be true at the same time.  Use this option "
      "multiple times to declare independent groups of exclusive "
      "propositions.", 0 },
139
140
    DECLARE_OPT_R,
    LEVEL_DOC(4),
141
    /**************************************************/
142
    { nullptr, 0, nullptr, 0,
143
      "Filtering options (matching is done after transformation):", 5 },
144
145
146
147
148
149
150
    { "ltl", OPT_LTL, nullptr, 0,
      "match only LTL formulas (no PSL operator)", 0 },
    { "boolean", OPT_BOOLEAN, nullptr, 0, "match Boolean formulas", 0 },
    { "eventual", OPT_EVENTUAL, nullptr, 0, "match pure eventualities", 0 },
    { "universal", OPT_UNIVERSAL, nullptr, 0,
      "match purely universal formulas", 0 },
    { "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0,
151
      "match syntactic-safety formulas", 0 },
152
    { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0,
153
      "match syntactic-guarantee formulas", 0 },
154
    { "syntactic-obligation", OPT_SYNTACTIC_OBLIGATION, nullptr, 0,
155
      "match syntactic-obligation formulas", 0 },
156
    { "syntactic-recurrence", OPT_SYNTACTIC_RECURRENCE, nullptr, 0,
157
      "match syntactic-recurrence formulas", 0 },
158
    { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, nullptr, 0,
159
      "match syntactic-persistence formulas", 0 },
160
    { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0,
161
      "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 },
162
163
    { "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "safety", OPT_SAFETY, nullptr, 0,
164
      "match safety formulas (even pathological)", 0 },
165
    { "guarantee", OPT_GUARANTEE, nullptr, 0,
166
      "match guarantee formulas (even pathological)", 0 },
167
    { "obligation", OPT_OBLIGATION, nullptr, 0,
168
169
170
171
172
173
174
175
176
      "match obligation formulas (even pathological)", 0 },
    { "size-max", OPT_SIZE_MAX, "INT", 0,
      "match formulas with size <= INT", 0 },
    { "size-min", OPT_SIZE_MIN, "INT", 0,
      "match formulas with size >= INT", 0 },
    { "bsize-max", OPT_BSIZE_MAX, "INT", 0,
      "match formulas with Boolean size <= INT", 0 },
    { "bsize-min", OPT_BSIZE_MIN, "INT", 0,
      "match formulas with Boolean size >= INT", 0 },
177
178
179
180
181
182
    { "implied-by", OPT_IMPLIED_BY, "FORMULA", 0,
      "match formulas implied by FORMULA", 0 },
    { "imply", OPT_IMPLY, "FORMULA", 0,
      "match formulas implying FORMULA", 0 },
    { "equivalent-to", OPT_EQUIVALENT_TO, "FORMULA", 0,
      "match formulas equivalent to FORMULA", 0 },
183
    { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, nullptr, 0,
184
      "match stutter-insensitive LTL formulas", 0 },
185
    { "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
186
187
    { "ap", OPT_AP_N, "N", 0,
      "match formulas which use exactly N atomic propositions", 0 },
188
189
    { "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
    { "unique", 'u', nullptr, 0,
190
      "drop formulas that have already been output (not affected by -v)", 0 },
191
    /**************************************************/
192
193
194
    { nullptr, 0, nullptr, 0, "Output options:", -20 },
    { "count", 'c', nullptr, 0, "print only a count of matched formulas", 0 },
    { "quiet", 'q', nullptr, 0, "suppress all normal output", 0 },
195
    { "max-count", 'n', "NUM", 0, "output at most NUM formulas", 0 },
196
    { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "\
197
      "the following interpreted sequences:", -19 },
198
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
199
      "the formula (in the selected syntax)", 0 },
200
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
201
      "the name of the input file", 0 },
202
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
203
      "the original line number in the input file", 0 },
204
    { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
205
206
      "the part of the line before the formula if it "
      "comes from a column extracted from a CSV file", 0 },
207
    { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
208
209
      "the part of the line after the formula if it "
      "comes from a column extracted from a CSV file", 0 },
210
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
211
      "a single %", 0 },
212
213
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
214
215
  };

216
217
const struct argp_child children[] =
  {
218
219
220
221
    { &finput_argp, 0, nullptr, 1 },
    { &output_argp, 0, nullptr, -20 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
222
223
  };

224
225
static bool one_match = false;

226
227
enum error_style_t { drop_errors, skip_errors };
static error_style_t error_style = drop_errors;
228
static bool ignore_errors = false;
229
230
static bool nnf = false;
static bool negate = false;
231
static bool boolean_to_isop = false;
232
233
234
235
236
237
238
239
240
241
242
243
static bool unique = false;
static bool psl = false;
static bool ltl = false;
static bool invert = false;
static bool boolean = false;
static bool universal = false;
static bool eventual = false;
static bool syntactic_safety = false;
static bool syntactic_guarantee = false;
static bool syntactic_obligation = false;
static bool syntactic_recurrence = false;
static bool syntactic_persistence = false;
244
static bool syntactic_si = false;
245
246
247
248
249
250
251
static bool safety = false;
static bool guarantee = false;
static bool obligation = false;
static int size_min = -1;
static int size_max = -1;
static int bsize_min = -1;
static int bsize_max = -1;
252
253
enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling };
static relabeling_mode relabeling = NoRelabeling;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
254
static spot::relabeling_style style = spot::Abc;
255
256
static bool remove_x = false;
static bool stutter_insensitive = false;
257
258
static bool ap = false;
static unsigned ap_n = 0;
259
static int opt_max_count = -1;
260
static long int match_count = 0;
261
static spot::exclusive_ap excl_ap;
262
static std::unique_ptr<output_file> output_define = nullptr;
263
static std::string unabbreviate;
264

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
265
266
267
static spot::formula implied_by = nullptr;
static spot::formula imply = nullptr;
static spot::formula equivalent_to = nullptr;
268

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
269
static spot::formula
270
271
parse_formula_arg(const std::string& input)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
272
273
274
  spot::parse_error_list pel;
  spot::formula f = parse_formula(input, pel);
  if (spot::format_parse_errors(std::cerr, input, pel))
275
    error(2, 0, "parse error when parsing an argument");
276
277
278
  return f;
}

279
static int
280
parse_opt(int key, char* arg, struct argp_state*)
281
282
283
284
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
285
286
287
    case 'c':
      output_format = count_output;
      break;
288
289
290
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
291
    case 'q':
292
      output_format = quiet_output;
293
      break;
294
295
    case OPT_R:
      parse_r(arg);
296
297
298
299
300
301
302
303
304
      break;
    case 'u':
      unique = true;
      break;
    case 'v':
      invert = true;
      break;
    case ARGP_KEY_ARG:
      // FIXME: use stat() to distinguish filename from string?
305
      jobs.emplace_back(arg, true);
306
307
308
309
      break;
    case OPT_BOOLEAN:
      boolean = true;
      break;
310
311
312
    case OPT_BOOLEAN_TO_ISOP:
      boolean_to_isop = true;
      break;
313
314
315
316
317
318
    case OPT_BSIZE_MIN:
      bsize_min = to_int(arg);
      break;
    case OPT_BSIZE_MAX:
      bsize_max = to_int(arg);
      break;
319
320
321
    case OPT_DEFINE:
      output_define.reset(new output_file(arg ? arg : "-"));
      break;
322
323
324
    case OPT_DROP_ERRORS:
      error_style = drop_errors;
      break;
325
326
327
    case OPT_EVENTUAL:
      eventual = true;
      break;
328
329
330
331
332
333
334
    case OPT_EQUIVALENT_TO:
      {
	if (equivalent_to)
	  error(2, 0, "only one --equivalent-to option can be given");
	equivalent_to = parse_formula_arg(arg);
	break;
      }
335
336
    case OPT_EXCLUSIVE_AP:
      excl_ap.add_group(arg);
337
      break;
338
339
340
    case OPT_GUARANTEE:
      guarantee = obligation = true;
      break;
341
342
343
    case OPT_IGNORE_ERRORS:
      ignore_errors = true;
      break;
344
345
    case OPT_IMPLIED_BY:
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346
	spot::formula i = parse_formula_arg(arg);
347
	// a→c∧b→c ≡ (a∨b)→c
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
348
	implied_by = spot::formula::Or({implied_by, i});
349
350
351
352
353
	break;
      }
    case OPT_IMPLY:
      {
	// a→b∧a→c ≡ a→(b∧c)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
354
355
	spot::formula i = parse_formula_arg(arg);
	imply = spot::formula::And({imply, i});
356
357
	break;
      }
358
359
360
    case OPT_LTL:
      ltl = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
361
362
363
    case OPT_NEGATE:
      negate = true;
      break;
364
365
366
367
368
369
    case OPT_NNF:
      nnf = true;
      break;
    case OPT_OBLIGATION:
      obligation = true;
      break;
370
    case OPT_RELABEL:
371
372
    case OPT_RELABEL_BOOL:
      relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling);
373
      if (!arg || !strncasecmp(arg, "abc", 6))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
374
	style = spot::Abc;
375
      else if (!strncasecmp(arg, "pnn", 4))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
376
	style = spot::Pnn;
377
      else
378
379
380
	error(2, 0, "invalid argument for --relabel%s: '%s'",
	      (key == OPT_RELABEL_BOOL ? "-bool" : ""),
	      arg);
381
      break;
382
    case OPT_REMOVE_WM:
383
      unabbreviate += "MW";
384
      break;
385
386
387
    case OPT_REMOVE_X:
      remove_x = true;
      break;
388
389
390
391
392
393
394
395
396
397
398
399
    case OPT_SAFETY:
      safety = obligation = true;
      break;
    case OPT_SIZE_MIN:
      size_min = to_int(arg);
      break;
    case OPT_SIZE_MAX:
      size_max = to_int(arg);
      break;
    case OPT_SKIP_ERRORS:
      error_style = skip_errors;
      break;
400
401
402
    case OPT_STUTTER_INSENSITIVE:
      stutter_insensitive = true;
      break;
403
404
405
406
    case OPT_UNABBREVIATE:
      if (arg)
	unabbreviate += arg;
      else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407
	unabbreviate += spot::default_unabbrev_string;
408
      break;
409
410
411
412
    case OPT_AP_N:
      ap = true;
      ap_n = to_int(arg);
      break;
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
    case OPT_SYNTACTIC_SAFETY:
      syntactic_safety = true;
      break;
    case OPT_SYNTACTIC_GUARANTEE:
      syntactic_guarantee = true;
      break;
    case OPT_SYNTACTIC_OBLIGATION:
      syntactic_obligation = true;
      break;
    case OPT_SYNTACTIC_RECURRENCE:
      syntactic_recurrence = true;
      break;
    case OPT_SYNTACTIC_PERSISTENCE:
      syntactic_persistence = true;
      break;
428
429
430
    case OPT_SYNTACTIC_SI:
      syntactic_si = true;
      break;
431
432
433
    case OPT_UNIVERSAL:
      universal = true;
      break;
434
435
436
437
438
439
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

440
typedef
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
441
std::unordered_set<spot::formula> fset_t;
442
443
444

namespace
{
445
  class ltl_processor: public job_processor
446
447
  {
  public:
448
    spot::tl_simplifier& simpl;
449
    fset_t unique_set;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
450
    spot::relabeling_map relmap;
451

452
    ltl_processor(spot::tl_simplifier& simpl)
453
      : simpl(simpl)
454
455
456
457
    {
    }

    int
458
    process_string(const std::string& input,
459
		    const char* filename = nullptr, int linenum = 0)
460
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
461
462
      spot::parse_error_list pel;
      spot::formula f = parse_formula(input, pel);
463
464
465

      if (!f || pel.size() > 0)
	  {
466
	    if (!ignore_errors)
467
468
	      {
		if (filename)
469
		  error_at_line(0, 0, filename, linenum, "parse error:");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
470
		spot::format_parse_errors(std::cerr, input, pel);
471
472
473
	      }

	    if (error_style == skip_errors)
474
475
476
	      std::cout << input << std::endl;
	    else
	      assert(error_style == drop_errors);
477
	    check_cout();
478
	    return !ignore_errors;
479
	  }
480
481
482
483
484
485
486
487
488
      try
	{
	  return process_formula(f, filename, linenum);
	}
      catch (const std::runtime_error& e)
	{
	  error_at_line(2, 0, filename, linenum, "%s", e.what());
	  SPOT_UNREACHABLE();
	}
489
    }
490

491
    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
492
    process_formula(spot::formula f,
493
		    const char* filename = nullptr, int linenum = 0)
494
    {
495
      if (opt_max_count >= 0 && match_count >= opt_max_count)
496
497
498
499
500
	{
	  abort_run = true;
	  return 0;
	}

501
      if (negate)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
502
	f = spot::formula::Not(f);
503

504
505
506
507
      if (remove_x)
	{
	  // If simplification are enabled, we do them before and after.
	  if (simplification_level)
508
	    f = simpl.simplify(f);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
509
	  f = spot::remove_x(f);
510
511
	}

512
      if (simplification_level || boolean_to_isop)
513
	f = simpl.simplify(f);
514
515

      if (nnf)
516
	f = simpl.negative_normal_form(f);
517

518
      switch (relabeling)
519
	{
520
521
	case ApRelabeling:
	  {
522
	    relmap.clear();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
523
	    f = spot::relabel(f, style, &relmap);
524
525
526
527
	    break;
	  }
	case BseRelabeling:
	  {
528
	    relmap.clear();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
529
	    f = spot::relabel_bse(f, style, &relmap);
530
531
532
533
	    break;
	  }
	case NoRelabeling:
	  break;
534
535
	}

536
      if (!unabbreviate.empty())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
537
	f = spot::unabbreviate(f, unabbreviate.c_str());
538

539
      if (!excl_ap.empty())
540
	f = excl_ap.constrain(f);
541

542
543
      bool matched = true;

544
545
546
547
548
549
550
551
552
553
554
      matched &= !ltl || f.is_ltl_formula();
      matched &= !psl || f.is_psl_formula();
      matched &= !boolean || f.is_boolean();
      matched &= !universal || f.is_universal();
      matched &= !eventual || f.is_eventual();
      matched &= !syntactic_safety || f.is_syntactic_safety();
      matched &= !syntactic_guarantee || f.is_syntactic_guarantee();
      matched &= !syntactic_obligation || f.is_syntactic_obligation();
      matched &= !syntactic_recurrence || f.is_syntactic_recurrence();
      matched &= !syntactic_persistence || f.is_syntactic_persistence();
      matched &= !syntactic_si || f.is_syntactic_stutter_invariant();
555
      matched &= !ap || atomic_prop_collect(f)->size() == ap_n;
556
557
558

      if (matched && (size_min > 0 || size_max >= 0))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
559
	  int l = spot::length(f);
560
561
562
563
564
565
	  matched &= (size_min <= 0) || (l >= size_min);
	  matched &= (size_max < 0) || (l <= size_max);
	}

      if (matched && (bsize_min > 0 || bsize_max >= 0))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
566
	  int l = spot::length_boolone(f);
567
568
569
570
	  matched &= (bsize_min <= 0) || (l >= bsize_min);
	  matched &= (bsize_max < 0) || (l <= bsize_max);
	}

571
572
573
      matched &= !implied_by || simpl.implication(implied_by, f);
      matched &= !imply || simpl.implication(f, imply);
      matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to);
574
      matched &= !stutter_insensitive || spot::is_stutter_invariant(f);
575

576
577
578
579
580
581
      // Match obligations and subclasses using WDBA minimization.
      // Because this is costly, we compute it later, so that we don't
      // have to compute it on formulas that have been discarded for
      // other reasons.
      if (matched && obligation)
	{
582
583
	  auto aut = ltl_to_tgba_fm(f, simpl.get_dict());
	  auto min = minimize_obligation(aut, f);
584
585
586
587
588
589
590
591
	  assert(min);
	  if (aut == min)
	    {
	      // Not an obligation
	      matched = false;
	    }
	  else
	    {
592
	      matched &= !guarantee || is_terminal_automaton(min);
593
594
595
596
597
598
	      matched &= !safety || is_safety_mwdba(min);
	    }
	}

      matched ^= invert;

599
600
      if (unique && !unique_set.insert(f).second)
	matched = false;
601
602
603

      if (matched)
	{
604
605
606
607
608
	  if (output_define
	      && output_format != count_output
	      && output_format != quiet_output)
	    {
	      // Sort the formulas alphabetically.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
609
	      std::map<std::string, spot::formula> m;
610
	      for (auto& p: relmap)
611
		m.emplace(str_psl(p.first), p.second);
612
613
614
615
616
	      for (auto& p: m)
		stream_formula(output_define->ostream()
			       << "#define " << p.first << " (",
			       p.second, filename, linenum) << ")\n";
	    }
617
	  one_match = true;
618
	  output_formula_checked(f, filename, linenum, prefix, suffix);
619
	  ++match_count;
620
621
622
623
624
625
626
627
628
	}
      return 0;
    }
  };
}

int
main(int argc, char** argv)
{
629
  setup(argv);
630

631
  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
632
		    argp_program_doc, children, nullptr, nullptr };
633

634
635
  try
    {
636
      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
637
638
639
640
641
642
643
	exit(err);

      if (jobs.empty())
	jobs.emplace_back("-", 1);

      if (boolean_to_isop && simplification_level == 0)
	simplification_level = 1;
644
      spot::tl_simplifier_options opt(simplification_level);
645
      opt.boolean_to_isop = boolean_to_isop;
646
      spot::tl_simplifier simpl(opt);
647

648
649
650
651
652
653
654
655
      ltl_processor processor(simpl);
      if (processor.run())
	return 2;
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
656
657
658
659
  catch (const std::invalid_argument& e)
    {
      error(2, 0, "%s", e.what());
    }
660
661
662
663

  if (output_format == count_output)
    std::cout << match_count << std::endl;

664
  return one_match ? 0 : 1;
665
}