ltlfilt.cc 20.1 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 38 39
#include "misc/hash.hh"
#include "ltlvisit/simplify.hh"
#include "ltlvisit/length.hh"
40
#include "ltlvisit/relabel.hh"
41
#include "ltlvisit/wmunabbrev.hh"
42
#include "ltlvisit/remove_x.hh"
43
#include "ltlvisit/apcollect.hh"
44
#include "ltlvisit/exclusive.hh"
45
#include "ltlvisit/tostring.hh"
46
#include "ltlast/unop.hh"
47
#include "ltlast/multop.hh"
48 49 50
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/safety.hh"
51
#include "tgbaalgos/stutter.hh"
52 53

const char argp_program_doc[] ="\
54 55 56
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\
57
  1  if no formulas were output (no match)\n\
58
  2  if any error has been reported";
59

60
enum {
61
  OPT_AP_N = 256,
62 63 64 65
  OPT_BOOLEAN,
  OPT_BOOLEAN_TO_ISOP,
  OPT_BSIZE_MAX,
  OPT_BSIZE_MIN,
66
  OPT_DEFINE,
67 68
  OPT_DROP_ERRORS,
  OPT_EQUIVALENT_TO,
69
  OPT_EXCLUSIVE_AP,
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
  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,
  OPT_UNIVERSAL,
};
96 97 98 99 100 101 102 103 104

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Error handling:", 2 },
    { "skip-errors", OPT_SKIP_ERRORS, 0, 0,
      "output erroneous lines as-is without processing", 0 },
    { "drop-errors", OPT_DROP_ERRORS, 0, 0,
      "discard erroneous lines (default)", 0 },
105 106
    { "ignore-errors", OPT_IGNORE_ERRORS, 0, 0,
      "do not report syntax errors", 0 },
107 108
    /**************************************************/
    { 0, 0, 0, 0, "Transformation options:", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
    { "negate", OPT_NEGATE, 0, 0, "negate each formula", 0 },
110
    { "nnf", OPT_NNF, 0, 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 118 119
    { "define", OPT_DEFINE, "[FILENAME]", OPTION_ARG_OPTIONAL,
      "when used with --relabel or --relabel-bool, output the relabeling map "
      "using #define statements", 0 },
120 121
    { "remove-wm", OPT_REMOVE_WM, 0, 0,
      "rewrite operators W and M using U and R", 0 },
122 123 124
    { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0,
      "rewrite Boolean subformulas as irredundant sum of products "
      "(implies at least -r1)", 0 },
125 126 127
    { "remove-x", OPT_REMOVE_X, 0, 0,
      "remove X operators (valid only for stutter-insensitive properties)",
      0 },
128 129 130 131 132
    { "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 },
133 134
    DECLARE_OPT_R,
    LEVEL_DOC(4),
135 136 137
    /**************************************************/
    { 0, 0, 0, 0,
      "Filtering options (matching is done after transformation):", 5 },
138
    { "ltl", OPT_LTL, 0, 0, "match only LTL formulas (no PSL operator)", 0 },
139 140 141 142 143 144 145 146 147 148 149 150 151
    { "boolean", OPT_BOOLEAN, 0, 0, "match Boolean formulas", 0 },
    { "eventual", OPT_EVENTUAL, 0, 0, "match pure eventualities", 0 },
    { "universal", OPT_UNIVERSAL, 0, 0, "match purely universal formulas", 0 },
    { "syntactic-safety", OPT_SYNTACTIC_SAFETY, 0, 0,
      "match syntactic-safety formulas", 0 },
    { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, 0, 0,
      "match syntactic-guarantee formulas", 0 },
    { "syntactic-obligation", OPT_SYNTACTIC_OBLIGATION, 0, 0,
      "match syntactic-obligation formulas", 0 },
    { "syntactic-recurrence", OPT_SYNTACTIC_RECURRENCE, 0, 0,
      "match syntactic-recurrence formulas", 0 },
    { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, 0, 0,
      "match syntactic-persistence formulas", 0 },
152 153 154
    { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, 0, 0,
      "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 },
    { "nox", 0, 0, OPTION_ALIAS, 0, 0 },
155 156 157 158 159 160 161 162 163 164 165 166 167 168
    { "safety", OPT_SAFETY, 0, 0,
      "match safety formulas (even pathological)", 0 },
    { "guarantee", OPT_GUARANTEE, 0, 0,
      "match guarantee formulas (even pathological)", 0 },
    { "obligation", OPT_OBLIGATION, 0, 0,
      "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 },
169 170 171 172 173 174
    { "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 },
175 176 177
    { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, 0, 0,
      "match stutter-insensitive LTL formulas", 0 },
    { "stutter-invariant", 0, 0, OPTION_ALIAS, 0, 0 },
178 179
    { "ap", OPT_AP_N, "N", 0,
      "match formulas which use exactly N atomic propositions", 0 },
180 181 182
    { "invert-match", 'v', 0, 0, "select non-matching formulas", 0},
    { "unique", 'u', 0, 0,
      "drop formulas that have already been output (not affected by -v)", 0 },
183
    /**************************************************/
184
    { 0, 0, 0, 0, "Output options:", -20 },
185
    { "count", 'c', 0, 0, "print only a count of matched formulas", 0 },
186
    { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
187
    { "max-count", 'n', "NUM", 0, "output at most NUM formulas", 0 },
188 189 190 191 192 193 194 195
    { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
      "the following interpreted sequences:", -19 },
    { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula (in the selected syntax)", 0 },
    { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the name of the input file", 0 },
    { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the original line number in the input file", 0 },
196 197 198 199 200 201
    { "%<", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the part of the line before the formula if it "
      "comes from a column extracted from a CSV file", 0 },
    { "%>", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the part of the line after the formula if it "
      "comes from a column extracted from a CSV file", 0 },
202 203
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
204 205 206 207
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };

208 209
const struct argp_child children[] =
  {
210
    { &finput_argp, 0, 0, 1 },
211
    { &output_argp, 0, 0, -20 },
212
    { &misc_argp, 0, 0, -1 },
213 214 215
    { 0, 0, 0, 0 }
  };

216 217
static bool one_match = false;

218 219
enum error_style_t { drop_errors, skip_errors };
static error_style_t error_style = drop_errors;
220
static bool ignore_errors = false;
221 222
static bool nnf = false;
static bool negate = false;
223
static bool boolean_to_isop = false;
224 225 226 227 228 229 230 231 232 233 234 235
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;
236
static bool syntactic_si = false;
237 238 239 240 241 242 243
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;
244 245
enum relabeling_mode { NoRelabeling = 0, ApRelabeling, BseRelabeling };
static relabeling_mode relabeling = NoRelabeling;
246
static spot::ltl::relabeling_style style = spot::ltl::Abc;
247
static bool remove_wm = false;
248 249
static bool remove_x = false;
static bool stutter_insensitive = false;
250 251
static bool ap = false;
static unsigned ap_n = 0;
252
static int opt_max_count = -1;
253
static long int match_count = 0;
254
static spot::exclusive_ap excl_ap;
255 256
static std::unique_ptr<output_file> output_define = nullptr;

257

258 259 260 261 262 263 264 265
static const spot::ltl::formula* implied_by = 0;
static const spot::ltl::formula* imply = 0;
static const spot::ltl::formula* equivalent_to = 0;

static const spot::ltl::formula*
parse_formula_arg(const std::string& input)
{
  spot::ltl::parse_error_list pel;
266
  const spot::ltl::formula* f = parse_formula(input, pel);
267
  if (spot::ltl::format_parse_errors(std::cerr, input, pel))
268
    error(2, 0, "parse error when parsing an argument");
269 270 271
  return f;
}

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

429 430 431
typedef
std::unordered_set<const spot::ltl::formula*,
		   const spot::ptr_hash<const spot::ltl::formula>> fset_t;
432 433 434

namespace
{
435
  class ltl_processor: public job_processor
436 437 438 439
  {
  public:
    spot::ltl::ltl_simplifier& simpl;
    fset_t unique_set;
440
    spot::ltl::relabeling_map relmap;
441

442 443 444 445 446
    ~ltl_processor()
    {
      fset_t::iterator i = unique_set.begin();
      while (i != unique_set.end())
	(*i++)->destroy();
447 448 449 450 451 452 453

      if (equivalent_to)
	equivalent_to->destroy();
      if (implied_by)
	implied_by->destroy();
      if (imply)
	imply->destroy();
454 455
    }

456 457 458 459 460 461
    ltl_processor(spot::ltl::ltl_simplifier& simpl)
    : simpl(simpl)
    {
    }

    int
462
    process_string(const std::string& input,
463 464 465
		    const char* filename = 0, int linenum = 0)
    {
      spot::ltl::parse_error_list pel;
466
      const spot::ltl::formula* f = parse_formula(input, pel);
467 468 469

      if (!f || pel.size() > 0)
	  {
470
	    if (!ignore_errors)
471 472
	      {
		if (filename)
473
		  error_at_line(0, 0, filename, linenum, "parse error:");
474 475 476 477 478 479 480
		spot::ltl::format_parse_errors(std::cerr, input, pel);
	      }

	    if (f)
	      f->destroy();

	    if (error_style == skip_errors)
481 482 483
	      std::cout << input << std::endl;
	    else
	      assert(error_style == drop_errors);
484
	    check_cout();
485
	    return !ignore_errors;
486
	  }
487 488 489 490 491 492 493 494 495
      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();
	}
496
    }
497

498 499 500 501
    int
    process_formula(const spot::ltl::formula* f,
		    const char* filename = 0, int linenum = 0)
    {
502
      if (opt_max_count >= 0 && match_count >= opt_max_count)
503 504 505 506 507 508
	{
	  abort_run = true;
	  f->destroy();
	  return 0;
	}

509
      if (negate)
510
	f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
511

512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
      if (remove_x)
	{
	  // If simplification are enabled, we do them before and after.
	  if (simplification_level)
	    {
	      const spot::ltl::formula* res = simpl.simplify(f);
	      f->destroy();
	      f = res;
	    }

	  const spot::ltl::formula* res = spot::ltl::remove_x(f);
	  f->destroy();
	  f = res;
	}

527
      if (simplification_level || boolean_to_isop)
528 529 530 531 532 533 534 535 536 537 538 539 540
	{
	  const spot::ltl::formula* res = simpl.simplify(f);
	  f->destroy();
	  f = res;
	}

      if (nnf)
	{
	  const spot::ltl::formula* res = simpl.negative_normal_form(f);
	  f->destroy();
	  f = res;
	}

541
      switch (relabeling)
542
	{
543 544
	case ApRelabeling:
	  {
545 546
	    relmap.clear();
	    auto res = spot::ltl::relabel(f, style, &relmap);
547 548 549 550 551 552
	    f->destroy();
	    f = res;
	    break;
	  }
	case BseRelabeling:
	  {
553 554
	    relmap.clear();
	    auto res = spot::ltl::relabel_bse(f, style, &relmap);
555 556 557 558 559 560
	    f->destroy();
	    f = res;
	    break;
	  }
	case NoRelabeling:
	  break;
561 562 563 564 565
	}

      if (remove_wm)
	{
	  const spot::ltl::formula* res = spot::ltl::unabbreviate_wm(f);
566 567 568 569
	  f->destroy();
	  f = res;
	}

570 571 572 573 574 575 576
      if (!excl_ap.empty())
	{
	  auto res = excl_ap.constrain(f);
	  f->destroy();
	  f = res;
	}

577 578 579 580 581 582 583 584 585 586 587 588
      bool matched = true;

      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();
589
      matched &= !syntactic_si || f->is_syntactic_stutter_invariant();
590
      matched &= !ap || atomic_prop_collect(f)->size() == ap_n;
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605

      if (matched && (size_min > 0 || size_max >= 0))
	{
	  int l = spot::ltl::length(f);
	  matched &= (size_min <= 0) || (l >= size_min);
	  matched &= (size_max < 0) || (l <= size_max);
	}

      if (matched && (bsize_min > 0 || bsize_max >= 0))
	{
	  int l = spot::ltl::length_boolone(f);
	  matched &= (bsize_min <= 0) || (l >= bsize_min);
	  matched &= (bsize_max < 0) || (l <= bsize_max);
	}

606 607 608
      matched &= !implied_by || simpl.implication(implied_by, f);
      matched &= !imply || simpl.implication(f, imply);
      matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to);
609
      matched &= !stutter_insensitive || spot::is_stutter_invariant(f);
610

611 612 613 614 615 616
      // 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)
	{
617 618
	  auto aut = ltl_to_tgba_fm(f, simpl.get_dict());
	  auto min = minimize_obligation(aut, f);
619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643
	  assert(min);
	  if (aut == min)
	    {
	      // Not an obligation
	      matched = false;
	    }
	  else
	    {
	      matched &= !guarantee || is_guarantee_automaton(min);
	      matched &= !safety || is_safety_mwdba(min);
	    }
	}

      matched ^= invert;

      if (unique)
	{
	  if (unique_set.insert(f).second)
	    f->clone();
	  else
	    matched = false;
	}

      if (matched)
	{
644 645 646 647 648 649 650 651 652 653 654 655 656
	  if (output_define
	      && output_format != count_output
	      && output_format != quiet_output)
	    {
	      // Sort the formulas alphabetically.
	      std::map<std::string, const spot::ltl::formula*> m;
	      for (auto& p: relmap)
		m.emplace(to_string(p.first), p.second);
	      for (auto& p: m)
		stream_formula(output_define->ostream()
			       << "#define " << p.first << " (",
			       p.second, filename, linenum) << ")\n";
	    }
657
	  one_match = true;
658
	  output_formula_checked(f, filename, linenum, prefix, suffix);
659
	  ++match_count;
660 661 662 663 664 665 666 667 668 669
	}
      f->destroy();
      return 0;
    }
  };
}

int
main(int argc, char** argv)
{
670
  setup(argv);
671

672
  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
673
		    argp_program_doc, children, 0, 0 };
674

675 676
  try
    {
677 678 679 680 681 682 683 684 685 686 687 688
      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
	exit(err);

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

      if (boolean_to_isop && simplification_level == 0)
	simplification_level = 1;
      spot::ltl::ltl_simplifier_options opt(simplification_level);
      opt.boolean_to_isop = boolean_to_isop;
      spot::ltl::ltl_simplifier simpl(opt);

689 690 691 692 693 694 695 696
      ltl_processor processor(simpl);
      if (processor.run())
	return 2;
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
697 698 699 700
  catch (const std::invalid_argument& e)
    {
      error(2, 0, "%s", e.what());
    }
701 702 703 704

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

705
  return one_match ? 0 : 1;
706
}