genltl: support --positive and --negative

* bin/genltl.cc: Implement these options.
* NEWS: Mention them.
* tests/core/genltl.test: New file with test cases.
* tests/Makefile.am: Add it.

NEWS

@@ -42,16 +42,20 @@ New in spot 2.0.3a (not yet released)
     'b U (a & b)' instead.  The operators that can be listed between
     brackets are the same as those of ltlfilt --unabbreviate option.
 
-  * genltl has three new options: --dac-patterns=1..45,
+  * genltl has learned three new families: --dac-patterns=1..45,
     --eh-patterns=1..12, and --sb-patterns=1..27.  Unlike other options
     these do not output scalable patterns, but simply a list of formulas
     appearing in these three papers: Dwyer et al (FMSP'98), Etessami &
     Holzmann (Concur'00), Somenzi & Bloem (CAV'00).
 
+  * genltl has two additional options, --positive and --negative, to
+    control wether formulas should be output after negation or not (or
+    both).
+
   * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
     that are not used are now reported as they might be typos.
     This ocurred a couple of times in our test-suite.  A similar
-    check is done the the arguments of autfilt --sat-minimize=...
+    check is done for the arguments of autfilt --sat-minimize=...
 
   Library:
 

bin/genltl.cc

@@ -161,6 +161,8 @@ enum {
   OPT_U_LEFT,
   OPT_U_RIGHT,
   LAST_CLASS,
+  OPT_POSITIVE,
+  OPT_NEGATIVE,
 };
 
 const char* const class_name[LAST_CLASS] =
@@ -251,6 +253,12 @@ static const argp_option options[] =
     RANGE_DOC,
   /**************************************************/
     { nullptr, 0, nullptr, 0, "Output options:", -20 },
+    { "negative", OPT_NEGATIVE, nullptr, 0,
+      "output the negated versions of all formulas", 0 },
+    OPT_ALIAS(negated),
+    { "positive", OPT_POSITIVE, nullptr, 0,
+      "output the positive versions of all formulas (done by default, unless"
+      " --negative is specified without --positive)", 0 },
     { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
       "the following interpreted sequences:", -19 },
     { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@@ -273,7 +281,8 @@ struct job
 
 typedef std::vector<job> jobs_t;
 static jobs_t jobs;
-
+bool opt_positive = false;
+bool opt_negative = false;
 
 const struct argp_child children[] =
   {
@@ -346,6 +355,12 @@ parse_opt(int key, char* arg, struct argp_state*)
       else
         enqueue_job(key, 1, 27);
       break;
+    case OPT_POSITIVE:
+      opt_positive = true;
+      break;
+    case OPT_NEGATIVE:
+      opt_negative = true;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }
@@ -1042,7 +1057,16 @@ output_pattern(int pattern, int n)
   if (output_format == lbt_output && !f.has_lbt_atomic_props())
     f = relabel(f, Pnn);
 
-  output_formula_checked(f, class_name[pattern - 1], n);
+  if (opt_positive || !opt_negative)
+    {
+      output_formula_checked(f, class_name[pattern - 1], n);
+    }
+  if (opt_negative)
+    {
+      std::string tmp = "!";
+      tmp += class_name[pattern - 1];
+      output_formula_checked(spot::formula::Not(f), tmp.c_str(), n);
+    }
 }
 
 static void

tests/Makefile.am

@@ -151,6 +151,7 @@ TESTS_tl = \
   core/length.test \
   core/equals.test \
   core/tostring.test \
+  core/genltl.test \
   core/lunabbrev.test \
   core/tunabbrev.test \
   core/nenoform.test \

tests/core/genltl.test

@@ -0,0 +1,80 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2016 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# 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
+# the Free Software Foundation; either version 3 of the License, or
+# (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
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+set -e
+
+run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output
+cat >expected <<EOF
+dac-patterns:1 G!p0
+!dac-patterns:1 !G!p0
+dac-patterns:2 Fp0 -> (!p1 U p0)
+!dac-patterns:2 !(Fp0 -> (!p1 U p0))
+dac-patterns:3 G(p0 -> G!p1)
+!dac-patterns:3 !G(p0 -> G!p1)
+dac-patterns:4 G((p0 & !p1 & Fp1) -> (!p2 U p1))
+!dac-patterns:4 !G((p0 & !p1 & Fp1) -> (!p2 U p1))
+dac-patterns:5 G((p0 & !p1) -> (!p2 W p1))
+!dac-patterns:5 !G((p0 & !p1) -> (!p2 W p1))
+eh-patterns:1 p0 U (p1 & Gp2)
+!eh-patterns:1 !(p0 U (p1 & Gp2))
+eh-patterns:2 p0 U (p1 & X(p2 U p3))
+!eh-patterns:2 !(p0 U (p1 & X(p2 U p3)))
+eh-patterns:3 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
+!eh-patterns:3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))))
+eh-patterns:4 F(p0 & XGp1)
+!eh-patterns:4 !F(p0 & XGp1)
+eh-patterns:5 F(p0 & X(p1 & XFp2))
+!eh-patterns:5 !F(p0 & X(p1 & XFp2))
+EOF
+diff expected output
+
+genltl --dac=1..5 --eh=1..5 --neg --format="%L %f" >output
+cat >expected <<EOF
+1 !G!p0
+2 !(Fp0 -> (!p1 U p0))
+3 !G(p0 -> G!p1)
+4 !G((p0 & !p1 & Fp1) -> (!p2 U p1))
+5 !G((p0 & !p1) -> (!p2 W p1))
+1 !(p0 U (p1 & Gp2))
+2 !(p0 U (p1 & X(p2 U p3)))
+3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))))
+4 !F(p0 & XGp1)
+5 !F(p0 & X(p1 & XFp2))
+EOF
+diff expected output
+
+genltl --dac=1..5 --eh=1..5 --pos --format="%f" >output
+cat >expected <<EOF
+G!p0
+Fp0 -> (!p1 U p0)
+G(p0 -> G!p1)
+G((p0 & !p1 & Fp1) -> (!p2 U p1))
+G((p0 & !p1) -> (!p2 W p1))
+p0 U (p1 & Gp2)
+p0 U (p1 & X(p2 U p3))
+p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
+F(p0 & XGp1)
+F(p0 & X(p1 & XFp2))
+EOF
+diff expected output
+
+genltl --dac=1..5 --eh=1..5 >output2
+diff output output2