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.
This commit is contained in:
Alexandre GBAGUIDI AISSE
parent
9a204b770f
commit
8a0eed6cef
6 changed files with 234 additions and 0 deletions
3
NEWS
3
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
|
||||
|
|
|
|||
|
|
@ -137,6 +137,7 @@
|
|||
#include <spot/twaalgos/stats.hh>
|
||||
#include <spot/twaalgos/isdet.hh>
|
||||
#include <spot/twaalgos/isunamb.hh>
|
||||
#include <spot/twaalgos/langmap.hh>
|
||||
#include <spot/twaalgos/simulation.hh>
|
||||
#include <spot/twaalgos/postproc.hh>
|
||||
#include <spot/twaalgos/product.hh>
|
||||
|
|
@ -524,6 +525,7 @@ def state_is_accepting(self, src) -> "bool":
|
|||
%include <spot/twaalgos/ltl2tgba_fm.hh>
|
||||
%include <spot/twaalgos/compsusp.hh>
|
||||
%include <spot/twaalgos/determinize.hh>
|
||||
%include <spot/twaalgos/langmap.hh>
|
||||
%include <spot/twaalgos/magic.hh>
|
||||
%include <spot/twaalgos/minimize.hh>
|
||||
%include <spot/twaalgos/neverclaim.hh>
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
83
spot/twaalgos/langmap.cc
Normal file
83
spot/twaalgos/langmap.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <numeric>
|
||||
#include <spot/twa/twa.hh>
|
||||
#include <spot/twaalgos/complement.hh>
|
||||
#include <spot/twaalgos/copy.hh>
|
||||
#include <spot/twaalgos/isdet.hh>
|
||||
#include <spot/twaalgos/langmap.hh>
|
||||
#include <spot/twaalgos/remfin.hh>
|
||||
|
||||
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>
|
||||
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<unsigned> res(n_states);
|
||||
std::iota(std::begin(res), std::end(res), 0);
|
||||
|
||||
std::vector<twa_graph_ptr> alt_init_st_auts(n_states);
|
||||
std::vector<twa_graph_ptr> 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;
|
||||
}
|
||||
}
|
||||
40
spot/twaalgos/langmap.hh
Normal file
40
spot/twaalgos/langmap.hh
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <vector>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
|
||||
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<unsigned>
|
||||
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<unsigned>& v);
|
||||
}
|
||||
104
tests/python/langmap.py
Normal file
104
tests/python/langmap.py
Normal file
|
|
@ -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 <http:#www.gnu.org/licenses/>.
|
||||
|
||||
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])
|
||||
Loading…
Add table
Add a link
Reference in a new issue