ltlfilt, autfilt: add support for --nth
* bin/autfilt.cc, bin/ltlfilt.cc: Implement it. * NEWS: Mention it. * tests/core/genaut.test, tests/core/genltl.test: Add test cases.
This commit is contained in:
Alexandre Duret-Lutz
parent
4e99518da7
commit
c3d7e942d3
5 changed files with 48 additions and 7 deletions
10
NEWS
10
NEWS
|
|
@ -14,13 +14,17 @@ New in spot 2.8.6.dev (not yet released)
|
|||
spot-accepted-word: "!a; cycle{a}"
|
||||
spot-rejected-word: "!a; !a; cycle{a}"
|
||||
|
||||
- When running translators ltlcross will now display {names} when
|
||||
supplied.
|
||||
|
||||
- autfilt learned the --partial-degeneralize option, to remove
|
||||
conjunctions of Inf, or disjunction of Fin that appears in
|
||||
arbitrary conditions.
|
||||
|
||||
- ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to
|
||||
select a range of their input formulas or automata (assuming a
|
||||
1-based numbering).
|
||||
|
||||
- When running translators ltlcross will now display {names} when
|
||||
supplied.
|
||||
|
||||
- ltlcross is now using the generic emptiness check procedure
|
||||
introduced in Spot 2.7, as opposed to removing Fin acceptance
|
||||
before using a classical emptiness check.
|
||||
|
|
|
|||
|
|
@ -267,6 +267,9 @@ static const argp_option options[] =
|
|||
"keep automata that accept WORD", 0 },
|
||||
{ "reject-word", OPT_REJECT_WORD, "WORD", 0,
|
||||
"keep automata that reject WORD", 0 },
|
||||
{ "nth", 'N', "RANGE", 0,
|
||||
"assuming input automata are numbered from 1, keep only those in RANGE",
|
||||
0 },
|
||||
/**************************************************/
|
||||
RANGE_DOC_FULL,
|
||||
WORD_DOC,
|
||||
|
|
@ -612,6 +615,7 @@ static bool opt_terminal_sccs_set = false;
|
|||
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
|
||||
static bool opt_nondet_states_set = false;
|
||||
static int opt_max_count = -1;
|
||||
static range opt_nth = { 0, std::numeric_limits<int>::max() };
|
||||
static bool opt_destut = false;
|
||||
static char opt_instut = 0;
|
||||
static bool opt_is_empty = false;
|
||||
|
|
@ -709,6 +713,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
case 'n':
|
||||
opt_max_count = to_pos_int(arg, "-n/--max-count");
|
||||
break;
|
||||
case 'N':
|
||||
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||
break;
|
||||
case 'u':
|
||||
opt->uniq =
|
||||
std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
|
||||
|
|
@ -1310,6 +1317,9 @@ namespace
|
|||
int
|
||||
process_automaton(const spot::const_parsed_aut_ptr& haut) override
|
||||
{
|
||||
static unsigned order = 0;
|
||||
++order;
|
||||
|
||||
spot::process_timer timer;
|
||||
timer.start();
|
||||
|
||||
|
|
@ -1350,6 +1360,7 @@ namespace
|
|||
|
||||
bool matched = true;
|
||||
|
||||
matched &= opt_nth.contains(order);
|
||||
matched &= opt_states.contains(aut->num_states());
|
||||
matched &= opt_edges.contains(aut->num_edges());
|
||||
matched &= opt_accsets.contains(aut->acc().num_sets());
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -223,6 +223,9 @@ static const argp_option options[] =
|
|||
{ "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
|
||||
{ "ap", OPT_AP_N, "RANGE", 0,
|
||||
"match formulas with a number of atomic propositions in RANGE", 0 },
|
||||
{ "nth", 'N', "RANGE", 0,
|
||||
"assuming input formulas are numbered from 1, keep only those 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 },
|
||||
|
|
@ -309,6 +312,7 @@ static spot::relabeling_style style = spot::Abc;
|
|||
static bool remove_x = false;
|
||||
static bool stutter_insensitive = false;
|
||||
static range ap_n = { -1, -1 };
|
||||
static range opt_nth = { 0, std::numeric_limits<int>::max() };
|
||||
static int opt_max_count = -1;
|
||||
static long int match_count = 0;
|
||||
static const char* from_ltlf = nullptr;
|
||||
|
|
@ -356,6 +360,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
case 'n':
|
||||
opt_max_count = to_pos_int(arg, "-n/--max-count");
|
||||
break;
|
||||
case 'N':
|
||||
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||
break;
|
||||
case 'q':
|
||||
output_format = quiet_output;
|
||||
break;
|
||||
|
|
@ -605,6 +612,8 @@ namespace
|
|||
process_formula(spot::formula f,
|
||||
const char* filename = nullptr, int linenum = 0) override
|
||||
{
|
||||
static unsigned order = 0;
|
||||
++order;
|
||||
spot::process_timer timer;
|
||||
timer.start();
|
||||
|
||||
|
|
@ -618,7 +627,7 @@ namespace
|
|||
if (negate)
|
||||
f = spot::formula::Not(f);
|
||||
|
||||
bool matched = true;
|
||||
bool matched = opt_nth.contains(order);
|
||||
|
||||
if (from_ltlf)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2017, 2018, 2019, 2020 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -60,3 +60,12 @@ genaut --l-nba='1..3?' 2>err && exit 1
|
|||
grep 'invalid range.*trailing garbage' err
|
||||
genaut --l-nba='1..' 2>err && exit 1
|
||||
grep 'invalid range.*missing end' err
|
||||
|
||||
|
||||
# Tests for autfilt -N/--nth
|
||||
genaut --ks-nca=1..5 | autfilt -N 2..4 > range1.hoa
|
||||
genaut --ks-nca=2..4 > range2.hoa
|
||||
diff range1.hoa range2.hoa
|
||||
genaut --ks-nca=1..5 | autfilt -v --nth 3..5 > range1.hoa
|
||||
genaut --ks-nca=1..2 > range2.hoa
|
||||
diff range1.hoa range2.hoa
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2016-2019 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2016-2020 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -259,3 +259,11 @@ test "`cat err`" = "genltl: no pattern sb-patterns=0, supported range is 1..27"
|
|||
genltl --sejk-patterns=0 2> err && exit 1
|
||||
test $? = 2
|
||||
test "`cat err`" = "genltl: no pattern sejk-patterns=0, supported range is 1..3"
|
||||
|
||||
# Tests for ltlfilt -N/--nth
|
||||
genltl --sb-patterns=1..20 | ltlfilt -N 5..10 > range1.ltl
|
||||
genltl --sb-patterns=5..10 > range2.ltl
|
||||
diff range1.ltl range2.ltl
|
||||
genltl --sb-patterns=1..20 | ltlfilt -v --nth 10..20 > range1.ltl
|
||||
genltl --sb-patterns=1..9 > range2.ltl
|
||||
diff range1.ltl range2.ltl
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue