From cad4d94cc2b302ddf2c9f49e4b9fc9c4a5d1ccc7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Dec 2014 11:59:06 +0100 Subject: [PATCH] autfilt: --states=RANGE * src/bin/autfilt.cc: Add a --states=RANGE option. * src/bin/common_range.cc, src/bin/common_range.hh: Generalize range_parse to allow an optional upper bound. --- src/bin/autfilt.cc | 14 +++++++++++++- src/bin/common_range.cc | 37 ++++++++++++++++++++++++------------- src/bin/common_range.hh | 21 ++++++++++++++++++--- 3 files changed, 55 insertions(+), 17 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 94a3f5d33..3c0877c7d 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -21,6 +21,7 @@ #include #include +#include #include #include "error.h" @@ -28,6 +29,7 @@ #include "common_setup.hh" #include "common_finput.hh" #include "common_cout.hh" +#include "common_range.hh" #include "common_post.hh" #include "tgbaalgos/dotty.hh" @@ -68,6 +70,8 @@ Exit status:\n\ #define OPT_ARE_ISOMORPHIC 10 #define OPT_IS_COMPLETE 11 #define OPT_IS_DETERMINISTIC 12 +#define OPT_STATES 17 +#define OPT_COUNT 18 static const argp_option options[] = { @@ -145,7 +149,10 @@ static const argp_option options[] = "the automaton is complete", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0, "the automaton is deterministic", 0 }, - { "invert-match", 'v', 0, 0, "select non-matching automata", 0}, + { "invert-match", 'v', 0, 0, "select non-matching automata", 0 }, + { "states", OPT_STATES, "RANGE", 0, + "keep automata whose number of states are in RANGE", 0 }, + RANGE_DOC_FULL, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, @@ -178,6 +185,7 @@ static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr; static bool opt_is_complete = false; static bool opt_is_deterministic = false; static bool opt_invert = false; +static range opt_states = { 0, std::numeric_limits::max() }; static int to_int(const char* s) @@ -306,6 +314,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SPOT: format = Spot; break; + case OPT_STATES: + opt_states = parse_range(arg, 0, std::numeric_limits::max()); + break; case OPT_STATS: if (!*arg) error(2, 0, "empty format string for --stats"); @@ -436,6 +447,7 @@ namespace bool matched = true; + matched &= opt_states.contains(aut->num_states()); if (opt_is_complete) matched &= is_complete(aut); if (opt_is_deterministic) diff --git a/src/bin/common_range.cc b/src/bin/common_range.cc index 761e48a0a..fd338f082 100644 --- a/src/bin/common_range.cc +++ b/src/bin/common_range.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,13 +24,17 @@ #include #include +// The range should have the form INT..INT or INT:INT, with +// "42" standing for "42..42", +// "..42" meaning "missing_left..42". +// and "42.." meaning "42..missing_right". +// +// As an exception, if missing_right is 0, then missing right bounds +// are disallowed. range -parse_range(const char* str) +parse_range(const char* str, int missing_left, int missing_right) { range res; - - // The range should have the form INT..INT or INT:INT, with - // "42" standing for "42..42", and "..42" meaning "1..42". char* end; res.min = strtol(str, &end, 10); if (end == str) @@ -39,7 +43,7 @@ parse_range(const char* str) // empty. if (!*end) error(1, 0, "invalid empty range"); - res.min = 1; + res.min = missing_left; } if (!*end) { @@ -54,13 +58,20 @@ parse_range(const char* str) else if (end[0] == '.' && end[1] == '.') end += 2; - // Parse the next integer. - char* end2; - res.max = strtol(end, &end2, 10); - if (end == end2) - error(1, 0, "invalid range '%s' (missing end?)", str); - if (*end2) - error(1, 0, "invalid range '%s' (trailing garbage?)", str); + if (!*end && missing_right != 0) + { + res.max = missing_right; + } + else + { + // Parse the next integer. + char* end2; + res.max = strtol(end, &end2, 10); + if (end == end2) + error(1, 0, "invalid range '%s' (missing end?)", str); + if (*end2) + error(1, 0, "invalid range '%s' (trailing garbage?)", str); + } } if (res.min < 0 || res.max < 0) diff --git a/src/bin/common_range.hh b/src/bin/common_range.hh index be38d0a88..587965d6f 100644 --- a/src/bin/common_range.hh +++ b/src/bin/common_range.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -26,12 +26,27 @@ "'INT..INT', or '..INT'.\nIn the latter case, the missing number " \ "is assumed to be 1.", 0 } +#define RANGE_DOC_FULL \ + { 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', " \ + "'INT..INT', '..INT', or 'INT..'", 0 } + struct range { int min; int max; + + bool contains(int val) + { + return val >= min && val <= max; + } }; -range parse_range(const char* str); +// INT, INT..INT, ..INT, or INT.. +// +// The missing_left and missing_right argument gives the default bound +// values. Additionally, if missing_right == 0, then the INT.. form +// is disallowed. +range parse_range(const char* str, + int missing_left = 1, int missing_right = 0); #endif // SPOT_BIN_COMMON_RANGE_HH