ltlfilt: add support for --to-delta2

* bin/ltlfilt.cc: Implement this option.
* tests/core/delta2.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.

NEWS

@@ -9,6 +9,8 @@ New in spot 2.12.0.dev (not yet released)
   - ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and
     --delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂.
 
+  - ltlfilt learned --to-delta2 to transform an LTL formula into Δ₂.
+
   Library:
 
    - restrict_dead_end_edges_here() can reduce non-determinism (but

bin/ltlfilt.cc

@@ -38,6 +38,7 @@
 #include <spot/misc/timer.hh>
 #include <spot/tl/simplify.hh>
 #include <spot/tl/sonf.hh>
+#include <spot/tl/delta2.hh>
 #include <spot/tl/length.hh>
 #include <spot/tl/relabel.hh>
 #include <spot/tl/unabbrev.hh>
@@ -115,6 +116,7 @@ enum {
   OPT_SYNTACTIC_RECURRENCE,
   OPT_SYNTACTIC_SAFETY,
   OPT_SYNTACTIC_SI,
+  OPT_TO_DELTA2,
   OPT_UNABBREVIATE,
   OPT_UNIVERSAL,
 };
@@ -161,6 +163,8 @@ static const argp_option options[] =
     { "remove-x", OPT_REMOVE_X, nullptr, 0,
       "remove X operators (valid only for stutter-insensitive properties)",
       0 },
+    { "to-delta2", OPT_TO_DELTA2, nullptr, 0,
+      "rewrite LTL formula in Δ₂-form", 0 },
     { "unabbreviate", OPT_UNABBREVIATE, "STR", OPTION_ARG_OPTIONAL,
       "remove all occurrences of the operators specified by STR, which "
       "must be a substring of \"eFGiMRW^\", where 'e', 'i', and '^' stand "
@@ -349,7 +353,7 @@ static int opt_max_count = -1;
 static long int match_count = 0;
 static const char* from_ltlf = nullptr;
 static const char* sonf = nullptr;
-
+static bool to_delta2 = false;
 
 // We want all these variables to be destroyed when we exit main, to
 // make sure it happens before all other global variables (like the
@@ -579,6 +583,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_STUTTER_INSENSITIVE:
       stutter_insensitive = true;
       break;
+    case OPT_TO_DELTA2:
+      to_delta2 = true;
+      break;
     case OPT_UNABBREVIATE:
       if (arg)
         unabbreviate += arg;
@@ -734,6 +741,9 @@ namespace
             }
         }
 
+      if (to_delta2)
+        f = spot::to_delta2(f);
+
       switch (relabeling)
         {
         case ApRelabeling:

tests/Makefile.am

@@ -236,6 +236,7 @@ TESTS_twa = \
   core/renault.test \
   core/nondet.test \
   core/det.test \
+  core/delta2.test \
   core/semidet.test \
   core/neverclaimread.test \
   core/parseaut.test \

tests/core/delta2.test

@@ -0,0 +1,30 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) by the Spot authors, see the AUTHORS file for details.
+#
+# 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
+
+genltl --dac-p --eh-p --hkrss-p --sb-p --sejk-p \
+       --stats='%F:%L,%f' > formulas.txt
+ltlfilt --to-delta2 --delta2 -F formulas.txt/2 > res.txt
+ltlfilt --to-delta2 -v --delta2 -F formulas.txt/2 --stats='%<' || :
+test `wc -l < formulas.txt` -eq `wc -l < res.txt`
+
+ltlcross -F formulas.txt/2 \
+         'ltl2tgba' 'ltlfilt --to-delta2 -f %f | ltl2tgba -G >%O'