ltl2tgba, ltldo: add a --negate option

Suggested by Victor Khomenko.

* bin/ltl2tgba.cc, bin/ltldo.cc: Implement it.
* doc/org/hierarchy.org: Use it.
* tests/core/ltldo2.test: Test it.
* bin/common_output.cc: Typo.
* NEWS: Mention the new option.

NEWS

 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

bin/common_output.cc

 // -*- 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

bin/ltl2tgba.cc

 // -*- 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);

bin/ltldo.cc

 // -*- 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);

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

tests/core/ltldo2.test

 #!/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 <<EOF
+!FGa,1
+! F G "a",1
+GF!a,1
+EOF
+diff out.csv expected