From fb63dfc309683d1ac443158605e22c94a11775e6 Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber-Caissier Date: Tue, 29 Nov 2022 14:01:45 +0100 Subject: [PATCH] introduce partitioned_relabel_here Function taking an automaton and trying to relabel it by partitioning the old conditions and encode the different subsets of the partition with new variables * spot/priv/Makefile.am: Add * spot/priv/partitioned_relabel.hh , spot/priv/partitioned_relabel.cc: try_partition_me, computes the partition of a given vector of bdds * spot/twaalgos/relabel.hh , spot/twaalgos/relabel.cc: Here. Adapt also relabel() to cope with the different type of relabeling_maps * tests/python/_partitioned_relabel.ipynb , tests/python/except.py: Test and Usage * tests/Makefile.am: Add test --- spot/priv/Makefile.am | 2 + spot/priv/partitioned_relabel.cc | 147 +++ spot/priv/partitioned_relabel.hh | 81 ++ spot/twaalgos/relabel.cc | 461 ++++++++- spot/twaalgos/relabel.hh | 33 + tests/Makefile.am | 1 + tests/python/_partitioned_relabel.ipynb | 1224 +++++++++++++++++++++++ tests/python/except.py | 15 + 8 files changed, 1920 insertions(+), 44 deletions(-) create mode 100644 spot/priv/partitioned_relabel.cc create mode 100644 spot/priv/partitioned_relabel.hh create mode 100644 tests/python/_partitioned_relabel.ipynb diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am index d4e9cc77c..317292bd3 100644 --- a/spot/priv/Makefile.am +++ b/spot/priv/Makefile.am @@ -29,6 +29,8 @@ libpriv_la_SOURCES = \ bddalloc.hh \ freelist.cc \ freelist.hh \ + partitioned_relabel.cc \ + partitioned_relabel.hh \ robin_hood.hh \ satcommon.hh\ satcommon.cc\ diff --git a/spot/priv/partitioned_relabel.cc b/spot/priv/partitioned_relabel.cc new file mode 100644 index 000000000..f28ea5554 --- /dev/null +++ b/spot/priv/partitioned_relabel.cc @@ -0,0 +1,147 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2022 Laboratoire de Recherche +// de l'Epita (LRE). +// +// 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 . + +#include "config.h" + +#include + + +relabeling_map +bdd_partition::to_relabeling_map(twa_graph& for_me) const +{ + relabeling_map res; + // Change to unordered_map? + bdd_dict_ptr bdddict = for_me.get_dict(); + + bool use_inner = ig->state_storage(0).new_label != bddfalse; + std::vector doskip + = use_inner ? std::vector(ig->num_states(), false) + : std::vector(); + + auto bdd2form = [&bdddict](const bdd& cond) + { + return bdd_to_formula(cond, bdddict); + }; + + for (const auto& [old_letter, s] : treated) + { + formula new_letter_form = bdd2form(ig->state_storage(s).new_label); + assert(res.count(new_letter_form) == 0); + if (use_inner) + doskip[s] = true; + res[new_letter_form] = bdd2form(old_letter); + } + + if (use_inner) + { + // This implies that the split option was false, + // so we can store further info + auto& all_cond = *all_cond_ptr; + const unsigned Norig = all_cond.size(); + + for (unsigned i = 0; i < Norig; ++i) + { + // Internal node -> new ? + if (doskip[i]) + continue; + // Leave node -> already exists + if (ig->state_storage(i).succ == 0) + continue; + doskip[i] = true; + formula new_letter_form + = bdd2form(ig->state_storage(i).new_label); +#ifdef NDEBUG + res[new_letter_form] = bdd2form(all_cond[i]); +#else + // Check if they are the same + formula old_form = bdd2form(all_cond[i]); + if (res.count(new_letter_form) == 0) + res[new_letter_form] = old_form; + else + assert(res[new_letter_form] == old_form); +#endif + } + } + return res; +} + +/// \brief Tries to partition the given condition vector \a all_cond +/// abandons at \a max_letter. +/// \return The corresponding bdd_partition +/// \note A pointer to all_cond is captured internally, it needs +/// to outlive the returned bdd_partition +bdd_partition +try_partition_me(const std::vector& all_cond, unsigned max_letter) +{ + // We create vector that will be succesively filled. + // Each entry corresponds to a "letter", of the partition + const size_t Norig = all_cond.size(); + + bdd_partition result(all_cond); + + auto& treated = result.treated; + auto& ig = *result.ig; + + for (unsigned io = 0; io < Norig; ++io) + { + bdd cond = all_cond[io]; + const auto Nt = treated.size(); + for (size_t in = 0; in < Nt; ++in) + { + if (cond == bddfalse) + break; + if (treated[in].first == cond) + { + // Found this very condition -> make transition + ig.new_edge(io, treated[in].second); + cond = bddfalse; + break; + } + if (bdd_have_common_assignment(treated[in].first, cond)) + { + bdd inter = treated[in].first & cond; + // Create two new states + unsigned ssplit = ig.new_states(2); + // ssplit becomes the state without the intersection + // ssplit + 1 becomes the intersection + // Both of them are implied by the original node, + // Only inter is implied by the current letter + ig.new_edge(treated[in].second, ssplit); + ig.new_edge(treated[in].second, ssplit+1); + ig.new_edge(io, ssplit+1); + treated.emplace_back(inter, ssplit+1); + // Update + cond -= inter; + treated[in].first -= inter; + treated[in].second = ssplit; + if (treated.size() > max_letter) + return bdd_partition{}; + } + } + if (cond != bddfalse) + { + unsigned sc = ig.new_state(); + treated.emplace_back(cond, sc); + ig.new_edge(io, sc); + } + } + + result.relabel_succ = true; + return result; +} \ No newline at end of file diff --git a/spot/priv/partitioned_relabel.hh b/spot/priv/partitioned_relabel.hh new file mode 100644 index 000000000..cd19ffaea --- /dev/null +++ b/spot/priv/partitioned_relabel.hh @@ -0,0 +1,81 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2022 Laboratoire de Recherche +// de l'Epita (LRE). +// +// 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 +#include +#include +#include +#include + + +using namespace spot; + +struct bdd_partition +{ + struct S + { + bdd new_label = bddfalse; + }; + struct T + { + }; + using implication_graph = digraph; + + // A pointer to the conditions to be partitioned + const std::vector* all_cond_ptr; + // Graph with the invariant that + // children imply parents + // Leaves from the partition + // original conditions are "root" nodes + std::unique_ptr ig; + // todo: technically there are at most two successors, so a graph + // is "too" generic + // All conditions currently part of the partition + // unsigned corresponds to the associated node + std::vector> treated; + std::vector new_aps; + bool relabel_succ = false; + + bdd_partition() = default; + bdd_partition(const std::vector& all_cond) + : all_cond_ptr(&all_cond) + , ig{std::make_unique(2*all_cond.size(), + 2*all_cond.size())} + { + // Create the roots of all old conditions + // Each condition is associated to the state with + // the same index + const unsigned Norig = all_cond.size(); + ig->new_states(Norig); + } + + // Facilitate conversion + // This can only be called when letters have already + // been computed + relabeling_map + to_relabeling_map(twa_graph& for_me) const; +}; // bdd_partition + + +bdd_partition +try_partition_me(const std::vector& all_cond, unsigned max_letter); \ No newline at end of file diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index ac1556aec..ba5e4ed14 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -20,60 +20,275 @@ #include "config.h" #include #include +#include + +#include + +#include +#include +#include + namespace spot { - void - relabel_here(twa_graph_ptr& aut, relabeling_map* relmap) + namespace { - std::unique_ptr pairs(bdd_newpair()); - auto d = aut->get_dict(); - std::vector vars; - std::set newvars; - vars.reserve(relmap->size()); - bool bool_subst = false; - auto aplist = aut->ap(); - for (auto& p: *relmap) - { - if (!p.first.is(op::ap)) - throw std::runtime_error - ("relabel_here: old labels should be atomic propositions"); - if (!p.second.is_boolean()) - throw std::runtime_error - ("relabel_here: new labels should be Boolean formulas"); + void + comp_new_letters(bdd_partition& part, + twa_graph& aut, + const std::string& var_prefix, + bool split) + { + auto& ig = *part.ig; + const auto& treated = part.treated; + auto& new_aps = part.new_aps; + // Get the new variables and their negations + const unsigned Nnl = treated.size(); + const unsigned Nnv = std::ceil(std::log2(Nnl)); + std::vector> Nv_vec(Nnv); - // Don't attempt to rename APs that are not used. - if (std::find(aplist.begin(), aplist.end(), p.first) == aplist.end()) - continue; + new_aps.reserve(Nnv); + for (unsigned i = 0; i < Nnv; ++i) + { + // todo check if it does not exist / use anonymous? + new_aps.push_back(formula::ap(var_prefix+std::to_string(i))); + int v = aut.register_ap(new_aps.back()); + Nv_vec[i] = {bdd_nithvar(v), bdd_ithvar(v)}; + } - int oldv = aut->register_ap(p.first); - vars.emplace_back(oldv); - if (p.second.is(op::ap)) - { - int newv = aut->register_ap(p.second); - newvars.insert(newv); - bdd_setpair(pairs.get(), oldv, newv); - } - else - { - p.second.traverse([&](const formula& f) - { - if (f.is(op::ap)) - newvars.insert(aut->register_ap(f)); - return false; - }); - bdd newb = formula_to_bdd(p.second, d, aut); - bdd_setbddpair(pairs.get(), oldv, newb); - bool_subst = true; - } + auto leaveidx2label = [&](unsigned idx) + { + unsigned c = 0; + unsigned rem = idx; + bdd thisbdd = bddtrue; + while (rem) + { + thisbdd &= Nv_vec[c][rem & 1]; + ++c; + rem >>= 1; + } + for (; c < Nnv; ++c) + thisbdd &= Nv_vec[c][0]; + return thisbdd; + }; + + // Compute only labels of leaves + for (unsigned idx = 0; idx < Nnl; ++idx) + ig.state_storage(treated[idx].second).new_label = leaveidx2label(idx); + + // We will label the implication graph with the new letters + auto relabel_impl = [&](unsigned s, auto&& relabel_impl_rec) + { + auto& ss = ig.state_storage(s); + if (ss.new_label != bddfalse) + return ss.new_label; + else + { + assert((ss.succ != 0) && "Should not be a leave"); + bdd thisbdd = bddfalse; + for (const auto& e : ig.out(s)) + thisbdd |= relabel_impl_rec(e.dst, relabel_impl_rec); + ss.new_label = thisbdd; + return thisbdd; + } + }; + + if (!split) + { + // For split only leaves is ok, + // disjunction is done via transitions + // This will compute the new_label for all states in the ig + const unsigned Norig = part.all_cond_ptr->size(); + for (unsigned i = 0; i < Norig; ++i) + relabel_impl(i, relabel_impl); + } + } // comp_new_letters + + // Recursive traversal of implication graph + void replace_label_(unsigned si, + unsigned esrc, unsigned edst, + bdd& econd, + const bdd_partition::implication_graph& ig, + twa_graph& aut) + { + auto& sstore = ig.state_storage(si); + if (sstore.succ == 0) + { + if (econd == bddfalse) + econd = sstore.new_label; + else + aut.new_edge(esrc, edst, sstore.new_label); + } + else + { + for (const auto& e_ig : ig.out(si)) + replace_label_(e_ig.dst, esrc, edst, econd, ig, aut); + } + } + + relabeling_map + partitioned_relabel_here_(twa_graph& aut, bool split, + unsigned max_letter, + unsigned max_letter_mult, + const bdd& concerned_ap, + bool treat_all, + const std::string& var_prefix) + { + auto abandon = []() + { + return relabeling_map{}; + }; + + + // When split we need to distiguish effectively new and old edges + if (split) + { + aut.get_graph().remove_dead_edges_(); + aut.get_graph().sort_edges_(); + aut.get_graph().chain_edges_(); + } + + // Get all conditions present in the automaton + std::vector all_cond; + bdd ignoredcon = bddtrue; + std::unordered_map all_cond_id2idx; + + all_cond.reserve(0.1*aut.num_edges()); + all_cond_id2idx.reserve(0.1*aut.num_edges()); + + // Map for all supports + // and whether or not they are to be relabeled + std::unordered_map, bdd_hash> all_supports; + + for (const auto& e : aut.edges()) + { + auto it = all_supports.find(e.cond); + if (it != all_supports.end()) + continue; // Already treated + bdd se = bddtrue; + bool is_concerned = true; + if (!treat_all) + { + se = bdd_support(e.cond); + is_concerned = bdd_implies(concerned_ap, se); + } + + all_supports.emplace(e.cond, + std::make_pair(is_concerned, se)); + + if (!is_concerned) + { + assert(bdd_existcomp(se, concerned_ap) == bddtrue + && "APs are not partitioned"); + continue; + } + + auto [_, ins] = + all_cond_id2idx.try_emplace(e.cond.id(), all_cond.size()); + if (ins) + { + all_cond.push_back(e.cond); + if (all_cond.size() > max_letter) + return abandon(); + } + } + + unsigned stop = max_letter; + if (max_letter_mult != -1u) + { + // Make sure it does not overflow + if (max_letter_mult <= (-1u / ((unsigned) all_cond.size()))) + stop = std::min(stop, + (unsigned) (max_letter_mult*all_cond.size())); + } + + auto this_partition = try_partition_me(all_cond, stop); + + if (!this_partition.relabel_succ) + return abandon(); + + comp_new_letters(this_partition, aut, var_prefix, split); + + // An original condition is represented by all leaves that imply it + auto& ig = *this_partition.ig; + const unsigned Ns = aut.num_states(); + const unsigned Nt = aut.num_edges(); + for (unsigned s = 0; s < Ns; ++s) + { + for (auto& e : aut.out(s)) + { + if (aut.edge_number(e) > Nt) + continue; + if (!all_supports.at(e.cond).first) + continue; // Edge not concerned + unsigned idx = all_cond_id2idx[e.cond.id()]; + + if (split) + { + // initial call + // We can not hold a ref to the edge + // as the edgevector might get reallocated + bdd econd = bddfalse; + unsigned eidx = aut.edge_number(e); + replace_label_(idx, e.src, e.dst, + econd, ig, aut); + aut.edge_storage(eidx).cond = econd; + } + else + e.cond = ig.state_storage(idx).new_label; + } // for edge + } // for state + return this_partition.to_relabeling_map(aut); + } + + void + relabel_here_ap_(twa_graph_ptr& aut_ptr, relabeling_map relmap) + { + assert(aut_ptr); + twa_graph& aut = *aut_ptr; + + std::unique_ptr pairs(bdd_newpair()); + auto d = aut.get_dict(); + std::vector vars; + std::set newvars; + vars.reserve(relmap.size()); + bool bool_subst = false; + auto aplist = aut.ap(); + + for (auto& p: relmap) + { + // Don't attempt to rename APs that are not used. + if (std::find(aplist.begin(), aplist.end(), p.first) == aplist.end()) + continue; + + int oldv = aut.register_ap(p.first); + vars.emplace_back(oldv); + if (p.second.is(op::ap)) + { + int newv = aut.register_ap(p.second); + newvars.insert(newv); + bdd_setpair(pairs.get(), oldv, newv); + } + else + { + p.second.traverse([&](const formula& f) + { + if (f.is(op::ap)) + newvars.insert(aut.register_ap(f)); + return false; + }); + bdd newb = formula_to_bdd(p.second, d, aut_ptr); + bdd_setbddpair(pairs.get(), oldv, newb); + bool_subst = true; + } } bool need_cleanup = false; typedef bdd (*op_t)(const bdd&, bddPair*); op_t op = bool_subst ? static_cast(bdd_veccompose) : static_cast(bdd_replace); - for (auto& t: aut->edges()) + for (auto& t: aut.edges()) { bdd c = (*op)(t.cond, pairs.get()); t.cond = c; @@ -86,14 +301,172 @@ namespace spot // p0) for (auto v: vars) if (newvars.find(v) == newvars.end()) - aut->unregister_ap(v); + aut.unregister_ap(v); // If some of the edges were relabeled false, we need to clean the // automaton. if (need_cleanup) { - aut->merge_edges(); // remove any edge labeled by 0 - aut->purge_dead_states(); // remove useless states + aut.merge_edges(); // remove any edge labeled by 0 + aut.purge_dead_states(); // remove useless states } + } + + void + relabel_here_gen_(twa_graph_ptr& aut_ptr, relabeling_map relmap) + { + assert(aut_ptr); + twa_graph& aut = *aut_ptr; + + auto form2bdd = [this_dict = aut.get_dict()](const formula& f) + { + return formula_to_bdd(f, this_dict, this_dict); + }; + + auto bdd2form = [bdddict = aut.get_dict()](const bdd& cond) + { + return bdd_to_formula(cond, bdddict); + }; + + + // translate formula -> bdd + std::unordered_map base_letters; + base_letters.reserve(relmap.size()); + + std::unordered_map comp_letters; + std::unordered_set ignored_letters; + + // Necessary to detect unused + bdd new_var_supp = bddtrue; + auto translate = [&](bdd& cond) + { + // Check if known + for (const auto& map : {base_letters, comp_letters}) + { + auto it = map.find(cond); + if (it != map.end()) + { + cond = it->second; + return; + } + } + + // Check if known to be ignored + if (auto it = ignored_letters.find(cond); + it != ignored_letters.end()) + return; + + // Check if ignored + bdd cond_supp = bdd_support(cond); + if (!bdd_implies(new_var_supp, cond_supp)) + { + ignored_letters.insert(cond); + assert(bdd_existcomp(cond_supp, new_var_supp) == bddtrue + && "APs are not partitioned"); + return; + } + + // Compute + // compose the given cond from a disjunction of base_letters + bdd old_cond = bddfalse; + for (const auto& [k, v] : base_letters) + { + if (bdd_implies(k, cond)) + old_cond |= v; + } + comp_letters[cond] = old_cond; + cond = old_cond; + return; + }; + + for (const auto& [new_f, old_f] : relmap) + { + bdd new_cond = form2bdd(new_f); + new_var_supp &= bdd_support(new_cond); + base_letters[new_cond] = form2bdd(old_f); + } + + + // Save the composed letters? With a special seperator like T/F? + // Is swapping between formula <-> bdd expensive + for (auto& e : aut.edges()) + translate(e.cond); + + // Remove the new auxilliary variables from the aut + bdd c_supp = new_var_supp; + while (c_supp != bddtrue) + { + aut.unregister_ap(bdd_var(c_supp)); + c_supp = bdd_high(c_supp); + } + + return; + } + + } // Namespace + + void + relabel_here(twa_graph_ptr& aut, relabeling_map* relmap) + { + if (!relmap || relmap->empty()) + return; + + // There are two different types of relabeling maps: + // 1) The "traditional": + // New atomic propositions (keys) correspond to general formulas over + // the original propositions (values) + // 2) The one resulting from partitioned_relabel_here + // Here general (boolean) formulas over new propositions (keys) + // are associated to general formulas over + // the original propositions (values) + + if (!std::all_of(relmap->begin(), relmap->end(), + [](const auto& it){return it.first.is_boolean() + && it.second.is_boolean(); })) + throw std::runtime_error + ("relabel_here: old labels and new labels " + "should be Boolean formulas"); + + bool only_ap = std::all_of(relmap->cbegin(), relmap->cend(), + [](const auto& p) + { + return p.first.is(op::ap); + }); + + if (only_ap) + relabel_here_ap_(aut, *relmap); + else + relabel_here_gen_(aut, *relmap); + } + + relabeling_map + partitioned_relabel_here(twa_graph_ptr& aut, + bool split, + unsigned max_letter, + unsigned max_letter_mult, + const bdd& concerned_ap, + std::string var_prefix) + { + if (!aut) + throw std::runtime_error("aut is null!"); + + if (std::find_if(aut->ap().cbegin(), aut->ap().cend(), + [var_prefix](const auto& ap) + { + return ap.ap_name().find(var_prefix) == 0; + }) != aut->ap().cend()) + throw std::runtime_error("partitioned_relabel_here(): " + "The given prefix for new variables may not appear as " + "a prefix of existing variables."); + + // If concerned_ap == bddtrue -> all aps are concerned + bool treat_all = concerned_ap == bddtrue; + bdd concerned_ap_ + = treat_all ? aut->ap_vars() : concerned_ap; + return partitioned_relabel_here_(*aut, split, + max_letter, max_letter_mult, + concerned_ap_, + treat_all, + var_prefix); } } diff --git a/spot/twaalgos/relabel.hh b/spot/twaalgos/relabel.hh index e10fe8903..34f7a0a41 100644 --- a/spot/twaalgos/relabel.hh +++ b/spot/twaalgos/relabel.hh @@ -21,6 +21,10 @@ #include #include +#include + +#include +#include namespace spot { @@ -33,4 +37,33 @@ namespace spot /// or relabel_bse(). SPOT_API void relabel_here(twa_graph_ptr& aut, relabeling_map* relmap); + + + /// \brief Replace conditions in \a aut with non-overlapping conditions + /// over fresh variables. + /// + /// Partitions the conditions in the automaton, then (binary) encodes + /// them using fresh propositions. + /// This can lead to an exponential explosion in the number of + /// conditions. The operations is aborted if either + /// the number of new letters (subsets of the partition) exceeds + /// \a max_letter OR \a max_letter_mult times the number of conditions + /// in the original automaton. + /// The argument \a concerned_ap can be used to filter out transitions. + /// If given, only the transitions whose support intersects the + /// concerned_ap (or whose condition is T) are taken into account. + /// The fresh aps will be enumerated and prefixed by \a var_prefix. + /// These variables need to be fresh, i.e. may not exist yet (not checked) + /// + /// \note If concerned_ap is given, then there may not be an edge + /// whose condition uses ap inside AND outside of concerned_ap. + /// Mostly used in a game setting to distinguish between + /// env and player transitions. + SPOT_API relabeling_map + partitioned_relabel_here(twa_graph_ptr& aut, bool split = false, + unsigned max_letter = -1u, + unsigned max_letter_mult = -1u, + const bdd& concerned_ap = bddtrue, + std::string var_prefix = "__nv"); + } diff --git a/tests/Makefile.am b/tests/Makefile.am index 4c2fe830c..0810df809 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -436,6 +436,7 @@ TESTS_python = \ python/origstate.py \ python/otfcrash.py \ python/parsetgba.py \ + python/_partitioned_relabel.ipynb \ python/parity.py \ python/pdegen.py \ python/prodexpt.py \ diff --git a/tests/python/_partitioned_relabel.ipynb b/tests/python/_partitioned_relabel.ipynb new file mode 100644 index 000000000..a9c1c7af7 --- /dev/null +++ b/tests/python/_partitioned_relabel.ipynb @@ -0,0 +1,1224 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "id": "4d896402", + "metadata": {}, + "outputs": [], + "source": [ + "import spot, buddy" + ] + }, + { + "cell_type": "markdown", + "id": "94e87f9c", + "metadata": {}, + "source": [ + "# Partitioned relabeling\n", + "\n", + "Partitioned relabeling will:\n", + "First compute a partition over all conditions appearing in the automaton.\n", + "That is, the set of new conditions is such that (1) they do not overlap (2) all valuations that verify some condition in the original automaton also verify (exactly one) of the new conditions.\n", + "These new conditions can be thought of as letters in a \"classical\" sense.\n", + "Then we create new aps and encode the \"number\" of these letters using the fresh aps, resulting in new letters which are a single valuation over the fresh aps.\n", + "\n", + "This can be helpful if there are many aps, but few different conditions over them\n", + "\n", + "The algorithm comes in two flavours:\n", + "\n", + "We maintain the original number of edges. Therefore the new label correspond to a disjunction over new letters (split=False).\n", + "We split each edge into its letters, creating more edges (split=True)." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "62123fa9", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b0311a80> >" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "#Relabeling a graph\n", + "aut = spot.make_twa_graph()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "na = buddy.bdd_nithvar(aut.register_ap(\"a\"))\n", + "b0 = buddy.bdd_ithvar(aut.register_ap(\"b0\"))\n", + "nb0 = buddy.bdd_nithvar(aut.register_ap(\"b0\"))\n", + "b1 = buddy.bdd_ithvar(aut.register_ap(\"b1\"))\n", + "nb1 = buddy.bdd_nithvar(aut.register_ap(\"b1\"))\n", + "b2 = buddy.bdd_ithvar(aut.register_ap(\"b2\"))\n", + "nb2 = buddy.bdd_nithvar(aut.register_ap(\"b2\"))\n", + "\n", + "aut.new_edge(0,1,buddy.bddtrue)\n", + "aut.new_edge(0,2,a)\n", + "aut.new_edge(0,3,a&b0&b1&b2)\n", + "aut.new_edge(0,4,a&nb0&nb1&nb2)\n", + "\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "d4c8e977", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "6\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "__nv0 | __nv1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "__nv0 & __nv1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b0311a80> >" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "relabel_dict = spot.partitioned_relabel_here(aut)\n", + "\n", + "print(relabel_dict.size())\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "6f90a095", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b0311a80> >" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Undo the relabeling\n", + "spot.relabel_here(aut, relabel_dict)\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "513067ab", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c0d50> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "States: 5\n", + "Start: 0\n", + "AP: 6 \"a\" \"b0\" \"b1\" \"b2\" \"__nv0\" \"__nv1\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc\n", + "--BODY--\n", + "State: 0\n", + "[!4&!5] 1\n", + "[4&!5] 2\n", + "[!4&5] 3\n", + "[4&5] 4\n", + "[4&!5] 1\n", + "[4&5] 1\n", + "[!4&5] 1\n", + "[4&5] 2\n", + "[!4&5] 2\n", + "State: 1\n", + "State: 2\n", + "State: 3\n", + "State: 4\n", + "--END--\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!__nv0 & !__nv1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "__nv0 & !__nv1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "__nv0 & !__nv1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "__nv0 & __nv1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c0d50> >" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Relabeling the same graph using the split option\n", + "aut = spot.make_twa_graph()\n", + "aut.new_states(5)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "na = buddy.bdd_nithvar(aut.register_ap(\"a\"))\n", + "b0 = buddy.bdd_ithvar(aut.register_ap(\"b0\"))\n", + "nb0 = buddy.bdd_nithvar(aut.register_ap(\"b0\"))\n", + "b1 = buddy.bdd_ithvar(aut.register_ap(\"b1\"))\n", + "nb1 = buddy.bdd_nithvar(aut.register_ap(\"b1\"))\n", + "b2 = buddy.bdd_ithvar(aut.register_ap(\"b2\"))\n", + "nb2 = buddy.bdd_nithvar(aut.register_ap(\"b2\"))\n", + "\n", + "aut.new_edge(0,1,buddy.bddtrue)\n", + "aut.new_edge(0,2,a)\n", + "aut.new_edge(0,3,a&b0&b1&b2)\n", + "aut.new_edge(0,4,a&nb0&nb1&nb2)\n", + "\n", + "display(aut)\n", + "xx = spot.partitioned_relabel_here(aut, True)\n", + "print(aut.to_str(\"hoa\"))\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "50c6a08b", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(a & !b0 & b2) | (a & b0 & !b2) | (a & !b1 & b2) | (a & b1 & !b2)\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(a & !b0 & b2) | (a & b0 & !b2) | (a & !b1 & b2) | (a & b1 & !b2)\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b0 & b1 & b2\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b0 & !b1 & !b2\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c0d50> >" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Undo the relabeling -> disjoint conditions over the original ap\n", + "spot.relabel_here(aut, relabel_dict)\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "d2efd313", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c90f0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "States: 6\n", + "Start: 0\n", + "AP: 5 \"a\" \"__nv0\" \"__nv1\" \"b\" \"c\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc\n", + "--BODY--\n", + "State: 0\n", + "[!1 | !2] 1\n", + "[!1&2 | 1&!2] 2\n", + "[!1&2] 3\n", + "[1&!2] 4\n", + "[4] 5\n", + "State: 1\n", + "State: 2\n", + "State: 3\n", + "State: 4\n", + "State: 5\n", + "--END--\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!__nv0 | !__nv1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(__nv0 & !__nv1) | (!__nv0 & __nv1)\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!__nv0 & __nv1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "__nv0 & !__nv1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c90f0> >" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Working only on a subset of the aps\n", + "# Note that True is always relabeled\n", + "\n", + "aut = spot.make_twa_graph()\n", + "aut.new_states(6)\n", + "\n", + "a = buddy.bdd_ithvar(aut.register_ap(\"a\"))\n", + "na = buddy.bdd_nithvar(aut.register_ap(\"a\"))\n", + "b = buddy.bdd_ithvar(aut.register_ap(\"b\"))\n", + "nb = buddy.bdd_nithvar(aut.register_ap(\"b\"))\n", + "c = buddy.bdd_ithvar(aut.register_ap(\"c\"))\n", + "nc = buddy.bdd_nithvar(aut.register_ap(\"c\"))\n", + "\n", + "aut.new_edge(0,1,buddy.bddtrue)\n", + "aut.new_edge(0,2,a)\n", + "aut.new_edge(0,3,a&b)\n", + "aut.new_edge(0,4,a&nb)\n", + "aut.new_edge(0,5,c)\n", + "\n", + "display(aut)\n", + "\n", + "concerned_aps = a & b # concerned aps are given as a conjunction of positive aps\n", + "# As partitioning can be exponentially costly,\n", + "# one can limit the number of new letters generated before abadoning\n", + "# This can be done either as a hard limit and/or as the number of current condition\n", + "# times a factor\n", + "relabel_dict = spot.partitioned_relabel_here(aut, False, 1000, 1000, concerned_aps)\n", + "print(aut.to_str(\"hoa\"))\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "1fbc8813", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "States: 6\n", + "Start: 0\n", + "AP: 3 \"a\" \"b\" \"c\"\n", + "acc-name: all\n", + "Acceptance: 0 t\n", + "properties: trans-labels explicit-labels state-acc\n", + "--BODY--\n", + "State: 0\n", + "[t] 1\n", + "[0] 2\n", + "[0&1] 3\n", + "[0&!1] 4\n", + "[2] 5\n", + "State: 1\n", + "State: 2\n", + "State: 3\n", + "State: 4\n", + "State: 5\n", + "--END--\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f65b02c90f0> >" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "#undo partial relabeling\n", + "spot.relabel_here(aut, relabel_dict)\n", + "print(aut.to_str(\"hoa\"))\n", + "aut" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.8.10" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/tests/python/except.py b/tests/python/except.py index 34aa61ad2..e531882dd 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -359,3 +359,18 @@ except RuntimeError as e: tc.assertIn(filename, str(e)) else: report_missing_exception() + + +# Relabeling must use new variables +aut = spot.make_twa_graph() +aut.new_states(2) +ap = buddy.bdd_ithvar(aut.register_ap("__nv0")) +aut.new_edge(0,1,ap) + +try: + spot.partitioned_relabel_here(aut) +except RuntimeError as e: + tc.assertIn("The given prefix for new variables", + str(e)) +else: + report_missing_exception() \ No newline at end of file