diff --git a/bin/autfilt.cc b/bin/autfilt.cc index f0aa9bd48..41ce76c9f 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -338,7 +338,7 @@ static const argp_option options[] = { "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}, + "highlight states that recognize identical languages", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " @@ -1219,7 +1219,7 @@ namespace spot::highlight_nondet_edges(aut, opt_highlight_nondet_edges); if (opt_highlight_languages) - spot::highlight_languages(aut, spot::language_map(aut)); + spot::highlight_languages(aut); if (!opt->hl_words.empty()) for (auto& word_aut: opt->hl_words) diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc index e81c1fa90..0899547c2 100644 --- a/spot/twaalgos/langmap.cc +++ b/spot/twaalgos/langmap.cc @@ -1,5 +1,6 @@ // -*- 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. // @@ -26,18 +27,6 @@ namespace spot { - void highlight_languages(twa_graph_ptr& aut, - const std::vector& v) - { - auto hs = new std::map; - 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 language_map(const const_twa_graph_ptr& aut) { @@ -80,4 +69,38 @@ namespace spot return res; } + + void highlight_languages(twa_graph_ptr& aut) + { + std::vector lang = language_map(aut); + unsigned lang_sz = lang.size(); + std::vector cnt(lang_sz, 0); + for (unsigned v: lang) + { + assert(v < lang_sz); + ++cnt[v]; + } + + unsigned color = 0; + auto hs = new std::map; + 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]; + } + } + } } diff --git a/spot/twaalgos/langmap.hh b/spot/twaalgos/langmap.hh index f16a813a4..afebe811c 100644 --- a/spot/twaalgos/langmap.hh +++ b/spot/twaalgos/langmap.hh @@ -1,5 +1,6 @@ // -*- 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. // @@ -34,7 +35,9 @@ namespace spot SPOT_API std::vector 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 - highlight_languages(twa_graph_ptr& aut, const std::vector& v); + highlight_languages(twa_graph_ptr& aut); } diff --git a/tests/core/highlightstate.test b/tests/core/highlightstate.test index 6c8952903..618a22b50 100755 --- a/tests/core/highlightstate.test +++ b/tests/core/highlightstate.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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). # # This file is part of Spot, a model checking library. @@ -21,8 +21,6 @@ . ./defs set -e -autfilt=autfilt - cat >aut.hoa <<'EOF' HOA: v1 States: 4 @@ -53,13 +51,65 @@ State: 3 {1 3} 3 2 --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 cat >expected << 'EOF' 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 -$autfilt aut.hoa --highlight-languages -H1.1 | grep -e 'spot.highlight.states'\ - > res - +autfilt aut.hoa --highlight-languages -H1.1 | grep spot.highlight.states >res diff expected res diff --git a/tests/python/langmap.py b/tests/python/langmap.py index 35a7c50f8..5d4ce3cd5 100644 --- a/tests/python/langmap.py +++ b/tests/python/langmap.py @@ -1,5 +1,6 @@ # -*- 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. # @@ -17,88 +18,38 @@ # along with this program. If not, see . import spot -import re import sys -def test_langmap_functions_for(aut, expected): - # First, let's get aut's languages map as v. - v = '' - try: - v = spot.language_map(aut) - except Exception as e: - # If aut is not deterministic and the exception is as expected then - # it is ok. - if 'language_map only works with deterministic automata' in str(e)\ - and not spot.is_deterministic(aut): - return - else: - print(e, file=sys.stderr) - exit(1) +def hstates(txt): + for line in txt.split('\n'): + if line.startswith('spot.highlight.states:'): + return line[23:] + return '' - # Now let's check highligthed states. - spot.highlight_languages(aut, v) - lines = aut.to_str('hoa', '1.1').split('\n') - colors_l = [] - for line in lines: - if 'spot.highlight.states' in line: - l = [int(w) for w in \ - re.search(': (.+?)$', line).group(1).split(' ')] - if l[1::2] != expected: - print('expected:' + repr(expected) + - ' but got:' + repr(l[1::2]), file=sys.stderr) - exit(1) -aut_l = [] -expected_l = [] +def test(f, opt, expected): + aut = spot.translate(f, opt, 'deterministic') + v = spot.language_map(aut) + assert len(v) == aut.num_states() + spot.highlight_languages(aut) + l = hstates(aut.to_str('hoa', '1.1')) + if l != expected: + print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l), + file=sys.stderr) + exit(1) -aut_l.append(spot.translate('(a U b) & GFc & GFd', 'BA', 'deterministic')) -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]) +test('GF(a) & GFb & c', 'BA', '1 0 2 0 3 0') +test('GF(a) & c & X!a', 'BA', '2 0 3 0') +test('(a U b) & GF(c & Xd)', 'generic', '1 0 2 0') +test('GF(a <-> Xb) & Fb', 'generic', '0 0 1 1 2 0 3 1 4 1') +test('Xa', 'BA', '') -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]) +# Non-deterministic automata are not supported +try: + test('FGa', 'BA', '') +except RuntimeError as e: + assert 'language_map only works with deterministic automata'in str(e) +else: + exit(1)