diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc index d1ffbbecd..09a1a2eb0 100644 --- a/spot/twaalgos/split.cc +++ b/spot/twaalgos/split.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement +// de l'Epita. IMDEA Software Institute. // // This file is part of Spot, a model checking library. // @@ -25,9 +25,200 @@ #include #include +#include + +namespace std +{ + template<> + struct hash<::bdd> + { + size_t operator()(::bdd const& instance) const noexcept + { + return ::spot::bdd_hash{}(instance); + } + }; + + template<> + struct hash> + { + size_t operator()(pair const& x) const noexcept + { + size_t first_hash = std::hash()(x.first); + size_t second_hash = std::hash()(x.second); + size_t sum = second_hash + + 0x9e3779b9 + + (first_hash << 6) + + (first_hash >> 2); + return first_hash ^ sum; + } + }; +} namespace spot { + // We attempt to add a potentially new set of symbols defined as "value" to + // our current set of edge partitions, "current_set". We also specify a set + // of valid symbols considered + static void add_to_lower_bound_set_helper( + std::unordered_set& current_set, + bdd valid_symbol_set, + bdd value) + { + // This function's correctness is defined by the invariant, that we never + // add a bdd to our current set unless the bdd is disjoint from every other + // element in the current_set. In other words, we will only reach the final + // set.insert(value), if we can iterate over the whole of current_set + // without finding some set intersections + if (value == bddfalse) // Don't add empty sets, as they subsume everything + { + return; + } + for (auto sym : current_set) + { + // If a sym is a subset of value, recursively add the set of symbols + // defined in value, but not in sym. This ensures the two elements + // are disjoint. + if (bdd_implies(sym, value)) + { + add_to_lower_bound_set_helper( + current_set, valid_symbol_set, (value - sym) & valid_symbol_set); + return; + } + // If a sym is a subset of the value we're trying to add, then we + // remove the symbol and add the two symbols created by partitioning + // the sym with value. + else if (bdd_implies(value, sym)) + { + current_set.erase(sym); + add_to_lower_bound_set_helper(current_set, + valid_symbol_set, + sym & value); + add_to_lower_bound_set_helper(current_set, + valid_symbol_set, + sym - value); + return; + } + } + // This line is only reachable if value is not a subset and doesn't + // subsume any element currently in our set + current_set.insert(value); + } + + static std::array create_possible_intersections( + bdd valid_symbol_set, + std::pair const& first, + std::pair const& second) + { + auto intermediate = second.first & valid_symbol_set; + auto intermediate2 = second.second & valid_symbol_set; + return { + first.first & intermediate, + first.second & intermediate, + first.first & intermediate2, + first.second & intermediate2, + }; + } + + using bdd_set = std::unordered_set; + using bdd_pair_set = std::unordered_set>; + + // Transforms each element of the basis into a complement pair, + // with a valid symbol set specified + static bdd_pair_set create_complement_pairs(std::vector const& basis, + bdd valid_symbol_set) + { + bdd_pair_set intersections; + for (auto& sym : basis) + { + auto intersection = sym & valid_symbol_set; + if (intersection != bddfalse) + { + auto negation = valid_symbol_set - intersection; + intersections.insert(std::make_pair(intersection, negation)); + } + } + return intersections; + } + + template + void iterate_possible_intersections(bdd_pair_set const& complement_pairs, + bdd valid_symbol_set, + Callable callable) + { + for (auto it = complement_pairs.begin(); it != complement_pairs.end(); ++it) + { + for (auto it2 = std::next(it); it2 != complement_pairs.end(); ++it2) + { + auto intersections = create_possible_intersections( + valid_symbol_set, *it, *it2); + for (auto& intersection : intersections) + { + callable(intersection); + } + } + } + } + + // Compute the lower set bound of a set. A valid symbol set is also + // provided to make sure that no symbol exists in the output if it is + // not also included in the valid symbol set + static bdd_set lower_set_bound(std::vector const& basis, + bdd valid_symbol_set) + { + auto complement_pairs = create_complement_pairs(basis, valid_symbol_set); + if (complement_pairs.size() == 1) + { + bdd_set lower_bound; + auto& pair = *complement_pairs.begin(); + if (pair.first != bddfalse + && bdd_implies(pair.first, valid_symbol_set)) + { + lower_bound.insert(pair.first); + } + if (pair.second != bddfalse + && bdd_implies(pair.second, valid_symbol_set)) + { + lower_bound.insert(pair.second); + } + return lower_bound; + } + else + { + bdd_set lower_bound; + iterate_possible_intersections(complement_pairs, valid_symbol_set, + [&](auto intersection) + { + add_to_lower_bound_set_helper(lower_bound, + valid_symbol_set, + intersection); + }); + + return lower_bound; + } + } + + // Partitions a symbol based on a list of other bdds called the basis. + // The resulting partition will have the property that for any paritioned + // element and any element element in the basis, the partitioned element will + // either by completely contained by that element of the basis, or completely + // disjoint. + static bdd_set generate_contained_or_disjoint_symbols(bdd sym, + std::vector const& basis) + { + auto lower_bound = lower_set_bound(basis, sym); + // If the sym was disjoint from everything in the basis, we'll be left with + // an empty lower_bound. To fix this, we will simply return a singleton, + // with sym as the only element. Notice, this singleton will satisfy the + // requirements of a return value from this function. Additionally, if the + // sym is false, that means nothing can traverse it, so we simply are left + // with no edges. + if (lower_bound.empty() && sym != bddfalse) + { + lower_bound.insert(sym); + } + return lower_bound; + } + twa_graph_ptr split_edges(const const_twa_graph_ptr& aut) { twa_graph_ptr out = make_twa_graph(aut->get_dict()); @@ -77,4 +268,60 @@ namespace spot } return out; } + + twa_graph_ptr split_edges(const const_twa_graph_ptr& aut, + std::vector const& basis) + { + twa_graph_ptr out = make_twa_graph(aut->get_dict()); + out->copy_acceptance_of(aut); + out->copy_ap_of(aut); + out->prop_copy(aut, twa::prop_set::all()); + out->new_states(aut->num_states()); + out->set_init_state(aut->get_init_state_number()); + + // We use a cache to avoid the costly loop around minterms_of(). + // Cache entries have the form (id, [begin, end]) where id is the + // number of a BDD that as been (or will be) split, and begin/end + // denotes a range of existing transition numbers that cover the + // split. + using cached_t = std::pair; + std::unordered_map split_cond; + internal::univ_dest_mapper uniq(out->get_graph()); + + for (auto& e: aut->edges()) + { + bdd const& cond = e.cond; + unsigned dst = e.dst; + + if (cond == bddfalse) + continue; + if (aut->is_univ_dest(dst)) + { + auto d = aut->univ_dests(dst); + dst = uniq.new_univ_dests(d.begin(), d.end()); + } + + auto& [begin, end] = split_cond[cond.id()]; + if (begin == end) + { + begin = out->num_edges() + 1; + auto split = generate_contained_or_disjoint_symbols(cond, + basis); + for (bdd minterm : split) + { + out->new_edge(e.src, dst, minterm, e.acc); + } + end = out->num_edges() + 1; + } + else + { + auto& g = out->get_graph(); + for (unsigned i = begin; i < end; ++i) + { + out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc); + } + } + } + return out; + } } diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh index 7bfe7b02c..54490ab8b 100644 --- a/spot/twaalgos/split.hh +++ b/spot/twaalgos/split.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2017, 2018, 2020, 2023 Laboratoire de Recherche +// et Développement de l'Epita. IMDEA Software Institute. // // This file is part of Spot, a model checking library. // @@ -20,6 +20,7 @@ #pragma once #include +#include namespace spot { @@ -28,7 +29,17 @@ namespace spot /// /// Create a new version of the automaton where all edges are split /// so that they are all labeled by a conjunction of all atomic - /// propositions. After this we can consider that each edge of the + /// propositions. After this we can consider that each edge of the /// automate is a transition labeled by one letter. SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut); + + /// \ingroup twa_misc + /// \brief transform edges into transitions based on set of bdds + /// + /// Create a new version of the automaton where all edges are split + /// such that, for any transformed edge and any set of symbols in + /// the basis, the transformed edge is either completely disjoint + /// from the set of symbols, or it is a subset of them. + SPOT_API twa_graph_ptr split_edges( + const const_twa_graph_ptr& aut, std::vector const& basis); } diff --git a/tests/Makefile.am b/tests/Makefile.am index db70e8810..3cca3e975 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -461,6 +461,7 @@ TESTS_python = \ python/simstate.py \ python/sonf.py \ python/split.py \ + python/splitedge.py \ python/streett_totgba.py \ python/streett_totgba2.py \ python/stutter.py \ diff --git a/tests/python/splitedge.py b/tests/python/splitedge.py new file mode 100644 index 000000000..fa9ff4358 --- /dev/null +++ b/tests/python/splitedge.py @@ -0,0 +1,215 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020-2022 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, buddy +from unittest import TestCase +tc = TestCase() + +def create_aps(aut): + return [buddy.bdd_ithvar(aut.register_ap(ap.ap_name())) for ap in aut.ap()] + +def do_edge_test(aut, aps, edges_before, edges_after): + tc.assertEqual(aut.num_edges(), edges_before) + aut = spot.split_edges(aut, aps) + tc.assertEqual(aut.num_edges(), edges_after) + +aut = spot.automaton(""" +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 0 +--END--""") + +aps = create_aps(aut) +do_edge_test(aut, aps, 1, 4) + +aut = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 0 +State: 1 +[0&1] 1 +--END--""") + +aps = create_aps(aut) +do_edge_test(aut, aps, 2, 5) + +aut = spot.automaton(""" +HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[f] 0 +--END--""") + +aps = create_aps(aut) +do_edge_test(aut, aps, 0, 0) + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[0|1] 1 +[!1] 2 +State: 1 +State: 2 +--END--""") +# Before: +# State: 0 +# {a, b, c, d} +# {a, b} +# After: +# State : 0 +# {a, b, c}, {d} +# {a, b} + +# a = 00 +# b = 10 +# c = 01 +# d = 11 + +aps = create_aps(aut) +# [{a, b, c}] +aps = [buddy.bdd_not(aps[0]) | buddy.bdd_not(aps[1])] +do_edge_test(aut, aps, 2, 3) + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 1 +[!0] 2 +State: 1 +State: 2 +--END--""") +# Before: +# State: 0 +# {a, b, c, d} +# {a, c} +# After: +# State : 0 +# {a, b}, {c, d} +# {a}, {c} + +# a = 00 +# b = 10 +# c = 01 +# d = 11 + +aps = create_aps(aut) +# [{a, b}, {c, d}] +aps = [buddy.bdd_not(aps[1]), aps[1]] +do_edge_test(aut, aps, 2, 4) + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 1 +[!0&!1 | !0&1] 2 +State: 1 +State: 2 +--END--""") +# Before: +# State: 0 +# {a, b, c, d} +# {a, c} +# After: +# State : 0 +# {a},{b},{c},{d} +# {a},{c} + +# a = 00 +# b = 10 +# c = 01 +# d = 11 + +aps = create_aps(aut) +neg_aps = [buddy.bdd_not(a) for a in aps] +# [{a},{b},{c},{d}] +aps = [ + neg_aps[0] & neg_aps[1], + neg_aps[0] & aps[1], + aps[0] & neg_aps[1], + aps[0] & aps[1] +] + +do_edge_test(aut, aps, 2, 6) + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 1 +[!0&!1 | 0&!1] 2 +State: 1 +State: 2 +--END--""") +# Before +# State: 0 +# {a, b, c, d} +# {a, b} +# After: +# State : 0 +# {a, b, c}, {d} +# {a, b} + +# a = 00 +# b = 10 +# c = 01 +# d = 11 + +aps = create_aps(aut) +neg_aps = [buddy.bdd_not(a) for a in aps] +# [{a, b, c}, {d}] +aps = [ + neg_aps[0] | neg_aps[1], + aps[0] & aps[1] +] +do_edge_test(aut, aps, 2, 3)