diff --git a/NEWS b/NEWS index a6d4370c1..65118ba56 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,9 @@ New in spot 2.8.1.dev (not yet released) + Command-line tools: + + - ltl2tgba and ltldo learned a --negate option. + Library: - Historically, Spot only supports LTL with infinite semantics diff --git a/bin/common_output.cc b/bin/common_output.cc index a264c3332..092a9329f 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -82,7 +82,7 @@ report_not_ltl(spot::formula f, { std::string s = spot::str_psl(f); static const char msg[] = - "formula '%s' cannot be written %s's syntax because it is not LTL"; + "formula '%s' cannot be written in %s's syntax because it is not LTL"; if (filename) error_at_line(2, 0, filename, atoi(linenum), msg, s.c_str(), syn); else diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 7ab4a5933..332b0a81b 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,6 +46,7 @@ the smallest Transition-based Generalized Büchi Automata, \ output in the HOA format.\n\ If multiple formulas are supplied, several automata will be output."; +enum { OPT_NEGATE = 256 }; static const argp_option options[] = { @@ -59,6 +60,7 @@ static const argp_option options[] = "the part of the line after the formula if it " "comes from a column extracted from a CSV file", 4 }, /**************************************************/ + { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 1 }, { "unambiguous", 'U', nullptr, 0, "output unambiguous automata", 2 }, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, @@ -76,6 +78,7 @@ const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; +static bool negate = false; static spot::option_map extra_options; static spot::postprocessor::output_pref unambig = 0; @@ -95,6 +98,9 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; + case OPT_NEGATE: + negate = true; + break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? if (*arg == '-' && !arg[1]) @@ -139,6 +145,9 @@ namespace s.c_str()); } + if (negate) + f = spot::formula::Not(f); + spot::process_timer timer; timer.start(); auto aut = trans.run(&f); diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 1b7afb48a..374d61c78 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,6 +33,7 @@ #include "common_conv.hh" #include "common_finput.hh" #include "common_aoutput.hh" +#include "common_output.hh" #include "common_post.hh" #include "common_trans.hh" #include "common_hoaread.hh" @@ -51,13 +52,15 @@ of input and output as required."; enum { OPT_ERRORS = 256, - OPT_SMALLEST, - OPT_GREATEST, OPT_FAIL_ON_TIMEOUT, + OPT_GREATEST, + OPT_NEGATE, + OPT_SMALLEST, }; static const argp_option options[] = { + { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 1 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Error handling:", 4 }, { "errors", OPT_ERRORS, "abort|warn|ignore", 0, @@ -129,6 +132,7 @@ static bool fail_on_timeout = false; static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection static const char* best_format = "%s,%e"; static int opt_max_count = -1; +static bool negate = false; static char const *const errors_args[] = { @@ -173,6 +177,9 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg) best_format = arg; break; + case OPT_NEGATE: + negate = true; + break; case OPT_SMALLEST: best_type = -1; if (arg) @@ -336,7 +343,17 @@ namespace return 1; } - inputf = input; + if (negate) + { + pf.f = spot::formula::Not(pf.f); + std::ostringstream os; + stream_formula(os, pf.f, filename, std::to_string(linenum).c_str()); + inputf = os.str(); + } + else + { + inputf = input; + } process_formula(pf.f, filename, linenum); return 0; } @@ -464,6 +481,12 @@ main(int argc, char** argv) setup_sig_handler(); + // Usually we print the formula as it was given to us, but + // if --negate is used we have to reformat it. We don't know + // was the input format unless --lbt-input was given, and in + // that case we keep it for output. + output_format = lbt_input ? lbt_output : spot_output; + spot::postprocessor post; post.set_pref(pref | comp | sbacc | colored); post.set_type(type); diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index b0c0e4d80..f0df4c157 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -646,9 +646,7 @@ complementation ourselves: #+NAME: hier-persistence-2 #+BEGIN_SRC sh :exports code -ltlfilt --negate -f FGa | - ltl2tgba -D | - autfilt --complement -d +ltl2tgba --negate -D FGa | autfilt --complement -d #+END_SRC #+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results $txt diff --git a/tests/core/ltldo2.test b/tests/core/ltldo2.test index 4d739f39e..4998ce98d 100755 --- a/tests/core/ltldo2.test +++ b/tests/core/ltldo2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +# Copyright (C) 2015-2017, 2019 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -37,3 +37,14 @@ diff aut1.hoa aut2.hoa test "ltl2tgba -D" = \ "`ltldo 'ltl2tgba -D' ltl2tgba -f 'Ga | Gb | Gc' --greatest=%e --stats=%T`" + + +ltldo --negate 'ltl2tgba -D' -f FGa --stats=%f,%s >out.csv +ltldo --negate 'ltl2tgba -D' --lbt-input -f 'F G a' --stats=%f,%s >>out.csv +ltl2tgba --negate -D FGa --stats=%f,%s >>out.csv +cat >expected <