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.
This commit is contained in:
parent
1a022c8093
commit
cad4d94cc2
3 changed files with 55 additions and 17 deletions
|
|
@ -21,6 +21,7 @@
|
||||||
|
|
||||||
#include <string>
|
#include <string>
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
#include <limits>
|
||||||
|
|
||||||
#include <argp.h>
|
#include <argp.h>
|
||||||
#include "error.h"
|
#include "error.h"
|
||||||
|
|
@ -28,6 +29,7 @@
|
||||||
#include "common_setup.hh"
|
#include "common_setup.hh"
|
||||||
#include "common_finput.hh"
|
#include "common_finput.hh"
|
||||||
#include "common_cout.hh"
|
#include "common_cout.hh"
|
||||||
|
#include "common_range.hh"
|
||||||
#include "common_post.hh"
|
#include "common_post.hh"
|
||||||
|
|
||||||
#include "tgbaalgos/dotty.hh"
|
#include "tgbaalgos/dotty.hh"
|
||||||
|
|
@ -68,6 +70,8 @@ Exit status:\n\
|
||||||
#define OPT_ARE_ISOMORPHIC 10
|
#define OPT_ARE_ISOMORPHIC 10
|
||||||
#define OPT_IS_COMPLETE 11
|
#define OPT_IS_COMPLETE 11
|
||||||
#define OPT_IS_DETERMINISTIC 12
|
#define OPT_IS_DETERMINISTIC 12
|
||||||
|
#define OPT_STATES 17
|
||||||
|
#define OPT_COUNT 18
|
||||||
|
|
||||||
static const argp_option options[] =
|
static const argp_option options[] =
|
||||||
{
|
{
|
||||||
|
|
@ -145,7 +149,10 @@ static const argp_option options[] =
|
||||||
"the automaton is complete", 0 },
|
"the automaton is complete", 0 },
|
||||||
{ "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
|
{ "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
|
||||||
"the automaton is deterministic", 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 },
|
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
|
||||||
{ "extra-options", 'x', "OPTS", 0,
|
{ "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_complete = false;
|
||||||
static bool opt_is_deterministic = false;
|
static bool opt_is_deterministic = false;
|
||||||
static bool opt_invert = false;
|
static bool opt_invert = false;
|
||||||
|
static range opt_states = { 0, std::numeric_limits<int>::max() };
|
||||||
|
|
||||||
static int
|
static int
|
||||||
to_int(const char* s)
|
to_int(const char* s)
|
||||||
|
|
@ -306,6 +314,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
case OPT_SPOT:
|
case OPT_SPOT:
|
||||||
format = Spot;
|
format = Spot;
|
||||||
break;
|
break;
|
||||||
|
case OPT_STATES:
|
||||||
|
opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
|
break;
|
||||||
case OPT_STATS:
|
case OPT_STATS:
|
||||||
if (!*arg)
|
if (!*arg)
|
||||||
error(2, 0, "empty format string for --stats");
|
error(2, 0, "empty format string for --stats");
|
||||||
|
|
@ -436,6 +447,7 @@ namespace
|
||||||
|
|
||||||
bool matched = true;
|
bool matched = true;
|
||||||
|
|
||||||
|
matched &= opt_states.contains(aut->num_states());
|
||||||
if (opt_is_complete)
|
if (opt_is_complete)
|
||||||
matched &= is_complete(aut);
|
matched &= is_complete(aut);
|
||||||
if (opt_is_deterministic)
|
if (opt_is_deterministic)
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -24,13 +24,17 @@
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
#include <cstdlib>
|
#include <cstdlib>
|
||||||
|
|
||||||
|
// 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
|
range
|
||||||
parse_range(const char* str)
|
parse_range(const char* str, int missing_left, int missing_right)
|
||||||
{
|
{
|
||||||
range res;
|
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;
|
char* end;
|
||||||
res.min = strtol(str, &end, 10);
|
res.min = strtol(str, &end, 10);
|
||||||
if (end == str)
|
if (end == str)
|
||||||
|
|
@ -39,7 +43,7 @@ parse_range(const char* str)
|
||||||
// empty.
|
// empty.
|
||||||
if (!*end)
|
if (!*end)
|
||||||
error(1, 0, "invalid empty range");
|
error(1, 0, "invalid empty range");
|
||||||
res.min = 1;
|
res.min = missing_left;
|
||||||
}
|
}
|
||||||
if (!*end)
|
if (!*end)
|
||||||
{
|
{
|
||||||
|
|
@ -54,13 +58,20 @@ parse_range(const char* str)
|
||||||
else if (end[0] == '.' && end[1] == '.')
|
else if (end[0] == '.' && end[1] == '.')
|
||||||
end += 2;
|
end += 2;
|
||||||
|
|
||||||
// Parse the next integer.
|
if (!*end && missing_right != 0)
|
||||||
char* end2;
|
{
|
||||||
res.max = strtol(end, &end2, 10);
|
res.max = missing_right;
|
||||||
if (end == end2)
|
}
|
||||||
error(1, 0, "invalid range '%s' (missing end?)", str);
|
else
|
||||||
if (*end2)
|
{
|
||||||
error(1, 0, "invalid range '%s' (trailing garbage?)", str);
|
// 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)
|
if (res.min < 0 || res.max < 0)
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
|
||||||
// l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// 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 " \
|
"'INT..INT', or '..INT'.\nIn the latter case, the missing number " \
|
||||||
"is assumed to be 1.", 0 }
|
"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
|
struct range
|
||||||
{
|
{
|
||||||
int min;
|
int min;
|
||||||
int max;
|
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
|
#endif // SPOT_BIN_COMMON_RANGE_HH
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue