From 46d8aaaae1faf73bb31b6ae446ebd4032f7e19e3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 10 Apr 2017 19:26:52 +0200 Subject: [PATCH] twa_graph: introduce copy_state_names_from() * spot/twa/twagraph.cc, spot/twa/twagraph.hh: Here. Also make sure "original-states" survives defrag_states(). * NEWS: Mention it. * tests/python/origstate.py: New file. * tests/Makefile.am: Add it. --- NEWS | 4 ++ spot/twa/twagraph.cc | 39 ++++++++++++++ spot/twa/twagraph.hh | 8 +++ tests/Makefile.am | 1 + tests/python/origstate.py | 108 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 160 insertions(+) create mode 100644 tests/python/origstate.py diff --git a/NEWS b/NEWS index a19d59952..b930bfbf9 100644 --- a/NEWS +++ b/NEWS @@ -62,6 +62,10 @@ New in spot 2.3.3.dev (not yet released) - The 'spot.gen' package exports the functions from libspotgen. See https://spot.lrde.epita.fr/ipynb/gen.html for examples. + - twa_graph::copy_state_names_from() can be used to copy the state + names from another automaton, honoring "original-states" if + present. + Bugs fixed: - the transformation to state-based acceptance (spot::sbacc()) was diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 1cc83e5c1..a3cde0f6e 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -542,6 +542,7 @@ namespace spot unsigned dst = newst[s]; if (dst == s || dst == -1U) continue; + assert(dst < s); (*names)[dst] = std::move((*names)[s]); } names->resize(used_states); @@ -558,6 +559,19 @@ 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); + } init_number_ = newst[init_number_]; g_.defrag_states(std::move(newst), used_states); } @@ -582,5 +596,30 @@ namespace spot } } + void twa_graph::copy_state_names_from(const const_twa_graph_ptr& other) + { + if (other == shared_from_this()) + return; + auto orig = get_named_prop>("original-states"); + if (orig && orig->size() != num_states()) + throw std::runtime_error("copy_state_names_from(): unexpected size " + "for original-states"); + + auto names = std::unique_ptr> + (new std::vector); + unsigned ns = num_states(); + unsigned ons = other->num_states(); + + for (unsigned s = 0; s < ns; ++s) + { + unsigned other_s = orig ? (*orig)[s] : s; + if (other_s >= ons) + throw std::runtime_error("copy_state_names_from(): state does not" + " exist in source automaton"); + names->emplace_back(other->format_state(other_s)); + } + + set_named_prop("state-names", names.release()); + } } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 1b3733d1e..7c30331ed 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -566,6 +566,14 @@ namespace spot /// automaton, those that are not actually used by its labels. void remove_unused_ap(); + /// \brief Define the state names of this automaton using + /// the names from \a other. + /// + /// If the "original-states" named property is set, it is used to + /// map the state numbers, otherwise an identity mapping is + /// assumed. + void copy_state_names_from(const const_twa_graph_ptr& other); + acc_cond::mark_t state_acc_sets(unsigned s) const { if (SPOT_UNLIKELY(!(bool)prop_state_acc())) diff --git a/tests/Makefile.am b/tests/Makefile.am index 16be77658..a60920109 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -346,6 +346,7 @@ TESTS_python = \ python/minato.py \ python/misc-ec.py \ python/optionmap.py \ + python/origstate.py \ python/otfcrash.py \ python/parsetgba.py \ python/prodexpt.py \ diff --git a/tests/python/origstate.py b/tests/python/origstate.py new file mode 100644 index 000000000..7c50c1d7e --- /dev/null +++ b/tests/python/origstate.py @@ -0,0 +1,108 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2015, 2017 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 +from sys import exit + +aut = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[0] 0 {0} +[!0] 0 +[1] 1 +State: 1 +[1] 1 {0} +--END-- +""") + +aut2 = spot.degeneralize(aut) +assert aut2.to_str() == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 {0} +[0] 0 +[!0] 1 +[1] 2 +State: 1 +[0] 0 +[!0] 1 +[1] 2 +State: 2 {0} +[1] 2 +--END--""" + +aut2.copy_state_names_from(aut) +assert aut2.to_str() == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 "0" {0} +[0] 0 +[!0] 1 +[1] 2 +State: 1 "0" +[0] 0 +[!0] 1 +[1] 2 +State: 2 "1" {0} +[1] 2 +--END--""" + +aut2.set_init_state(2) +aut2.purge_unreachable_states() +ref = """HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc colored +properties: deterministic +--BODY-- +State: 0 "1" {0} +[1] 0 +--END--""" +assert aut2.to_str() == ref +# This makes sure that the original-states vector has also been renamed. +aut2.copy_state_names_from(aut) +assert aut2.to_str() == ref + +aut2 = spot.degeneralize(aut) +aut2.release_named_properties() +try: + aut2.copy_state_names_from(aut) +except RuntimeError as e: + assert "state does not exist in source automaton" in str(e) +else: + exit(1)