bin/autfilt.cc: Add '--highlight-languages' option

* bin/autfilt.cc: Add that option.
* tests/core/highlightstate.test: Add test.
* NEWS: Update.
parent 8a0eed6c
......@@ -16,6 +16,9 @@ New in spot 2.2.2.dev (Not yet released)
* the --check option can now take "semi-determinism" as argument.
* autfilt has a new option '--highlight-languages' that helps to see
graphically which states of an automaton recognize the same languages.
Library:
* A twa is required to have at least one state, the initial state.
......
......@@ -66,6 +66,7 @@
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/langmap.hh>
static const char argp_program_doc[] ="\
Convert, transform, and filter omega-automata.\v\
......@@ -98,6 +99,7 @@ enum {
OPT_HIGHLIGHT_NONDET_EDGES,
OPT_HIGHLIGHT_NONDET_STATES,
OPT_HIGHLIGHT_WORD,
OPT_HIGHLIGHT_LANGUAGES,
OPT_INSTUT,
OPT_INCLUDED_IN,
OPT_INHERENTLY_WEAK_SCCS,
......@@ -329,6 +331,8 @@ static const argp_option options[] =
"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},
{ "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
"highlight states that recognize same language with same color", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0,
"If any option among --small, --deterministic, or --any is given, "
......@@ -470,6 +474,7 @@ static bool opt_sep_sets = false;
static const char* opt_sat_minimize = nullptr;
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
static bool opt_highlight_languages = false;
static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
......@@ -631,7 +636,9 @@ parse_opt(int key, char* arg, struct argp_state*)
}
}
break;
case OPT_HIGHLIGHT_LANGUAGES:
opt_highlight_languages = true;
break;
case OPT_INSTUT:
if (!arg || (arg[0] == '1' && arg[1] == 0))
opt_instut = 1;
......@@ -1205,6 +1212,9 @@ namespace
if (opt_highlight_nondet_edges >= 0)
spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges);
if (opt_highlight_languages)
spot::highlight_languages(aut, spot::language_map(aut));
if (!opt->hl_words.empty())
for (auto& word_aut: opt->hl_words)
{
......
#!/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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
autfilt=autfilt
cat >aut.hoa <<'EOF'
HOA: v1
States: 4
properties: implicit-labels trans-labels no-univ-branch deterministic complete
acc-name: Rabin 2
Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3))
Start: 0
AP: 2 "p0" "p1"
--BODY--
State: 0 {0}
1
0
3
2
State: 1 {1}
1
0
3
2
State: 2 {0 3}
1
0
3
2
State: 3 {1 3}
1
0
3
2
--END--
EOF
cat >expected << 'EOF'
spot.highlight.states: 0 0 1 0 2 0 3 0
EOF
$autfilt aut.hoa --highlight-languages -H1.1 | grep -e 'spot.highlight.states'\
> res
diff expected res
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