From 77a17881a3222bd8604e5e33974a542351490638 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Sep 2024 17:10:27 +0200 Subject: [PATCH] defrag_states: allow a permutation of state numbers * spot/misc/permute.hh: New file. * spot/misc/Makefile.am: Add it. * spot/graph/graph.hh, spot/twa/twagraph.cc, spot/twaalgos/randomize.cc: Use the new permute_vector() function. * spot/twa/twagraph.hh: Update documentation. * NEWS: Update. --- NEWS | 3 ++ spot/graph/graph.hh | 31 ++++++--------- spot/misc/Makefile.am | 1 + spot/misc/permute.hh | 81 ++++++++++++++++++++++++++++++++++++++ spot/twa/twagraph.cc | 37 +++-------------- spot/twa/twagraph.hh | 3 +- spot/twaalgos/randomize.cc | 8 ++-- 7 files changed, 108 insertions(+), 56 deletions(-) create mode 100644 spot/misc/permute.hh diff --git a/NEWS b/NEWS index 5465c6b67..0da353568 100644 --- a/NEWS +++ b/NEWS @@ -93,6 +93,9 @@ New in spot 2.12.0.dev (not yet released) any word accepted by A from state x satisfies V[x]. Related to Issue #591. + - twa_graph::defrag_states(num) no longer require num[i]≤i; num + can now describe a permutation of the state numbers. + Bug fixes: - Generating random formulas without any unary opertor would very diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 04d0a8421..3b43f751b 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -20,6 +20,7 @@ #include #include +#include #include #include #include @@ -1446,8 +1447,7 @@ namespace spot /// dangling. /// /// \param newst A vector indicating how each state should be - /// renumbered. Use -1U to erase an unreachable state. All other - /// numbers are expected to satisfy newst[i] ≤ i for all i. + /// renumbered. Use -1U to erase an unreachable state. /// /// \param used_states the number of states used (after /// renumbering) @@ -1461,24 +1461,19 @@ namespace spot //std::cerr << "\nbefore defrag\n"; //dump_storage(std::cerr); - // Shift all states in states_, as indicated by newst. + // Permute all states in states_, as indicated by newst. + // This will put erased states after used_states. + permute_vector(states_, newst); unsigned send = states_.size(); - for (state s = 0; s < send; ++s) + for (state s = used_states; s < send; ++s) { - state dst = newst[s]; - if (dst == s) - continue; - if (dst == -1U) - { - // This is an erased state. Mark all its edges as - // dead (i.e., t.next_succ should point to t for each of - // them). - auto t = states_[s].succ; - while (t) - std::swap(t, edges_[t].next_succ); - continue; - } - states_[dst] = std::move(states_[s]); + // This is an erased state. Mark all its edges as + // dead (i.e., t.next_succ should point to t for each of + // them). + auto t = states_[s].succ; + while (t) + std::swap(t, edges_[t].next_succ); + continue; } states_.resize(used_states); diff --git a/spot/misc/Makefile.am b/spot/misc/Makefile.am index 747153500..085ac55a0 100644 --- a/spot/misc/Makefile.am +++ b/spot/misc/Makefile.am @@ -46,6 +46,7 @@ misc_HEADERS = \ memusage.hh \ mspool.hh \ optionmap.hh \ + permute.hh \ position.hh \ random.hh \ satsolver.hh \ diff --git a/spot/misc/permute.hh b/spot/misc/permute.hh new file mode 100644 index 000000000..1bcd39d86 --- /dev/null +++ b/spot/misc/permute.hh @@ -0,0 +1,81 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// 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 +#include + +namespace spot +{ + + // Reorder `data` according the permutation in `indices` by + // following the cycles in the permutation. Additionally, if an + // index is -1, the corresponding value is moved to the end of the + // data. + // + // After running this algorithm, data[i] should be moved to + // data[indices[i]] or to the end of the data if indices[i] == -1U. + // + // If indices.size() != data.size(), the minimum of both size is + // used, and indices are expected to stay in this range. + template + void permute_vector(std::vector& data, + const std::vector& indices) + { + unsigned n = std::min(data.size(), indices.size()); + if (n == 0) + return; + std::vector done(n, false); + unsigned end_of_data = n - 1; // index for the first -1 + for (unsigned i = 0; i < n; ++i) + { + if (done[i] || indices[i] == i) + continue; // already done or identity + unsigned next = indices[i]; + if (next == -1U) + { + next = end_of_data--; + if (next == i) + continue; + } + values tmp = std::move(data[i]); + while (next != i) + { + SPOT_ASSERT(next < n); + if (done[next]) + throw std::invalid_argument + ("permute_vector: invalid permutation"); + // this is a swap, but std::swap will not work + // when data[next] is a bool_reference. + values tmp2 = std::move(data[next]); + data[next] = std::move(tmp); + tmp = std::move(tmp2); + done[next] = true; + + next = indices[next]; + if (next == -1U) + next = end_of_data--; + } + data[i] = std::move(tmp); + done[i] = true; + } + } + +} diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 2ccc411a9..882714ab2 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1257,18 +1257,10 @@ namespace spot for (auto& e: edges()) fixup(e.dst); } - + // Update properties... if (auto* names = get_named_prop>("state-names")) { - unsigned size = names->size(); - for (unsigned s = 0; s < size; ++s) - { - unsigned dst = newst[s]; - if (dst == s || dst == -1U) - continue; - assert(dst < s); - (*names)[dst] = std::move((*names)[s]); - } + permute_vector(*names, newst); names->resize(used_states); } if (auto hs = get_named_prop> @@ -1325,15 +1317,7 @@ namespace spot "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]; - } + permute_vector(*os, newst); os->resize(used_states); } if (auto ss = get_named_prop>("simulated-states")) @@ -1349,19 +1333,10 @@ namespace spot // Reassign the state-players if (auto sp = get_named_prop>("state-player")) { - const auto ns = (unsigned) used_states; - const auto sps = (unsigned) sp->size(); - assert(ns <= sps); - assert(sps == newst.size()); - - for (unsigned i = 0; i < sps; ++i) - { - if (newst[i] == -1u) - continue; - (*sp)[newst[i]] = (*sp)[i]; - } - sp->resize(ns); + permute_vector(*sp, newst); + sp->resize(used_states); } + // Finally, update all states and edges. init_number_ = newst[init_number_]; g_.defrag_states(newst, used_states); } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 36fa31836..614aeb9d9 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -734,8 +734,7 @@ namespace spot /// /// \param newst A vector indicating how each state should be /// renumbered. Use -1U to mark an unreachable state for removal. - /// Ignoring the occurrences of -1U, the renumbering is expected - /// to satisfy newst[i] ≤ i for all i. If the automaton contains + /// Ignoring the occurrences of -1U. If the automaton contains /// universal branching, this vector is likely to be modified by /// this function, so do not reuse it afterwards. /// diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc index 19c32bea0..c7975a82a 100644 --- a/spot/twaalgos/randomize.cc +++ b/spot/twaalgos/randomize.cc @@ -20,6 +20,7 @@ #include #include #include +#include #include namespace spot @@ -47,11 +48,8 @@ namespace spot if (auto sn = aut->get_named_prop>("state-names")) { - unsigned sns = sn->size(); // Might be != n. - auto nn = new std::vector(n); - for (unsigned i = 0; i < sns && i < n; ++i) - (*nn)[nums[i]] = (*sn)[i]; - aut->set_named_prop("state-names", nn); + sn->resize(n); + permute_vector(*sn, nums); } if (auto hs = aut->get_named_prop> ("highlight-states"))