alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

introduce the original-classes named property

Browse source 
* doc/org/concepts.org, NEWS: Document it.
* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/sbacc.cc, spot/twaalgos/sbacc.hh: Use it.
* spot/twa/twagraph.cc: Update it on defrag.
* spot/twa/twa.cc (copy_named_properties_of): Copy it.
* tests/python/det.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i (get_original_states, get_original_classes): New
methods, to help with the tests.
This commit is contained in:
Alexandre Duret-Lutz 2021-12-17 17:51:06 +01:00
parent d8f245a7de
commit 20bcc216a0
11 changed files with 170 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

18
NEWS
View file

@ -1,5 +1,23 @@
New in spot 2.10.2.dev (not yet released)
Library:
- "original-classes" is a new named property similar to
"original-states". It maps an each state to an unsigned integer
such that if two classes are in the same class, they are expected
to recognize the same language. The "original-states" should be
prefered property when that integer correspond to some actual
state.
- tgba_determinize() learned to fill the "original-classes" property.
States of the determinized automaton that correspond to the same
subset of states of the original automaton belong to the same
class. Filling this property is only done on demand has it inccurs
on small overhead.
- sbacc() learned to take the "original-classes" property into
account and preserve it.
Bugs fixed:
- On automata where the absence of color is not rejecting

1
doc/org/concepts.org
View file

@ -1138,6 +1138,7 @@ Here is a list of named properties currently used inside Spot:
| ~highlight-edges~ | ~std::map<unsigned, unsigned>~ | map of (edge number, color number) for highlighting the output |
| ~highlight-states~ | ~std::map<unsigned, unsigned>~ | map of (state number, color number) for highlighting the output |
| ~incomplete-states~ | ~std::set<unsigned>~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) |
| ~original-classes~ | ~std::vector<unsigned>~ | class number associated to each state of a construction (used by some algorithms like =tgba_deternize()=) |
| ~original-clauses~ | ~std::vector<unsigned>~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= |
| ~original-states~ | ~std::vector<unsigned>~ | original state number before transformation (used by some algorithms like =degeneralize()=) |
| ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton |

9
python/spot/impl.i
View file

@ -983,6 +983,15 @@ static void* ptr_for_bdddict(PyObject* obj)
<std::vector<std::pair<unsigned, unsigned>>>("product-states");
}
std::vector<unsigned>* get_original_states()
{
return self->get_named_prop<std::vector<unsigned>>("original-states");
}
std::vector<unsigned>* get_original_classes()
{
return self->get_named_prop<std::vector<unsigned>>("original-classes");
}
twa* highlight_state(unsigned state, unsigned color)
{

1
spot/twa/twa.cc
View file

@ -303,6 +303,7 @@ namespace spot
COPY_PROP(hlmap, "highlight-edges");
COPY_PROP(hlmap, "highlight-states");
COPY_PROP(std::set<unsigned>, "incomplete-states");
COPY_PROP(std::vector<unsigned>, "original-classes");
COPY_PROP(std::vector<unsigned>, "original-clauses");
COPY_PROP(std::vector<unsigned>, "original-states");
COPY_PROP(spot::product_states, "product-states");

42
spot/twa/twagraph.cc
View file

@ -908,32 +908,22 @@ namespace spot
}
std::swap(*hs, hs2);
}
if (auto os = get_named_prop<std::vector<unsigned>>("original-states"))
{
unsigned size = os->size();
for (unsigned s = 0; s < size; ++s)
{
unsigned dst = newst[s];
if (dst == s || dst == -1U)
continue;
assert(dst < s);
(*os)[dst] = (*os)[s];
}
os->resize(used_states);
}
if (auto dl = get_named_prop<std::vector<unsigned>>("degen-levels"))
{
unsigned size = dl->size();
for (unsigned s = 0; s < size; ++s)
{
unsigned dst = newst[s];
if (dst == s || dst == -1U)
continue;
assert(dst < s);
(*dl)[dst] = (*dl)[s];
}
dl->resize(used_states);
}
for (const char* prop: {"original-classes",
"original-states",
"degen-levels"})
if (auto os = get_named_prop<std::vector<unsigned>>(prop))
{
unsigned size = os->size();
for (unsigned s = 0; s < size; ++s)
{
unsigned dst = newst[s];
if (dst == s || dst == -1U)
continue;
assert(dst < s);
(*os)[dst] = (*os)[s];
}
os->resize(used_states);
}
if (auto ss = get_named_prop<std::vector<unsigned>>("simulated-states"))
{
for (auto& s : *ss)

53
spot/twaalgos/determinize.cc
View file

@ -548,6 +548,35 @@ namespace spot
return res;
}
std::vector<unsigned>*
classify(const power_set& states,
const std::vector<unsigned>* original_class)
{
unsigned sz = states.size();
auto classes = new std::vector<unsigned>(sz);
std::vector<std::set<unsigned>> state_sets(sz);
for (const auto& p: states)
{
// Get the set of original stats of this
std::set<unsigned> s;
for (auto& n: p.first.nodes_)
{
unsigned st = n.first;
if (original_class)
st = (*original_class)[st];
s.insert(st);
}
state_sets[p.second] = std::move(s);
}
std::map<std::set<unsigned>, unsigned> seensets;
for (unsigned s = 0; s < sz; ++s)
{
auto p = seensets.emplace(state_sets[s], s);
(*classes)[s] = p.first->second;
}
return classes;
}
class safra_support
{
const std::vector<bdd>& state_supports;
@ -812,7 +841,8 @@ namespace spot
bool pretty_print, bool use_scc,
bool use_simulation, bool use_stutter,
const output_aborter* aborter,
int trans_pruning)
int trans_pruning,
bool want_classes)
{
if (!a->is_existential())
throw std::runtime_error
@ -996,6 +1026,27 @@ namespace spot
if (pretty_print)
res->set_named_prop("state-names", print_debug(aut, seen));
if (want_classes)
{
auto* ptr =
aut->get_named_prop<std::vector<unsigned>>("original-states");
if (ptr && ptr->size() != aut->num_states())
throw std::runtime_error("tgba_determinize(): "
"input's \"original-states\" property "
"has unexpected size");
if (!ptr)
{
ptr =
aut->get_named_prop<std::vector<unsigned>>("original-classes");
if (ptr && ptr->size() != aut->num_states())
throw std::runtime_error("tgba_determinize(): "
"input's \"original-classes\" property "
"has unexpected size");
}
res->set_named_prop("original-classes", classify(seen, ptr));
}
return res;
}
}

13
spot/twaalgos/determinize.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2016, 2019-2020 Laboratoire de Recherche et
// Copyright (C) 2015-2016, 2019-2021 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -81,6 +81,14 @@ namespace spot
/// \param trans_pruning when \a use_simulation is true, \a trans_pruning
/// is passed to the simulation-based reduction to limit
/// the effect of transition pruning.
///
/// \param want_classes If set, define a "original-class" named property
/// as a vector of unsigned. If two states are associated
/// to the same integer, it means they use the same subset
/// of original states as support, so they recognize the
/// same language. If the input define an "original-state"
/// property (or else an "original-class" property), it is
/// taken into account while computing the above support.
SPOT_API twa_graph_ptr
tgba_determinize(const const_twa_graph_ptr& aut,
bool pretty_print = false,
@ -88,5 +96,6 @@ namespace spot
bool use_simulation = true,
bool use_stutter = true,
const output_aborter* aborter = nullptr,
int trans_pruning = -1);
int trans_pruning = -1,
bool want_classes = false);
}

27
spot/twaalgos/sbacc.cc
View file

@ -95,7 +95,6 @@ namespace spot
std::vector<std::pair<pair_t, unsigned>> todo;
auto* origin = new std::vector<unsigned>;
origin->reserve(ns);
res->set_named_prop("original-states", origin);
auto new_state =
[&](unsigned state, acc_cond::mark_t m) -> unsigned
@ -186,11 +185,27 @@ namespace spot
}
res->merge_edges();
// Compose original-states with the any previously existing one.
if (auto old_orig_states =
old->get_named_prop<std::vector<unsigned>>("original-states"))
for (auto& s: *origin)
s = (*old_orig_states)[s];
// if we had some origin-classes, compose them, and output that
// instead of original-states.
if (auto old_orig_classes =
old->get_named_prop<std::vector<unsigned>>("original-classes"))
{
for (auto& s: *origin)
s = (*old_orig_classes)[s];
res->set_named_prop("original-classes", origin);
}
else
{
// Otherwise, define original-states, and compose it with any
// previously existing one.
if (auto old_orig_states =
old->get_named_prop<std::vector<unsigned>>("original-states"))
for (auto& s: *origin)
s = (*old_orig_states)[s];
res->set_named_prop("original-states", origin);
}
// If the automaton was marked as not complete or not universal,
// and we have ignored some unreachable state, then it is possible

5
spot/twaalgos/sbacc.hh
View file

@ -49,5 +49,10 @@ namespace spot
/// vectors will be composed, so the `original-states[s]` in the
/// output will contains the value of `original-states[y] if state s
/// was created from state y.
///
/// If the input has a property named "original-classes", then the
/// above "original-state" property is replaced by an
/// "original-classes" property such that
/// original-classes[s] is the class of the original state of s.
SPOT_API twa_graph_ptr sbacc(twa_graph_ptr aut);
}

1
tests/Makefile.am
View file

@ -397,6 +397,7 @@ TESTS_python = \
python/complement_semidet.py \
python/declenv.py \
python/decompose_scc.py \
python/det.py \
python/dualize.py \
python/ecfalse.py \
python/except.py \

35
tests/python/det.py Normal file
View file

@ -0,0 +1,35 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2021 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
a = spot.translate('FGa | FGb')
# The 8th argument requests the computation of original-classes.
d = spot.tgba_determinize(a, False, True, True, True,
None, -1, True)
cld = list(d.get_original_classes())
assert [0, 1, 2, 3, 3] == cld
e = spot.sbacc(d)
assert e.get_original_states() is None
cle = list(e.get_original_classes())
assert len(cle) == e.num_states()
assert set(cle) == set(cld)