alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

split_edges: actually use the cache, and minterms_of()

Browse source 
* spot/twaalgos/split.cc (split_edges): Fix some typos, reported by
Philipp, that were causing the cache not to be used.  Speed up using
minterms_of().
This commit is contained in:
Alexandre Duret-Lutz 2021-04-06 21:26:07 +02:00
parent c58aa678ec
commit f3c42596aa
1 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

30
spot/twaalgos/split.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement // Copyright (C) 2017-2021 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -20,8 +20,8 @@
#include "config.h" #include "config.h"
#include <spot/twaalgos/split.hh> #include <spot/twaalgos/split.hh>
#include <spot/misc/minato.hh> #include <spot/misc/minato.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/misc/bddlt.hh> #include <spot/misc/bddlt.hh>
#include <spot/priv/robin_hood.hh>
#include <algorithm> #include <algorithm>
#include <map> #include <map>
@ -37,10 +37,16 @@ namespace spot
out->new_states(aut->num_states()); out->new_states(aut->num_states());
out->set_init_state(aut->get_init_state_number()); out->set_init_state(aut->get_init_state_number());
internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph()); // 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.
typedef std::pair<unsigned, unsigned> cached_t;
robin_hood::unordered_map<unsigned, cached_t> split_cond;
bdd all = aut->ap_vars(); bdd all = aut->ap_vars();
std::map<unsigned, std::pair<unsigned, unsigned>> split_cond; internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph());
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
@ -57,20 +63,14 @@ namespace spot
auto& [begin, end] = split_cond[cond.id()]; auto& [begin, end] = split_cond[cond.id()];
if (begin == end) if (begin == end)
{ {
begin = aut->num_edges(); begin = out->num_edges() + 1;
for (bdd minterm: minterms_of(cond, all))
while (cond != bddfalse) out->new_edge(e.src, dst, minterm, e.acc);
{ end = out->num_edges() + 1;
bdd cube = bdd_satoneset(cond, all, bddfalse);
cond -= cube;
out->new_edge(e.src, dst, cube, e.acc);
}
end = aut->num_edges();
} }
else else
{ {
auto& g = aut->get_graph(); auto& g = out->get_graph();
for (unsigned i = begin; i < end; ++i) for (unsigned i = begin; i < end; ++i)
out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc); out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc);
} }