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

langmap: adjust to only color non-unique languages

Fixes #203.

* spot/twaalgos/langmap.hh (highlight_languages): Simplify the
interface by only taking the automaton to color.
* spot/twaalgos/langmap.cc (highlight_languages): Only introduce
color for states that have a non-unique language.
* tests/core/highlightstate.test: Update and add more tests.
* tests/python/langmap.py: Keep the tests simple.
* bin/autfilt.cc: Adjust usage and help string.
parent aa457a20
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -338,7 +338,7 @@ static const argp_option options[] = ...@@ -338,7 +338,7 @@ static const argp_option options[] =
{ "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0, { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
"highlight one run matching WORD using color NUM", 0}, "highlight one run matching WORD using color NUM", 0},
{ "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 , { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
"highlight states that recognize same language with same color", 0}, "highlight states that recognize identical languages", 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, "
...@@ -1219,7 +1219,7 @@ namespace ...@@ -1219,7 +1219,7 @@ namespace
spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges); spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges);
if (opt_highlight_languages) if (opt_highlight_languages)
spot::highlight_languages(aut, spot::language_map(aut)); spot::highlight_languages(aut);
if (!opt->hl_words.empty()) if (!opt->hl_words.empty())
for (auto& word_aut: opt->hl_words) for (auto& word_aut: opt->hl_words)
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. // Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -26,18 +27,6 @@ ...@@ -26,18 +27,6 @@
namespace spot namespace spot
{ {
void highlight_languages(twa_graph_ptr& aut,
const std::vector<unsigned>& v)
{
auto hs = new std::map<unsigned, unsigned>;
aut->set_named_prop("highlight-states", hs);
unsigned n_states = aut->num_states();
for (unsigned i = 0; i < n_states; ++i)
(*hs)[i] = v[i];
}
std::vector<unsigned> std::vector<unsigned>
language_map(const const_twa_graph_ptr& aut) language_map(const const_twa_graph_ptr& aut)
{ {
...@@ -80,4 +69,38 @@ namespace spot ...@@ -80,4 +69,38 @@ namespace spot
return res; return res;
} }
void highlight_languages(twa_graph_ptr& aut)
{
std::vector<unsigned> lang = language_map(aut);
unsigned lang_sz = lang.size();
std::vector<unsigned> cnt(lang_sz, 0);
for (unsigned v: lang)
{
assert(v < lang_sz);
++cnt[v];
}
unsigned color = 0;
auto hs = new std::map<unsigned, unsigned>;
aut->set_named_prop("highlight-states", hs);
assert(lang_sz == aut->num_states());
// Give a unique color number to each state that has not a unique
// language. This assumes that lang[i] <= i, as guaranteed by
// language_map.
for (unsigned i = 0; i < lang_sz; ++i)
{
unsigned v = lang[i];
if (cnt[v] > 1)
{
if (v == i)
lang[i] = color++;
else
assert(v < i);
(*hs)[i] = lang[v];
}
}
}
} }
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. // Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -34,7 +35,9 @@ namespace spot ...@@ -34,7 +35,9 @@ namespace spot
SPOT_API std::vector<unsigned> SPOT_API std::vector<unsigned>
language_map(const const_twa_graph_ptr& aut); language_map(const const_twa_graph_ptr& aut);
/// \brief Color automaton's states that recognize the same language. /// \brief Color state that recognize identical language.
///
/// State that recognize a unique language will not be colored.
SPOT_API void SPOT_API void
highlight_languages(twa_graph_ptr& aut, const std::vector<unsigned>& v); highlight_languages(twa_graph_ptr& aut);
} }
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement # Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -21,8 +21,6 @@ ...@@ -21,8 +21,6 @@
. ./defs . ./defs
set -e set -e
autfilt=autfilt
cat >aut.hoa <<'EOF' cat >aut.hoa <<'EOF'
HOA: v1 HOA: v1
States: 4 States: 4
...@@ -53,13 +51,65 @@ State: 3 {1 3} ...@@ -53,13 +51,65 @@ State: 3 {1 3}
3 3
2 2
--END-- --END--
HOA: v1
name: "Fb & GF((a & Xb) | (!a & X!b))"
States: 5
Start: 0
AP: 2 "b" "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0&!1] 0
[0] 1
[!0&1] 2
State: 1
[!1] 3
[1] 4
State: 2
[!0&!1] 0 {0}
[!0&1] 2 {0}
[0&!1] 3
[0&1] 4
State: 3
[!0] 1 {1}
[0&!1] 3
[0&1] 4
State: 4
[0] 1 {1}
[!0&!1] 3
[!0&1] 4
--END--
HOA: v1
name: "X(a & FGb)"
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[t] 1
State: 1
[0&!1] 2
[0&1] 3
State: 2
[!1] 2
[1] 3
State: 3
[!1] 2 {0}
[1] 3 {1}
--END--
EOF EOF
cat >expected << 'EOF' cat >expected << 'EOF'
spot.highlight.states: 0 0 1 0 2 0 3 0 spot.highlight.states: 0 0 1 0 2 0 3 0
spot.highlight.states: 0 0 1 1 2 0 3 1 4 1
spot.highlight.states: 2 0 3 0
EOF EOF
$autfilt aut.hoa --highlight-languages -H1.1 | grep -e 'spot.highlight.states'\ autfilt aut.hoa --highlight-languages -H1.1 | grep spot.highlight.states >res
> res
diff expected res diff expected res
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. # Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE)
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
...@@ -17,88 +18,38 @@ ...@@ -17,88 +18,38 @@
# along with this program. If not, see <http:#www.gnu.org/licenses/>. # along with this program. If not, see <http:#www.gnu.org/licenses/>.
import spot import spot
import re
import sys import sys
def test_langmap_functions_for(aut, expected): def hstates(txt):
# First, let's get aut's languages map as v. for line in txt.split('\n'):
v = '' if line.startswith('spot.highlight.states:'):
try: return line[23:]
v = spot.language_map(aut) return ''
except Exception as e:
# If aut is not deterministic and the exception is as expected then
# it is ok. def test(f, opt, expected):
if 'language_map only works with deterministic automata' in str(e)\ aut = spot.translate(f, opt, 'deterministic')
and not spot.is_deterministic(aut): v = spot.language_map(aut)
return assert len(v) == aut.num_states()
else: spot.highlight_languages(aut)
print(e, file=sys.stderr) l = hstates(aut.to_str('hoa', '1.1'))
exit(1) if l != expected:
print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l),
# Now let's check highligthed states. file=sys.stderr)
spot.highlight_languages(aut, v) exit(1)
lines = aut.to_str('hoa', '1.1').split('\n')
colors_l = []
for line in lines: test('GF(a) & GFb & c', 'BA', '1 0 2 0 3 0')
if 'spot.highlight.states' in line: test('GF(a) & c & X!a', 'BA', '2 0 3 0')
l = [int(w) for w in \ test('(a U b) & GF(c & Xd)', 'generic', '1 0 2 0')
re.search(': (.+?)$', line).group(1).split(' ')] test('GF(a <-> Xb) & Fb', 'generic', '0 0 1 1 2 0 3 1 4 1')
if l[1::2] != expected: test('Xa', 'BA', '')
print('expected:' + repr(expected) +
' but got:' + repr(l[1::2]), file=sys.stderr) # Non-deterministic automata are not supported
exit(1) try:
test('FGa', 'BA', '')
aut_l = [] except RuntimeError as e:
expected_l = [] assert 'language_map only works with deterministic automata'in str(e)
else:
aut_l.append(spot.translate('(a U b) & GFc & GFd', 'BA', 'deterministic')) exit(1)
expected_l.append([0, 1, 1, 1])
aut_l.append(spot.translate('GF(a <-> b) | c', 'BA', 'deterministic'))
expected_l.append([0, 1, 2, 2])
aut_l.append(spot.translate('GF(a <-> b) | c | X!a', 'BA', 'deterministic'))
expected_l.append([0, 1, 2, 3, 3])
aut = spot.automaton("""
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--
""")
aut_l.append(aut)
expected_l.append([0, 0, 0, 0])
# Add a non deterministic test:
aut_l.append(spot.translate('GF(a <-> XXb) | Xc', 'BA'))
expected_l.append([])
len_aut = len(aut_l)
for i in range(0, len_aut):
test_langmap_functions_for(aut_l[i], expected_l[i])
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