diff --git a/NEWS b/NEWS index 80c4a2ed1..d76130a12 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/doc/org/concepts.org b/doc/org/concepts.org index eb9fef471..a0cbf289a 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1138,6 +1138,7 @@ Here is a list of named properties currently used inside Spot: | ~highlight-edges~ | ~std::map~ | map of (edge number, color number) for highlighting the output | | ~highlight-states~ | ~std::map~ | map of (state number, color number) for highlighting the output | | ~incomplete-states~ | ~std::set~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) | +| ~original-classes~ | ~std::vector~ | class number associated to each state of a construction (used by some algorithms like =tgba_deternize()=) | | ~original-clauses~ | ~std::vector~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= | | ~original-states~ | ~std::vector~ | 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 | diff --git a/python/spot/impl.i b/python/spot/impl.i index 67d29ea09..cc0862ffe 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -983,6 +983,15 @@ static void* ptr_for_bdddict(PyObject* obj) >>("product-states"); } + std::vector* get_original_states() + { + return self->get_named_prop>("original-states"); + } + + std::vector* get_original_classes() + { + return self->get_named_prop>("original-classes"); + } twa* highlight_state(unsigned state, unsigned color) { diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index d3ba85fd6..d1fccadf4 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -303,6 +303,7 @@ namespace spot COPY_PROP(hlmap, "highlight-edges"); COPY_PROP(hlmap, "highlight-states"); COPY_PROP(std::set, "incomplete-states"); + COPY_PROP(std::vector, "original-classes"); COPY_PROP(std::vector, "original-clauses"); COPY_PROP(std::vector, "original-states"); COPY_PROP(spot::product_states, "product-states"); diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 1fbe76f77..62c0d10aa 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -908,32 +908,22 @@ namespace spot } std::swap(*hs, hs2); } - if (auto os = get_named_prop>("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>("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>(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>("simulated-states")) { for (auto& s : *ss) diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 3e361a813..82305f564 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -548,6 +548,35 @@ namespace spot return res; } + std::vector* + classify(const power_set& states, + const std::vector* original_class) + { + unsigned sz = states.size(); + auto classes = new std::vector(sz); + std::vector> state_sets(sz); + for (const auto& p: states) + { + // Get the set of original stats of this + std::set 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, 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& 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>("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>("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; } } diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index 61b69f6fb..b047e8234 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -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); } diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index e79cba774..5f93e0584 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -95,7 +95,6 @@ namespace spot std::vector> todo; auto* origin = new std::vector; 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>("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>("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>("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 diff --git a/spot/twaalgos/sbacc.hh b/spot/twaalgos/sbacc.hh index 11bc99e35..4d91ce75a 100644 --- a/spot/twaalgos/sbacc.hh +++ b/spot/twaalgos/sbacc.hh @@ -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); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 60858d9c3..accbad825 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/det.py b/tests/python/det.py new file mode 100644 index 000000000..03f07c096 --- /dev/null +++ b/tests/python/det.py @@ -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 . + +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)