From 8a0eed6cef82fab09412003f2de6a813d27ec05b Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Mon, 12 Dec 2016 16:45:03 +0100 Subject: [PATCH] twaalgos: Implement language_map algo * python/spot/impl.i: Add python bindings. * spot/twaalgos/langmap.cc: Implement algo. * spot/twaalgos/langmap.hh: Declare algo. * spot/twaalgos/Makefile.am: Add new files. * tests/python/langmap.py: Add tests. * NEWS: Update. --- NEWS | 3 ++ python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/langmap.cc | 83 ++++++++++++++++++++++++++++++ spot/twaalgos/langmap.hh | 40 +++++++++++++++ tests/python/langmap.py | 104 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 234 insertions(+) create mode 100644 spot/twaalgos/langmap.cc create mode 100644 spot/twaalgos/langmap.hh create mode 100644 tests/python/langmap.py diff --git a/NEWS b/NEWS index 623151421..94a931af9 100644 --- a/NEWS +++ b/NEWS @@ -74,6 +74,9 @@ New in spot 2.2.2.dev (Not yet released) deterministic/semi-deterministic/unambiguous should be preserved only if they are positive. + * language_map() and highlight_languages() are new functions used to + implement the --highlight-languages command line option described above. + Build: * The configure script has a new option --enable-c++14, to compile in diff --git a/python/spot/impl.i b/python/spot/impl.i index 11dd17120..cff9ca1c9 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -137,6 +137,7 @@ #include #include #include +#include #include #include #include @@ -524,6 +525,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 00d3b8bb4..352d88e76 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -50,6 +50,7 @@ twaalgos_HEADERS = \ isdet.hh \ isunamb.hh \ isweakscc.hh \ + langmap.hh \ lbtt.hh \ ltl2taa.hh \ ltl2tgba_fm.hh \ @@ -106,6 +107,7 @@ libtwaalgos_la_SOURCES = \ isdet.cc \ isunamb.cc \ isweakscc.cc \ + langmap.cc \ lbtt.cc \ ltl2taa.cc \ ltl2tgba_fm.cc \ diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc new file mode 100644 index 000000000..e81c1fa90 --- /dev/null +++ b/spot/twaalgos/langmap.cc @@ -0,0 +1,83 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. +// +// 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 . + +#include +#include +#include +#include +#include +#include +#include + +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) + { + if (!is_deterministic(aut)) + throw std::runtime_error( + "language_map only works with deterministic automata"); + + unsigned n_states = aut->num_states(); + std::vector res(n_states); + std::iota(std::begin(res), std::end(res), 0); + + std::vector alt_init_st_auts(n_states); + std::vector compl_alt_init_st_auts(n_states); + + // Prepare all automatons needed. + for (unsigned i = 0; i < n_states; ++i) + { + twa_graph_ptr c = copy(aut, twa::prop_set::all()); + c->set_init_state(i); + alt_init_st_auts[i] = c; + + twa_graph_ptr cc = + remove_fin(dtwa_complement(copy(c, twa::prop_set::all()))); + compl_alt_init_st_auts[i] = cc; + } + + for (unsigned i = 1; i < n_states; ++i) + for (unsigned j = 0; j < i; ++j) + { + if (res[j] != j) + continue; + + if (!alt_init_st_auts[i]->intersects(compl_alt_init_st_auts[j]) + && (!compl_alt_init_st_auts[i]->intersects(alt_init_st_auts[j]))) + { + res[i] = res[j]; + break; + } + } + + return res; + } +} diff --git a/spot/twaalgos/langmap.hh b/spot/twaalgos/langmap.hh new file mode 100644 index 000000000..f16a813a4 --- /dev/null +++ b/spot/twaalgos/langmap.hh @@ -0,0 +1,40 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. +// +// 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 . + +#pragma once + +#include +#include + +namespace spot +{ + /// \brief Identify states that recognize the same language. + /// + /// The returned vector is the same size as the automaton's number of state. + /// The number of different values (ignoring occurences) in the vector is the + /// total number of recognized languages, states recognizing the same + /// language have the same value. + /// + /// The given automaton must be deterministic. + SPOT_API std::vector + language_map(const const_twa_graph_ptr& aut); + + /// \brief Color automaton's states that recognize the same language. + SPOT_API void + highlight_languages(twa_graph_ptr& aut, const std::vector& v); +} diff --git a/tests/python/langmap.py b/tests/python/langmap.py new file mode 100644 index 000000000..35a7c50f8 --- /dev/null +++ b/tests/python/langmap.py @@ -0,0 +1,104 @@ +# -*- coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement de l'Epita. +# +# 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 . + +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) + + # 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 = [] + +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]) + +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]) -- GitLab