From 52bf1da3c2e205b4b4649aa63ad2fefb83ce1c2f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 15 Feb 2016 14:14:18 +0100
Subject: [PATCH] ltlfilt: support --ap=RANGE instead of --ap=N

Fixes #131.

* bin/ltlfilt.cc: Implement the option.
* tests/core/ltlfilt.test: Test it.
* NEWS: Mention it.
---
 NEWS                    |  2 ++
 bin/ltlfilt.cc          | 19 ++++++++++++-------
 tests/core/ltlfilt.test | 28 +++++++++++++++++++++++++++-
 3 files changed, 41 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 26fa1f5fe..9406f3253 100644
--- a/NEWS
+++ b/NEWS
@@ -48,6 +48,8 @@ New in spot 1.99.7a (not yet released)
     --bsize=RANGE.  The old names are still supported for backward
     compatibility, but they are not documented anymore.
 
+  * ltlfilt's option --ap=N can now take a RANGE as parameter.
+
   Library:
 
   * Building products with different dictionaries now raise an
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index c278cb62c..5f6098da5 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -194,8 +194,8 @@ static const argp_option options[] =
     { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, nullptr, 0,
       "match stutter-insensitive LTL formulas", 0 },
     { "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
-    { "ap", OPT_AP_N, "N", 0,
-      "match formulas which use exactly N atomic propositions", 0 },
+    { "ap", OPT_AP_N, "RANGE", 0,
+      "match formulas with a number of atomic propositions in RANGE", 0 },
     { "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
     { "unique", 'u', nullptr, 0,
       "drop formulas that have already been output (not affected by -v)", 0 },
@@ -264,8 +264,7 @@ static relabeling_mode relabeling = NoRelabeling;
 static spot::relabeling_style style = spot::Abc;
 static bool remove_x = false;
 static bool stutter_insensitive = false;
-static bool ap = false;
-static unsigned ap_n = 0;
+static range ap_n = { -1, -1 };
 static int opt_max_count = -1;
 static long int match_count = 0;
 
@@ -433,8 +432,7 @@ parse_opt(int key, char* arg, struct argp_state*)
 	unabbreviate += spot::default_unabbrev_string;
       break;
     case OPT_AP_N:
-      ap = true;
-      ap_n = to_int(arg);
+      ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
     case OPT_SYNTACTIC_SAFETY:
       syntactic_safety = true;
@@ -578,7 +576,14 @@ namespace
       matched &= !syntactic_recurrence || f.is_syntactic_recurrence();
       matched &= !syntactic_persistence || f.is_syntactic_persistence();
       matched &= !syntactic_si || f.is_syntactic_stutter_invariant();
-      matched &= !ap || atomic_prop_collect(f)->size() == ap_n;
+      if (matched && (ap_n.min > 0 || ap_n.max >= 0))
+	{
+	  auto s = atomic_prop_collect(f);
+	  int n = s->size();
+	  delete s;
+	  matched &= (ap_n.min <= 0) || (n >= ap_n.min);
+	  matched &= (ap_n.max < 0) || (n <= ap_n.max);
+	}
 
       if (matched && (size.min > 0 || size.max >= 0))
 	{
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index b2cd43641..31d37265c 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -140,6 +140,32 @@ checkopt -v --ltl <<EOF
 !{a:b[*]:c}
 EOF
 
+checkopt -v --ap=3 <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+a U Fb
+G(a & Xb)
+Xa
+F(a & !Xa & Xb)
+EOF
+
+checkopt --ap=2..3 <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+!({a;b[*];c}!)
+!{a:b[*]:c}
+a U Fb
+G(a & Xb)
+F(a & !Xa & Xb)
+a & (b | c)
+EOF
+
 checkopt -v --stutter-invariant <<EOF
 !({a;b[*];c}!)
 G(a & Xb)