From 1c8244437634f37b6f04f359391531277dbd1998 Mon Sep 17 00:00:00 2001 From: Amaury Fauchille Date: Fri, 5 Feb 2016 17:26:31 +0100 Subject: [PATCH] autfilt: add new option --accept-word Suggested by Matthias Heizmann. Fixes #109. * NEWS: notify the new option * THANKS: add Matthias Heizmann * bin/autfilt.cc: add new option --accept-word=WORD which filters automata that accept WORD * doc/org/autfilt.org: add an example of the new option * tests/Makefile.am: add core/acc_word.test to the list of test files * tests/core/acc_word.test: test some uses of the new option --- NEWS | 6 ++++++ THANKS | 1 + bin/autfilt.cc | 41 ++++++++++++++++++++++++++++++++++++++++ doc/org/autfilt.org | 24 +++++------------------ tests/Makefile.am | 3 ++- tests/core/acc_word.test | 27 ++++++++++++++++++++++++++ 6 files changed, 82 insertions(+), 20 deletions(-) create mode 100644 tests/core/acc_word.test diff --git a/NEWS b/NEWS index 4e9243b64..cd093861a 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ New in spot 1.99.8a (not yet released) + Command-line tools: + + * autfilt has a new option: --accept-word=WORD, that filters automata + that accept WORD. This option can be used several times, and will + filter automata that accept all words. + Library: * twa::ap_var() renamed to twa::ap_vars(). diff --git a/THANKS b/THANKS index a6855224b..4c9aa543a 100644 --- a/THANKS +++ b/THANKS @@ -19,6 +19,7 @@ Jean-Michel Ilié Joachim Klein Kristin Y. Rozier Martin Dieguez Lodeiro +Matthias Heizmann Michael Tautschnig Michael Weber Ming-Hsien Tsai diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e0f20d125..a4b070b0c 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -69,6 +69,7 @@ Exit status:\n\ // Keep this list sorted enum { OPT_ACC_SETS = 256, + OPT_ACC_WORD, OPT_AP_N, OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, @@ -224,6 +225,8 @@ static const argp_option options[] = "keep automata whose number of edges are in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets are in RANGE", 0 }, + { "accept-word", OPT_ACC_WORD, "WORD", 0, + "keep automata that recognize WORD", 0 }, RANGE_DOC_FULL, { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " @@ -293,6 +296,7 @@ static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; static range opt_ap_n = { 0, std::numeric_limits::max() }; +static std::vector opt_acc_words; static int opt_max_count = -1; static bool opt_destut = false; static char opt_instut = 0; @@ -361,6 +365,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ACC_SETS: opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_ACC_WORD: + opt_acc_words.push_back(arg); + break; case OPT_ARE_ISOMORPHIC: opt->are_isomorphic = read_automaton(arg, opt->dict); break; @@ -652,6 +659,20 @@ namespace matched &= spot::product(aut, opt->equivalent_neg)->is_empty() && spot::product(dtwa_complement(ensure_deterministic(aut)), opt->equivalent_pos)->is_empty(); + if (!opt_acc_words.empty()) + { + auto word_aut = spot::parse_word(opt_acc_words[0], + opt->dict)->as_automaton(); + for (size_t i = 1; i < opt_acc_words.size(); ++i) + { + // Compose each additionnanl word with the first one + word_aut = spot::product(word_aut, + spot::parse_word(opt_acc_words[i], + opt->dict) + ->as_automaton()); + } + matched &= !spot::product(aut, word_aut)->is_empty(); + } // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) @@ -812,6 +833,26 @@ main(int argc, char** argv) if (processor.run()) return 2; } + catch (const spot::parse_error& e) + { + auto is_several_lines = + [] (const char* err) + { + for (;;) + { + if (*err == '\0') + return false; + else if (*err == '\n') + return true; + ++err; + } + }; + auto err = e.what(); + if (is_several_lines(err)) + error(2, 0, "\n%s", err); + else + error(2, 0, "%s", err); + } catch (const std::runtime_error& e) { error(2, 0, "%s", e.what()); diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index c5129f885..2755b539d 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -700,25 +700,6 @@ autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a #+END_SRC #+RESULTS: autfilt-ex6c -#+begin_example -digraph G { - rankdir=LR - label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> - labelloc="t" - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 0 - 0 [label="0"] - 0 -> 0 [label=<1
❸>] - 0 -> 1 [label=<1
❶❸>] - 1 [label="1"] - 1 -> 0 [label=❸>] - 1 -> 1 [label=⓿❸>] -} -#+end_example #+BEGIN_SRC dot :file autfilt-ex6c.png :cmdline -Tpng :var txt=autfilt-ex6c :exports results $txt @@ -730,3 +711,8 @@ $txt #+BEGIN_SRC sh :results silent :exports results rm -f example.hoa aut-ex1.hoa #+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba 'a U b U c' | autfilt --accept-word 'b; cycle{c}' -q && +echo "word accepted" +#+END_SRC diff --git a/tests/Makefile.am b/tests/Makefile.am index 638af8e06..a1c49208e 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -277,7 +277,8 @@ TESTS_twa = \ core/ltlcross2.test \ core/complementation.test \ core/randpsl.test \ - core/cycles.test + core/cycles.test \ + core/acc_word.test ############################## PYTHON ############################## diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test new file mode 100644 index 000000000..7b7869462 --- /dev/null +++ b/tests/core/acc_word.test @@ -0,0 +1,27 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +# The --accept-word option filters automata that accept the given word +# If several words are given, it filters automata that accept ALL words +ltl2tgba 'G!a' | autfilt --accept-word 'b; cycle{!a}' +ltl2tgba 'a U b' | autfilt --accept-word 'a; a; cycle{b}' +ltl2tgba 'F(!a&b)' | + autfilt --accept-word 'b; cycle{b; !a&b}' --accept-word 'cycle{b}'