From b13caea3d86b456c9501cdedacff98a26bf504f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Jul 2016 17:59:25 +0200 Subject: [PATCH] autfilt: --highlight-word * bin/autfilt.cc: Add the option. * NEWS: Mention it. * tests/core/acc_word.test: Test it. * spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh (twa_run::project): New method. --- NEWS | 8 +++++ bin/autfilt.cc | 55 +++++++++++++++++++++++++++-- spot/twaalgos/emptiness.cc | 65 +++++++++++++++++++++++++++++++++- spot/twaalgos/emptiness.hh | 10 ++++++ tests/core/acc_word.test | 72 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 207 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index a2450b955..bb07e1899 100644 --- a/NEWS +++ b/NEWS @@ -28,6 +28,10 @@ New in spot 2.0.3a (not yet released) where NUM is a color number. Additionally --highlight-nondet=NUM is a shorthand for using the two. + * autfilt can now highlight a run matching a given word using the + --highlight-word=[NUM,]WORD option. However currently this only + work on automata with Fin-less acceptance. + * ltlcross and ltldo have a new syntax to specify that an input formula should be written in some given syntax after rewriting some operators away. For instance the defaults arguments passed @@ -85,6 +89,10 @@ New in spot 2.0.3a (not yet released) * language_containment_checker now has default values for all parameters of its constructor. + * spot::twa_run has a new method, project(), that can be used to + project a run found in a product onto one of the original operand. + This is for instance used by autfilt --highlight-word. + Python: * The __format__() method for formula support the same diff --git a/bin/autfilt.cc b/bin/autfilt.cc index b92d5c454..83ae1d9d3 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -61,6 +61,7 @@ #include #include #include +#include static const char argp_program_doc[] ="\ Convert, transform, and filter omega-automata.\v\ @@ -91,6 +92,7 @@ enum { OPT_HIGHLIGHT_NONDET, OPT_HIGHLIGHT_NONDET_EDGES, OPT_HIGHLIGHT_NONDET_STATES, + OPT_HIGHLIGHT_WORD, OPT_INSTUT, OPT_INCLUDED_IN, OPT_INHERENTLY_WEAK_SCCS, @@ -283,15 +285,19 @@ static const argp_option options[] = { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL, "minimize the automaton using a SAT solver (only works for deterministic" " automata)", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Decoration (for -d and -H1.1 output):", 8 }, { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM", - 0}, + 0 }, { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM", - 0}, + 0 }, { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic states and edges with color NUM", 0}, + { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0, + "highlight one run matching WORD using color NUM", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " @@ -349,6 +355,7 @@ static struct opt_t spot::remove_ap rem_ap; std::vector acc_words; std::vector rej_words; + std::vector> hl_words; }* opt; static bool opt_merge = false; @@ -518,6 +525,39 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_HIGHLIGHT_NONDET_EDGES: opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1; break; + case OPT_HIGHLIGHT_WORD: + { + char* endptr; + int res = strtol(arg, &endptr, 10); + if (endptr == arg) + { + res = 1; + } + else + { + if (res < 0) + error(2, 0, "failed to parse the argument of --highlight-word: " + "%d is not positive", res); + while (std::isspace(*endptr)) + ++endptr; + if (*endptr != ',') + error(2, 0, "failed to parse the argument of --highlight-word: " + "%d should be followed by a comma and WORD", res); + arg = endptr + 1; + } + try + { + opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict) + ->as_automaton(), res); + } + catch (const spot::parse_error& e) + { + error(2, 0, "failed to parse the argument of --highlight-word:\n%s", + e.what()); + } + } + break; + case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) opt_instut = 1; @@ -973,6 +1013,17 @@ namespace if (opt_highlight_nondet_edges >= 0) spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges); + if (!opt->hl_words.empty()) + for (auto& word_aut: opt->hl_words) + { + if (aut->acc().uses_fin_acceptance()) + error(2, 0, + "--highlight-word does not yet work with Fin acceptance"); + if (auto res = + spot::couvreur99(spot::product(aut, word_aut.first))->check()) + res->accepting_run()->project(aut)->highlight(word_aut.second); + } + const double conversion_time = sw.stop(); if (opt->uniq) diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index d0d05de23..b7c92e290 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -32,6 +32,7 @@ #include #include #include +#include namespace spot { @@ -434,6 +435,68 @@ namespace spot return res; } + twa_run_ptr twa_run::project(const const_twa_ptr& other, bool right) + { + unsigned shift = 0; + if (right) + shift = aut->num_sets() - other->num_sets(); + auto res = std::make_shared(other); + if (auto ps = aut->get_named_prop("product-states")) + { + auto a = std::dynamic_pointer_cast(aut); + if (!a) + throw std::runtime_error("twa_run::project() confused: " + "product-states found in a non-twa_graph"); + auto oth = std::dynamic_pointer_cast(other); + if (!oth) + throw std::runtime_error("twa_run::project() confused: " + "other ought to be a twa_graph"); + if (right) + { + for (auto& i: prefix) + { + unsigned s = (*ps)[a->state_number(i.s)].second; + res->prefix.emplace_back(oth->state_from_number(s), + i.label, i.acc >> shift); + } + for (auto& i: cycle) + { + unsigned s = (*ps)[a->state_number(i.s)].second; + res->cycle.emplace_back(oth->state_from_number(s), + i.label, i.acc >> shift); + } + } + else + { + auto all = oth->acc().all_sets(); + for (auto& i: prefix) + { + unsigned s = (*ps)[a->state_number(i.s)].first; + res->prefix.emplace_back(oth->state_from_number(s), + i.label, i.acc & all); + } + for (auto& i: cycle) + { + unsigned s = (*ps)[a->state_number(i.s)].first; + res->cycle.emplace_back(oth->state_from_number(s), + i.label, i.acc & all); + } + } + } + else + { + auto all = other->acc().all_sets(); + for (auto& i: prefix) + res->prefix.emplace_back(aut->project_state(i.s, other), + i.label, (i.acc >> shift) & all); + for (auto& i: cycle) + res->cycle.emplace_back(aut->project_state(i.s, other), + i.label, (i.acc >> shift) & all); + } + return res; + } + + bool twa_run::replay(std::ostream& os, bool debug) const { const state* s = aut->get_init_state(); @@ -677,7 +740,7 @@ namespace spot } for (auto& t: a->out(src)) - if (t.dst == dst && t.cond == label && t.acc == acc) + if (t.dst == dst && bdd_implies(label, t.cond) && t.acc == acc) { (*h)[a->get_graph().index_of_edge(t)] = color; break; diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 2b0be3b16..a9ce377b6 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -408,6 +408,16 @@ namespace spot /// but is no longer than this one. twa_run_ptr reduce() const; + /// \brief Project an accepting run + /// + /// This only works if the automaton associated to this run has + /// been created with otf_product() or product(), and \a other is + /// one of the two operands of the product. + /// + /// Use the \a right Boolean to specify whether \a other was a + /// left or right operand. + twa_run_ptr project(const const_twa_ptr& other, bool right = false); + /// \brief Replay a run. /// /// This is similar to os << run;, except that the diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index d80d0183c..8a9b195c3 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -20,6 +20,8 @@ . ./defs +set -e + # 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}' -q @@ -65,3 +67,73 @@ Missing ';' or '}' after formula EOF diff expect error + + +ltl2tgba 'a U b' | autfilt -H1.1 --highlight-word='cycle{b}' >out +cat >expected <out +cat >expected <stderr && exit 1 + test $? -eq 2 + cat stderr + grep 'failed to parse the argument of --highlight-word' stderr +done + + +# highlight-word does not yet work with Fin acceptance +ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1 +test $? -eq 2 +grep 'highlight-word.*Fin' stderr