diff --git a/NEWS b/NEWS index 8072a641b..3eb0e09db 100644 --- a/NEWS +++ b/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. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 1f25e4fd4..ac559fdca 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -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::max() }; static bool opt_nondet_states_set = false; static int opt_max_count = -1; +static range opt_nth = { 0, std::numeric_limits::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::max()); + break; case 'u': opt->uniq = std::unique_ptr(new std::set>()); @@ -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()); diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index d16684ef8..02596cde1 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -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::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::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) { diff --git a/tests/core/genaut.test b/tests/core/genaut.test index 064aec795..5da9509ed 100644 --- a/tests/core/genaut.test +++ b/tests/core/genaut.test @@ -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 diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 23d284ab3..4a85c7c66 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -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