From 4b8910d3f9a2cec3bb9584e07b911ce1a54bc745 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 24 Jul 2018 14:52:14 +0200
Subject: [PATCH] ltlfilt: introduce --suspendable

* bin/ltlfilt.cc: Add the option.
* tests/core/ltlfilt.test: Use it.
* NEWS: Mention it.
---
 NEWS                    | 3 +++
 bin/ltlfilt.cc          | 7 +++++++
 tests/core/ltlfilt.test | 5 +++++
 3 files changed, 15 insertions(+)

diff --git a/NEWS b/NEWS
index d4713d5d9..423a16e95 100644
--- a/NEWS
+++ b/NEWS
@@ -31,6 +31,9 @@ New in spot 2.6.0.dev  (not yet released)
     with arbitrary acceptance condition into a parity automaton,
     based on a last-appearance record (LAR) construction.
 
+  - "ltlfilt --suspendable" is now a synonym for
+    "ltlfilt --universal --eventual".
+
 New in spot 2.6  (2018-07-04)
 
   Command-line tools:
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index f44dfe82d..460d31c13 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -100,6 +100,7 @@ enum {
   OPT_SIZE_MIN,
   OPT_SKIP_ERRORS,
   OPT_STUTTER_INSENSITIVE,
+  OPT_SUSPENDABLE,
   OPT_SYNTACTIC_GUARANTEE,
   OPT_SYNTACTIC_OBLIGATION,
   OPT_SYNTACTIC_PERSISTENCE,
@@ -167,6 +168,8 @@ static const argp_option options[] =
     { "eventual", OPT_EVENTUAL, nullptr, 0, "match pure eventualities", 0 },
     { "universal", OPT_UNIVERSAL, nullptr, 0,
       "match purely universal formulas", 0 },
+    { "suspendable", OPT_SUSPENDABLE, nullptr, 0,
+      "synonym for --universal --eventual", 0 },
     { "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0,
       "match syntactic-safety formulas", 0 },
     { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0,
@@ -507,6 +510,10 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_AP_N:
       ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
+    case OPT_SUSPENDABLE:
+      universal = true;
+      eventual = true;
+      break;
     case OPT_SYNTACTIC_SAFETY:
       syntactic_safety = true;
       break;
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index 063c01159..3ab827c3f 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -84,6 +84,11 @@ GFa | FGb
 F(GFa | Gb)
 EOF
 
+checkopt --suspendable <<EOF
+GFa | FGb
+F(GFa | Gb)
+EOF
+
 checkopt --stutter-invariant <<EOF
 GFa | FGb
 F(GFa | Gb)