Commit b13caea3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 6793d6de
...@@ -28,6 +28,10 @@ New in spot 2.0.3a (not yet released) ...@@ -28,6 +28,10 @@ New in spot 2.0.3a (not yet released)
where NUM is a color number. Additionally --highlight-nondet=NUM where NUM is a color number. Additionally --highlight-nondet=NUM
is a shorthand for using the two. 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 * ltlcross and ltldo have a new syntax to specify that an input
formula should be written in some given syntax after rewriting formula should be written in some given syntax after rewriting
some operators away. For instance the defaults arguments passed some operators away. For instance the defaults arguments passed
...@@ -85,6 +89,10 @@ New in spot 2.0.3a (not yet released) ...@@ -85,6 +89,10 @@ New in spot 2.0.3a (not yet released)
* language_containment_checker now has default values for all * language_containment_checker now has default values for all
parameters of its constructor. 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: Python:
* The __format__() method for formula support the same * The __format__() method for formula support the same
......
...@@ -61,6 +61,7 @@ ...@@ -61,6 +61,7 @@
#include <spot/twaalgos/hoa.hh> #include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh> #include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/gtec/gtec.hh>
static const char argp_program_doc[] ="\ static const char argp_program_doc[] ="\
Convert, transform, and filter omega-automata.\v\ Convert, transform, and filter omega-automata.\v\
...@@ -91,6 +92,7 @@ enum { ...@@ -91,6 +92,7 @@ enum {
OPT_HIGHLIGHT_NONDET, OPT_HIGHLIGHT_NONDET,
OPT_HIGHLIGHT_NONDET_EDGES, OPT_HIGHLIGHT_NONDET_EDGES,
OPT_HIGHLIGHT_NONDET_STATES, OPT_HIGHLIGHT_NONDET_STATES,
OPT_HIGHLIGHT_WORD,
OPT_INSTUT, OPT_INSTUT,
OPT_INCLUDED_IN, OPT_INCLUDED_IN,
OPT_INHERENTLY_WEAK_SCCS, OPT_INHERENTLY_WEAK_SCCS,
...@@ -283,15 +285,19 @@ static const argp_option options[] = ...@@ -283,15 +285,19 @@ static const argp_option options[] =
{ "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL, { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
"minimize the automaton using a SAT solver (only works for deterministic" "minimize the automaton using a SAT solver (only works for deterministic"
" automata)", 0 }, " automata)", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Decoration (for -d and -H1.1 output):", 8 },
{ "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM", { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
0}, 0 },
{ "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM", { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM", OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
0}, 0 },
{ "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM", { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
OPTION_ARG_OPTIONAL, OPTION_ARG_OPTIONAL,
"highlight nondeterministic states and edges with color NUM", 0}, "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, { nullptr, 0, nullptr, 0,
"If any option among --small, --deterministic, or --any is given, " "If any option among --small, --deterministic, or --any is given, "
...@@ -349,6 +355,7 @@ static struct opt_t ...@@ -349,6 +355,7 @@ static struct opt_t
spot::remove_ap rem_ap; spot::remove_ap rem_ap;
std::vector<spot::twa_graph_ptr> acc_words; std::vector<spot::twa_graph_ptr> acc_words;
std::vector<spot::twa_graph_ptr> rej_words; std::vector<spot::twa_graph_ptr> rej_words;
std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
}* opt; }* opt;
static bool opt_merge = false; static bool opt_merge = false;
...@@ -518,6 +525,39 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -518,6 +525,39 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_HIGHLIGHT_NONDET_EDGES: case OPT_HIGHLIGHT_NONDET_EDGES:
opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1; opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1;
break; 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: case OPT_INSTUT:
if (!arg || (arg[0] == '1' && arg[1] == 0)) if (!arg || (arg[0] == '1' && arg[1] == 0))
opt_instut = 1; opt_instut = 1;
...@@ -973,6 +1013,17 @@ namespace ...@@ -973,6 +1013,17 @@ namespace
if (opt_highlight_nondet_edges >= 0) if (opt_highlight_nondet_edges >= 0)
spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges); 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(); const double conversion_time = sw.stop();
if (opt->uniq) if (opt->uniq)
......
...@@ -32,6 +32,7 @@ ...@@ -32,6 +32,7 @@
#include <spot/twaalgos/tau03.hh> #include <spot/twaalgos/tau03.hh>
#include <spot/twaalgos/tau03opt.hh> #include <spot/twaalgos/tau03opt.hh>
#include <spot/twa/bddprint.hh> #include <spot/twa/bddprint.hh>
#include <spot/twaalgos/product.hh>
namespace spot namespace spot
{ {
...@@ -434,6 +435,68 @@ namespace spot ...@@ -434,6 +435,68 @@ namespace spot
return res; 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<twa_run>(other);
if (auto ps = aut->get_named_prop<const product_states>("product-states"))
{
auto a = std::dynamic_pointer_cast<const twa_graph>(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<const twa_graph>(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 bool twa_run::replay(std::ostream& os, bool debug) const
{ {
const state* s = aut->get_init_state(); const state* s = aut->get_init_state();
...@@ -677,7 +740,7 @@ namespace spot ...@@ -677,7 +740,7 @@ namespace spot
} }
for (auto& t: a->out(src)) 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; (*h)[a->get_graph().index_of_edge(t)] = color;
break; break;
......
...@@ -408,6 +408,16 @@ namespace spot ...@@ -408,6 +408,16 @@ namespace spot
/// but is no longer than this one. /// but is no longer than this one.
twa_run_ptr reduce() const; 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. /// \brief Replay a run.
/// ///
/// This is similar to <code>os << run;</code>, except that the /// This is similar to <code>os << run;</code>, except that the
......
...@@ -20,6 +20,8 @@ ...@@ -20,6 +20,8 @@
. ./defs . ./defs
set -e
# The --accept-word option filters automata that accept the given word # The --accept-word option filters automata that accept the given word
# If several words are given, it filters automata that accept ALL words # If several words are given, it filters automata that accept ALL words
ltl2tgba 'G!a' | autfilt --accept-word 'b; cycle{!a}' -q ltl2tgba 'G!a' | autfilt --accept-word 'b; cycle{!a}' -q
...@@ -65,3 +67,73 @@ Missing ';' or '}' after formula ...@@ -65,3 +67,73 @@ Missing ';' or '}' after formula
EOF EOF
diff expect error diff expect error
ltl2tgba 'a U b' | autfilt -H1.1 --highlight-word='cycle{b}' >out
cat >expected <<EOF
HOA: v1.1
name: "a U b"
States: 2
Start: 1
AP: 2 "b" "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal
spot.highlight.edges: 1 1 2 1
--BODY--
State: 0 {0}
[t] 0
State: 1
[0] 0
[!0&1] 1
--END--
EOF
diff expected out
ltl2tgba 'Fa & Fb' |
autfilt -H1.1 \
--highlight-word='2,!a&!b;cycle{!a&b;a&b}' \
--highlight-word='3,!a&!b;cycle{a&!b;a&b}' >out
cat >expected <<EOF
HOA: v1.1
name: "Fa & Fb"
States: 4
Start: 2
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant terminal
spot.highlight.edges: 1 3 2 3 5 3 6 3 7 2 8 2
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[!1] 1
State: 2
[0&1] 0
[0&!1] 1
[!0&!1] 2
[!0&1] 3
State: 3
[0] 0
[!0] 3
--END--
EOF
diff expected out
for w in ',!a&!b;cycle{!a&b;a&b}' '-1,cycle{a}' '1 cycle{a}'; do
autfilt --highlight-word="$w" </dev/null 2>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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment