1527 lines
42 KiB
C++
1527 lines
42 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2014-2018, 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 <http://www.gnu.org/licenses/>.
|
|
|
|
#pragma once
|
|
|
|
#include <spot/misc/common.hh>
|
|
#include <spot/misc/_config.h>
|
|
#include <vector>
|
|
#include <type_traits>
|
|
#include <tuple>
|
|
#include <cassert>
|
|
#include <iterator>
|
|
#include <algorithm>
|
|
#include <map>
|
|
#include <iostream>
|
|
#ifdef SPOT_ENABLE_PTHREAD
|
|
# include <thread>
|
|
#endif // SPOT_ENABLE_PTHREAD
|
|
|
|
namespace spot
|
|
{
|
|
template <typename State_Data, typename Edge_Data>
|
|
class SPOT_API digraph;
|
|
|
|
namespace internal
|
|
{
|
|
#ifndef SWIG
|
|
template <typename Of, typename ...Args>
|
|
struct first_is_base_of
|
|
{
|
|
static const bool value = false;
|
|
};
|
|
|
|
template <typename Of, typename Arg1, typename ...Args>
|
|
struct first_is_base_of<Of, Arg1, Args...>
|
|
{
|
|
static const bool value =
|
|
std::is_base_of<Of, typename std::decay<Arg1>::type>::value;
|
|
};
|
|
#endif
|
|
|
|
// The boxed_label class stores Data as an attribute called
|
|
// "label" if boxed is true. It is an empty class if Data is
|
|
// void, and it simply inherits from Data if boxed is false.
|
|
//
|
|
// The data() method offers an homogeneous access to the Data
|
|
// instance.
|
|
template <typename Data, bool boxed = !std::is_class<Data>::value>
|
|
struct SPOT_API boxed_label
|
|
{
|
|
typedef Data data_t;
|
|
Data label;
|
|
|
|
#ifndef SWIG
|
|
template <typename... Args,
|
|
typename = typename std::enable_if<
|
|
!first_is_base_of<boxed_label, Args...>::value>::type>
|
|
boxed_label(Args&&... args)
|
|
noexcept(std::is_nothrow_constructible<Data, Args...>::value)
|
|
: label{std::forward<Args>(args)...}
|
|
{
|
|
}
|
|
#endif
|
|
|
|
// if Data is a POD type, G++ 4.8.2 wants default values for all
|
|
// label fields unless we define this default constructor here.
|
|
explicit boxed_label()
|
|
noexcept(std::is_nothrow_constructible<Data>::value)
|
|
{
|
|
}
|
|
|
|
Data& data()
|
|
{
|
|
return label;
|
|
}
|
|
|
|
const Data& data() const
|
|
{
|
|
return label;
|
|
}
|
|
|
|
bool operator<(const boxed_label& other) const
|
|
{
|
|
return label < other.label;
|
|
}
|
|
};
|
|
|
|
template <>
|
|
struct SPOT_API boxed_label<void, true>: public std::tuple<>
|
|
{
|
|
typedef std::tuple<> data_t;
|
|
std::tuple<>& data()
|
|
{
|
|
return *this;
|
|
}
|
|
|
|
const std::tuple<>& data() const
|
|
{
|
|
return *this;
|
|
}
|
|
|
|
};
|
|
|
|
template <typename Data>
|
|
struct SPOT_API boxed_label<Data, false>: public Data
|
|
{
|
|
typedef Data data_t;
|
|
|
|
#ifndef SWIG
|
|
template <typename... Args,
|
|
typename = typename std::enable_if<
|
|
!first_is_base_of<boxed_label, Args...>::value>::type>
|
|
boxed_label(Args&&... args)
|
|
noexcept(std::is_nothrow_constructible<Data, Args...>::value)
|
|
: Data{std::forward<Args>(args)...}
|
|
{
|
|
}
|
|
#endif
|
|
|
|
// if Data is a POD type, G++ 4.8.2 wants default values for all
|
|
// label fields unless we define this default constructor here.
|
|
explicit boxed_label()
|
|
noexcept(std::is_nothrow_constructible<Data>::value)
|
|
{
|
|
}
|
|
|
|
Data& data()
|
|
{
|
|
return *this;
|
|
}
|
|
|
|
const Data& data() const
|
|
{
|
|
return *this;
|
|
}
|
|
};
|
|
|
|
//////////////////////////////////////////////////
|
|
// State storage for digraphs
|
|
//////////////////////////////////////////////////
|
|
|
|
// We have two implementations, one with attached State_Data, and
|
|
// one without.
|
|
|
|
template <typename Edge, typename State_Data>
|
|
struct SPOT_API distate_storage final: public State_Data
|
|
{
|
|
Edge succ = 0; // First outgoing edge (used when iterating)
|
|
Edge succ_tail = 0; // Last outgoing edge (used for
|
|
// appending new edges)
|
|
#ifndef SWIG
|
|
template <typename... Args,
|
|
typename = typename std::enable_if<
|
|
!first_is_base_of<distate_storage, Args...>::value>::type>
|
|
distate_storage(Args&&... args)
|
|
noexcept(std::is_nothrow_constructible<State_Data, Args...>::value)
|
|
: State_Data{std::forward<Args>(args)...}
|
|
{
|
|
}
|
|
#endif
|
|
};
|
|
|
|
//////////////////////////////////////////////////
|
|
// Edge storage
|
|
//////////////////////////////////////////////////
|
|
|
|
// Again two implementation: one with label, and one without.
|
|
|
|
template <typename StateIn,
|
|
typename StateOut, typename Edge, typename Edge_Data>
|
|
struct SPOT_API edge_storage final: public Edge_Data
|
|
{
|
|
typedef Edge edge;
|
|
|
|
StateOut dst; // destination
|
|
Edge next_succ; // next outgoing edge with same
|
|
// source, or 0
|
|
StateIn src; // source
|
|
|
|
explicit edge_storage()
|
|
noexcept(std::is_nothrow_constructible<Edge_Data>::value)
|
|
: Edge_Data{}
|
|
{
|
|
}
|
|
|
|
#ifndef SWIG
|
|
template <typename... Args>
|
|
edge_storage(StateOut dst, Edge next_succ,
|
|
StateIn src, Args&&... args)
|
|
noexcept(std::is_nothrow_constructible<Edge_Data, Args...>::value
|
|
&& std::is_nothrow_constructible<StateOut, StateOut>::value
|
|
&& std::is_nothrow_constructible<Edge, Edge>::value)
|
|
: Edge_Data{std::forward<Args>(args)...},
|
|
dst(dst), next_succ(next_succ), src(src)
|
|
{
|
|
}
|
|
#endif
|
|
|
|
bool operator<(const edge_storage& other) const
|
|
{
|
|
if (src < other.src)
|
|
return true;
|
|
if (src > other.src)
|
|
return false;
|
|
// This might be costly if the destination is a vector
|
|
if (dst < other.dst)
|
|
return true;
|
|
if (dst > other.dst)
|
|
return false;
|
|
return this->data() < other.data();
|
|
}
|
|
|
|
bool operator==(const edge_storage& other) const
|
|
{
|
|
return src == other.src &&
|
|
dst == other.dst &&
|
|
this->data() == other.data();
|
|
}
|
|
};
|
|
|
|
//////////////////////////////////////////////////
|
|
// Edge iterator
|
|
//////////////////////////////////////////////////
|
|
|
|
// This holds a graph and a edge number that is the start of
|
|
// a list, and it iterates over all the edge_storage_t elements
|
|
// of that list.
|
|
|
|
template <typename Graph>
|
|
class SPOT_API edge_iterator
|
|
{
|
|
public:
|
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
|
const typename Graph::edge_storage_t,
|
|
typename Graph::edge_storage_t>::type
|
|
value_type;
|
|
typedef value_type& reference;
|
|
typedef value_type* pointer;
|
|
typedef std::ptrdiff_t difference_type;
|
|
typedef std::forward_iterator_tag iterator_category;
|
|
|
|
typedef typename Graph::edge edge;
|
|
|
|
edge_iterator() noexcept
|
|
: g_(nullptr), t_(0)
|
|
{
|
|
}
|
|
|
|
edge_iterator(Graph* g, edge t) noexcept
|
|
: g_(g), t_(t)
|
|
{
|
|
}
|
|
|
|
bool operator==(edge_iterator o) const
|
|
{
|
|
return t_ == o.t_;
|
|
}
|
|
|
|
bool operator!=(edge_iterator o) const
|
|
{
|
|
return t_ != o.t_;
|
|
}
|
|
|
|
reference operator*() const
|
|
{
|
|
return g_->edge_storage(t_);
|
|
}
|
|
|
|
pointer operator->() const
|
|
{
|
|
return &g_->edge_storage(t_);
|
|
}
|
|
|
|
edge_iterator operator++()
|
|
{
|
|
t_ = operator*().next_succ;
|
|
return *this;
|
|
}
|
|
|
|
edge_iterator operator++(int)
|
|
{
|
|
edge_iterator ti = *this;
|
|
t_ = operator*().next_succ;
|
|
return ti;
|
|
}
|
|
|
|
operator bool() const
|
|
{
|
|
return t_;
|
|
}
|
|
|
|
edge trans() const
|
|
{
|
|
return t_;
|
|
}
|
|
|
|
protected:
|
|
Graph* g_;
|
|
edge t_;
|
|
};
|
|
|
|
template <typename Graph>
|
|
class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
|
|
{
|
|
typedef edge_iterator<Graph> super;
|
|
public:
|
|
typedef typename Graph::state_storage_t state_storage_t;
|
|
typedef typename Graph::edge edge;
|
|
|
|
killer_edge_iterator(Graph* g, edge t, state_storage_t& src) noexcept
|
|
: super(g, t), src_(src), prev_(0)
|
|
{
|
|
}
|
|
|
|
killer_edge_iterator operator++()
|
|
{
|
|
prev_ = this->t_;
|
|
this->t_ = this->operator*().next_succ;
|
|
return *this;
|
|
}
|
|
|
|
killer_edge_iterator operator++(int)
|
|
{
|
|
killer_edge_iterator ti = *this;
|
|
++*this;
|
|
return ti;
|
|
}
|
|
|
|
// Erase the current edge and advance the iterator.
|
|
void erase()
|
|
{
|
|
edge next = this->operator*().next_succ;
|
|
|
|
// Update source state and previous edges
|
|
if (prev_)
|
|
{
|
|
this->g_->edge_storage(prev_).next_succ = next;
|
|
}
|
|
else
|
|
{
|
|
if (src_.succ == this->t_)
|
|
src_.succ = next;
|
|
}
|
|
if (src_.succ_tail == this->t_)
|
|
{
|
|
src_.succ_tail = prev_;
|
|
SPOT_ASSERT(next == 0);
|
|
}
|
|
|
|
// Erased edges have themselves as next_succ.
|
|
this->operator*().next_succ = this->t_;
|
|
|
|
// Advance iterator to next edge.
|
|
this->t_ = next;
|
|
|
|
++this->g_->killed_edge_;
|
|
}
|
|
|
|
protected:
|
|
state_storage_t& src_;
|
|
edge prev_;
|
|
};
|
|
|
|
|
|
//////////////////////////////////////////////////
|
|
// State OUT
|
|
//////////////////////////////////////////////////
|
|
|
|
// Fake container listing the outgoing edges of a state.
|
|
|
|
template <typename Graph>
|
|
class SPOT_API state_out
|
|
{
|
|
public:
|
|
typedef typename Graph::edge edge;
|
|
state_out(Graph* g, edge t) noexcept
|
|
: g_(g), t_(t)
|
|
{
|
|
}
|
|
|
|
edge_iterator<Graph> begin() const
|
|
{
|
|
return {g_, t_};
|
|
}
|
|
|
|
edge_iterator<Graph> end() const
|
|
{
|
|
return {};
|
|
}
|
|
|
|
void recycle(edge t)
|
|
{
|
|
t_ = t;
|
|
}
|
|
|
|
protected:
|
|
Graph* g_;
|
|
edge t_;
|
|
};
|
|
|
|
//////////////////////////////////////////////////
|
|
// all_trans
|
|
//////////////////////////////////////////////////
|
|
|
|
template <typename Graph>
|
|
class SPOT_API all_edge_iterator
|
|
{
|
|
public:
|
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
|
const typename Graph::edge_storage_t,
|
|
typename Graph::edge_storage_t>::type
|
|
value_type;
|
|
typedef value_type& reference;
|
|
typedef value_type* pointer;
|
|
typedef std::ptrdiff_t difference_type;
|
|
typedef std::forward_iterator_tag iterator_category;
|
|
|
|
protected:
|
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
|
const typename Graph::edge_vector_t,
|
|
typename Graph::edge_vector_t>::type
|
|
tv_t;
|
|
|
|
unsigned t_;
|
|
tv_t& tv_;
|
|
|
|
void skip_()
|
|
{
|
|
unsigned s = tv_.size();
|
|
do
|
|
++t_;
|
|
while (t_ < s && tv_[t_].next_succ == t_);
|
|
}
|
|
|
|
public:
|
|
all_edge_iterator(unsigned pos, tv_t& tv) noexcept
|
|
: t_(pos), tv_(tv)
|
|
{
|
|
skip_();
|
|
}
|
|
|
|
all_edge_iterator(tv_t& tv) noexcept
|
|
: t_(tv.size()), tv_(tv)
|
|
{
|
|
}
|
|
|
|
all_edge_iterator& operator++()
|
|
{
|
|
skip_();
|
|
return *this;
|
|
}
|
|
|
|
all_edge_iterator operator++(int)
|
|
{
|
|
all_edge_iterator old = *this;
|
|
++*this;
|
|
return old;
|
|
}
|
|
|
|
bool operator==(all_edge_iterator o) const
|
|
{
|
|
return t_ == o.t_;
|
|
}
|
|
|
|
bool operator!=(all_edge_iterator o) const
|
|
{
|
|
return t_ != o.t_;
|
|
}
|
|
|
|
reference operator*() const
|
|
{
|
|
return tv_[t_];
|
|
}
|
|
|
|
pointer operator->() const
|
|
{
|
|
return &tv_[t_];
|
|
}
|
|
};
|
|
|
|
|
|
template <typename Graph>
|
|
class SPOT_API all_trans
|
|
{
|
|
public:
|
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
|
const typename Graph::edge_vector_t,
|
|
typename Graph::edge_vector_t>::type
|
|
tv_t;
|
|
typedef all_edge_iterator<Graph> iter_t;
|
|
private:
|
|
tv_t& tv_;
|
|
public:
|
|
|
|
all_trans(tv_t& tv) noexcept
|
|
: tv_(tv)
|
|
{
|
|
}
|
|
|
|
iter_t begin() const
|
|
{
|
|
return {0, tv_};
|
|
}
|
|
|
|
iter_t end() const
|
|
{
|
|
return {tv_};
|
|
}
|
|
};
|
|
|
|
class SPOT_API const_universal_dests
|
|
{
|
|
private:
|
|
const unsigned* begin_;
|
|
const unsigned* end_;
|
|
unsigned tmp_;
|
|
public:
|
|
const_universal_dests(const unsigned* begin, const unsigned* end) noexcept
|
|
: begin_(begin), end_(end)
|
|
{
|
|
}
|
|
|
|
const_universal_dests(unsigned state) noexcept
|
|
: begin_(&tmp_), end_(&tmp_ + 1), tmp_(state)
|
|
{
|
|
}
|
|
|
|
const unsigned* begin() const
|
|
{
|
|
return begin_;
|
|
}
|
|
|
|
const unsigned* end() const
|
|
{
|
|
return end_;
|
|
}
|
|
};
|
|
|
|
template<class G>
|
|
class univ_dest_mapper
|
|
{
|
|
std::map<std::vector<unsigned>, unsigned> uniq_;
|
|
G& g_;
|
|
unsigned acc_sink_;
|
|
public:
|
|
|
|
univ_dest_mapper(G& graph, unsigned sink = -1u)
|
|
: g_(graph), acc_sink_(sink)
|
|
{
|
|
}
|
|
|
|
template<class I>
|
|
unsigned new_univ_dests(I begin, I end)
|
|
{
|
|
std::vector<unsigned> tmp(begin, end);
|
|
std::sort(tmp.begin(), tmp.end());
|
|
tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
|
|
if (acc_sink_ != -1u && tmp.size() > 1)
|
|
tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_),
|
|
tmp.end());
|
|
auto p = uniq_.emplace(tmp, 0);
|
|
if (p.second)
|
|
p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());
|
|
return p.first->second;
|
|
}
|
|
|
|
};
|
|
|
|
} // namespace internal
|
|
|
|
|
|
/// \brief A directed graph
|
|
///
|
|
/// \tparam State_Data data to attach to states
|
|
/// \tparam Edge_Data data to attach to edges
|
|
template <typename State_Data, typename Edge_Data>
|
|
class digraph
|
|
{
|
|
friend class internal::edge_iterator<digraph>;
|
|
friend class internal::edge_iterator<const digraph>;
|
|
friend class internal::killer_edge_iterator<digraph>;
|
|
|
|
public:
|
|
typedef internal::edge_iterator<digraph> iterator;
|
|
typedef internal::edge_iterator<const digraph> const_iterator;
|
|
|
|
// Extra data to store on each state or edge.
|
|
typedef State_Data state_data_t;
|
|
typedef Edge_Data edge_data_t;
|
|
|
|
// State and edges are identified by their indices in some
|
|
// vector.
|
|
typedef unsigned state;
|
|
typedef unsigned edge;
|
|
|
|
typedef internal::distate_storage<edge,
|
|
internal::boxed_label<State_Data>>
|
|
state_storage_t;
|
|
typedef internal::edge_storage<state, state, edge,
|
|
internal::boxed_label<Edge_Data>>
|
|
edge_storage_t;
|
|
typedef std::vector<state_storage_t> state_vector;
|
|
typedef std::vector<edge_storage_t> edge_vector_t;
|
|
|
|
// A sequence of universal destination groups of the form:
|
|
// (n state_1 state_2 ... state_n)*
|
|
typedef std::vector<unsigned> dests_vector_t;
|
|
|
|
protected:
|
|
state_vector states_;
|
|
edge_vector_t edges_;
|
|
dests_vector_t dests_; // Only used by alternating automata.
|
|
// Number of erased edges.
|
|
unsigned killed_edge_;
|
|
public:
|
|
/// \brief Construct an empty graph
|
|
///
|
|
/// Construct an empty graph, and reserve space for \a max_states
|
|
/// states and \a max_trans edges. These are not hard
|
|
/// limits, but just hints to pre-allocate a data structure that
|
|
/// may hold that much items.
|
|
digraph(unsigned max_states = 10, unsigned max_trans = 0)
|
|
: killed_edge_(0)
|
|
{
|
|
states_.reserve(max_states);
|
|
if (max_trans == 0)
|
|
max_trans = max_states * 2;
|
|
edges_.reserve(max_trans + 1);
|
|
// Edge number 0 is not used, because we use this index
|
|
// to mark the absence of a edge.
|
|
edges_.resize(1);
|
|
// This causes edge 0 to be considered as dead.
|
|
edges_[0].next_succ = 0;
|
|
}
|
|
|
|
/// The number of states in the automaton
|
|
unsigned num_states() const
|
|
{
|
|
return states_.size();
|
|
}
|
|
|
|
/// \brief The number of edges in the automaton
|
|
///
|
|
/// Killed edges are omitted.
|
|
unsigned num_edges() const
|
|
{
|
|
return edges_.size() - killed_edge_ - 1;
|
|
}
|
|
|
|
/// Whether the automaton uses only existential branching.
|
|
bool is_existential() const
|
|
{
|
|
return dests_.empty();
|
|
}
|
|
|
|
/// \brief Create a new states
|
|
///
|
|
/// All arguments are forwarded to the State_Data constructor.
|
|
///
|
|
/// \return a state number
|
|
template <typename... Args>
|
|
state new_state(Args&&... args)
|
|
{
|
|
state s = states_.size();
|
|
states_.emplace_back(std::forward<Args>(args)...);
|
|
return s;
|
|
}
|
|
|
|
/// \brief Create n new states
|
|
///
|
|
/// All arguments are forwarded to the State_Data constructor of
|
|
/// each of the n states.
|
|
///
|
|
/// \return the first state number
|
|
template <typename... Args>
|
|
state new_states(unsigned n, Args&&... args)
|
|
{
|
|
state s = states_.size();
|
|
states_.reserve(s + n);
|
|
while (n--)
|
|
states_.emplace_back(std::forward<Args>(args)...);
|
|
return s;
|
|
}
|
|
|
|
/// @{
|
|
/// \brief return a reference to the storage of a state
|
|
///
|
|
/// The storage includes any of the user-supplied State_Data, plus
|
|
/// some custom fields needed to find the outgoing transitions.
|
|
state_storage_t&
|
|
state_storage(state s)
|
|
{
|
|
return states_[s];
|
|
}
|
|
|
|
const state_storage_t&
|
|
state_storage(state s) const
|
|
{
|
|
return states_[s];
|
|
}
|
|
///@}
|
|
|
|
///@{
|
|
/// \brief return the State_Data associated to a state
|
|
///
|
|
/// This does not use State_Data& as return type, because
|
|
/// State_Data might be void.
|
|
typename state_storage_t::data_t&
|
|
state_data(state s)
|
|
{
|
|
return states_[s].data();
|
|
}
|
|
|
|
const typename state_storage_t::data_t&
|
|
state_data(state s) const
|
|
{
|
|
return states_[s].data();
|
|
}
|
|
///@}
|
|
|
|
///@{
|
|
/// \brief return a reference to the storage of an edge
|
|
///
|
|
/// The storage includes any of the user-supplied Edge_Data, plus
|
|
/// some custom fields needed to find the next transitions.
|
|
edge_storage_t&
|
|
edge_storage(edge s)
|
|
{
|
|
return edges_[s];
|
|
}
|
|
|
|
const edge_storage_t&
|
|
edge_storage(edge s) const
|
|
{
|
|
return edges_[s];
|
|
}
|
|
///@}
|
|
|
|
///@{
|
|
/// \brief return the Edgeg_Data of an edge.
|
|
///
|
|
/// This does not use Edge_Data& as return type, because
|
|
/// Edge_Data might be void.
|
|
typename edge_storage_t::data_t&
|
|
edge_data(edge s)
|
|
{
|
|
return edges_[s].data();
|
|
}
|
|
|
|
const typename edge_storage_t::data_t&
|
|
edge_data(edge s) const
|
|
{
|
|
return edges_[s].data();
|
|
}
|
|
///@}
|
|
|
|
/// \brief Create a new edge
|
|
///
|
|
/// \param src the source state
|
|
/// \param dst the destination state
|
|
/// \param args arguments to forward to the Edge_Data constructor
|
|
template <typename... Args>
|
|
edge
|
|
new_edge(state src, state dst, Args&&... args)
|
|
{
|
|
edge t = edges_.size();
|
|
edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
|
|
|
|
edge st = states_[src].succ_tail;
|
|
SPOT_ASSERT(st < t || !st);
|
|
if (!st)
|
|
states_[src].succ = t;
|
|
else
|
|
edges_[st].next_succ = t;
|
|
states_[src].succ_tail = t;
|
|
return t;
|
|
}
|
|
|
|
/// \brief Create a new universal destination group
|
|
///
|
|
/// The resulting state number can be used as the destination of
|
|
/// an edge.
|
|
///
|
|
/// \param dst_begin start of a non-empty container of destination states
|
|
/// \param dst_end end of a non-empty container of destination states
|
|
template <typename I>
|
|
state
|
|
new_univ_dests(I dst_begin, I dst_end)
|
|
{
|
|
unsigned sz = std::distance(dst_begin, dst_end);
|
|
if (sz == 1)
|
|
return *dst_begin;
|
|
SPOT_ASSERT(sz > 1);
|
|
unsigned d = dests_.size();
|
|
if (!dests_.empty()
|
|
&& &*dst_begin >= &dests_.front()
|
|
&& &*dst_begin <= &dests_.back()
|
|
&& (dests_.capacity() - dests_.size()) < (sz + 1))
|
|
{
|
|
// If dst_begin...dst_end points into dests_ and dests_ risk
|
|
// being reallocated, we have to savea the destination
|
|
// states before we lose them.
|
|
std::vector<unsigned> tmp(dst_begin, dst_end);
|
|
dests_.emplace_back(sz);
|
|
dests_.insert(dests_.end(), tmp.begin(), tmp.end());
|
|
}
|
|
else
|
|
{
|
|
dests_.emplace_back(sz);
|
|
dests_.insert(dests_.end(), dst_begin, dst_end);
|
|
}
|
|
return ~d;
|
|
}
|
|
|
|
/// \brief Create a new universal edge
|
|
///
|
|
/// \param src the source state
|
|
/// \param dst_begin start of a non-empty container of destination states
|
|
/// \param dst_end end of a non-empty container of destination states
|
|
/// \param args arguments to forward to the Edge_Data constructor
|
|
template <typename I, typename... Args>
|
|
edge
|
|
new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args)
|
|
{
|
|
return new_edge(src, new_univ_dests(dst_begin, dst_end),
|
|
std::forward<Args>(args)...);
|
|
}
|
|
|
|
/// \brief Create a new universal edge
|
|
///
|
|
/// \param src the source state
|
|
/// \param dsts a non-empty list of destination states
|
|
/// \param args arguments to forward to the Edge_Data constructor
|
|
template <typename... Args>
|
|
edge
|
|
new_univ_edge(state src, const std::initializer_list<state>& dsts,
|
|
Args&&... args)
|
|
{
|
|
return new_univ_edge(src, dsts.begin(), dsts.end(),
|
|
std::forward<Args>(args)...);
|
|
}
|
|
|
|
internal::const_universal_dests univ_dests(state src) const
|
|
{
|
|
if ((int)src < 0)
|
|
{
|
|
unsigned pos = ~src;
|
|
const unsigned* d = dests_.data();
|
|
d += pos;
|
|
unsigned num = *d;
|
|
return { d + 1, d + num + 1 };
|
|
}
|
|
else
|
|
{
|
|
return src;
|
|
}
|
|
}
|
|
|
|
internal::const_universal_dests univ_dests(const edge_storage_t& e) const
|
|
{
|
|
return univ_dests(e.dst);
|
|
}
|
|
|
|
/// Convert a storage reference into a state number
|
|
state index_of_state(const state_storage_t& ss) const
|
|
{
|
|
SPOT_ASSERT(!states_.empty());
|
|
return &ss - &states_.front();
|
|
}
|
|
|
|
/// Convert a storage reference into an edge number
|
|
edge index_of_edge(const edge_storage_t& tt) const
|
|
{
|
|
SPOT_ASSERT(!edges_.empty());
|
|
return &tt - &edges_.front();
|
|
}
|
|
|
|
/// @{
|
|
/// \brief Return a fake container with all edges leaving \a src
|
|
internal::state_out<digraph>
|
|
out(state src)
|
|
{
|
|
return {this, states_[src].succ};
|
|
}
|
|
|
|
internal::state_out<digraph>
|
|
out(state_storage_t& src)
|
|
{
|
|
return out(index_of_state(src));
|
|
}
|
|
|
|
internal::state_out<const digraph>
|
|
out(state src) const
|
|
{
|
|
return {this, states_[src].succ};
|
|
}
|
|
|
|
internal::state_out<const digraph>
|
|
out(state_storage_t& src) const
|
|
{
|
|
return out(index_of_state(src));
|
|
}
|
|
/// @}
|
|
|
|
/// @{
|
|
///
|
|
/// \brief Return a fake container with all edges leaving \a src,
|
|
/// allowing erasure.
|
|
internal::killer_edge_iterator<digraph>
|
|
out_iteraser(state_storage_t& src)
|
|
{
|
|
return {this, src.succ, src};
|
|
}
|
|
|
|
internal::killer_edge_iterator<digraph>
|
|
out_iteraser(state src)
|
|
{
|
|
return out_iteraser(state_storage(src));
|
|
}
|
|
///@}
|
|
|
|
/// @{
|
|
///
|
|
/// \brief Return the vector of states.
|
|
const state_vector& states() const
|
|
{
|
|
return states_;
|
|
}
|
|
|
|
state_vector& states()
|
|
{
|
|
return states_;
|
|
}
|
|
/// @}
|
|
|
|
/// @{
|
|
///
|
|
/// \brief Return a fake container with all edges (exluding erased
|
|
/// edges)
|
|
internal::all_trans<const digraph> edges() const
|
|
{
|
|
return edges_;
|
|
}
|
|
|
|
internal::all_trans<digraph> edges()
|
|
{
|
|
return edges_;
|
|
}
|
|
/// @}
|
|
|
|
/// @{
|
|
/// \brief Return the vector of all edges.
|
|
///
|
|
/// When using this method, beware that the first entry (edge #0)
|
|
/// is not a real edge, and that any edge with next_succ pointing
|
|
/// to itself is an erased edge.
|
|
///
|
|
/// You should probably use edges() instead.
|
|
const edge_vector_t& edge_vector() const
|
|
{
|
|
return edges_;
|
|
}
|
|
|
|
edge_vector_t& edge_vector()
|
|
{
|
|
return edges_;
|
|
}
|
|
/// @}
|
|
|
|
/// \brief Test whether the given edge is valid.
|
|
///
|
|
/// An edge is valid if its number is less than the total number
|
|
/// of edges, and it does not correspond to an erased (dead) edge.
|
|
///
|
|
/// \see is_dead_edge()
|
|
bool is_valid_edge(edge t) const
|
|
{
|
|
// Erased edges have their next_succ pointing to
|
|
// themselves.
|
|
return (t < edges_.size() &&
|
|
edges_[t].next_succ != t);
|
|
}
|
|
|
|
/// @{
|
|
/// \brief Tests whether an edge has been erased.
|
|
///
|
|
/// \see is_valid_edge
|
|
bool is_dead_edge(unsigned t) const
|
|
{
|
|
return edges_[t].next_succ == t;
|
|
}
|
|
|
|
bool is_dead_edge(const edge_storage_t& t) const
|
|
{
|
|
return t.next_succ == index_of_edge(t);
|
|
}
|
|
/// @}
|
|
|
|
/// @{
|
|
/// \brief The vector used to store universal destinations.
|
|
///
|
|
/// The actual way those destinations are stored is an
|
|
/// implementation detail you should not rely on.
|
|
const dests_vector_t& dests_vector() const
|
|
{
|
|
return dests_;
|
|
}
|
|
|
|
dests_vector_t& dests_vector()
|
|
{
|
|
return dests_;
|
|
}
|
|
/// @}
|
|
|
|
/// Dump the state and edge storage for debugging
|
|
void dump_storage(std::ostream& o) const
|
|
{
|
|
unsigned tend = edges_.size();
|
|
for (unsigned t = 1; t < tend; ++t)
|
|
{
|
|
o << 't' << t << ": (s"
|
|
<< edges_[t].src << ", ";
|
|
int d = edges_[t].dst;
|
|
if (d < 0)
|
|
o << 'd' << ~d;
|
|
else
|
|
o << 's' << d;
|
|
o << ") t" << edges_[t].next_succ << '\n';
|
|
}
|
|
unsigned send = states_.size();
|
|
for (unsigned s = 0; s < send; ++s)
|
|
{
|
|
o << 's' << s << ": t"
|
|
<< states_[s].succ << " t"
|
|
<< states_[s].succ_tail << '\n';
|
|
}
|
|
unsigned dend = dests_.size();
|
|
unsigned size = 0;
|
|
for (unsigned s = 0; s < dend; ++s)
|
|
{
|
|
o << 'd' << s << ": ";
|
|
if (size == 0)
|
|
{
|
|
o << '#';
|
|
size = dests_[s];
|
|
}
|
|
else
|
|
{
|
|
o << 's';
|
|
--size;
|
|
}
|
|
o << dests_[s] << '\n';
|
|
}
|
|
}
|
|
|
|
enum dump_storage_items {
|
|
DSI_GraphHeader = 1,
|
|
DSI_GraphFooter = 2,
|
|
DSI_StatesHeader = 4,
|
|
DSI_StatesBody = 8,
|
|
DSI_StatesFooter = 16,
|
|
DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter,
|
|
DSI_EdgesHeader = 32,
|
|
DSI_EdgesBody = 64,
|
|
DSI_EdgesFooter = 128,
|
|
DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter,
|
|
DSI_DestsHeader = 256,
|
|
DSI_DestsBody = 512,
|
|
DSI_DestsFooter = 1024,
|
|
DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter,
|
|
DSI_All =
|
|
DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter,
|
|
};
|
|
|
|
/// Dump the state and edge storage for debugging
|
|
void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const
|
|
{
|
|
if (dsi & DSI_GraphHeader)
|
|
o << "digraph g { \nnode [shape=plaintext]\n";
|
|
unsigned send = states_.size();
|
|
if (dsi & DSI_StatesHeader)
|
|
{
|
|
o << ("states [label=<\n"
|
|
"<table border='0' cellborder='1' cellspacing='0'>\n"
|
|
"<tr><td sides='b' bgcolor='yellow' port='s'>states</td>\n");
|
|
for (unsigned s = 0; s < send; ++s)
|
|
o << "<td sides='b' bgcolor='yellow' port='s" << s << "'>"
|
|
<< s << "</td>\n";
|
|
o << "</tr>\n";
|
|
}
|
|
if (dsi & DSI_StatesBody)
|
|
{
|
|
o << "<tr><td port='ss'>succ</td>\n";
|
|
for (unsigned s = 0; s < send; ++s)
|
|
{
|
|
o << "<td port='ss" << s;
|
|
if (states_[s].succ)
|
|
o << "' bgcolor='cyan";
|
|
o << "'>" << states_[s].succ << "</td>\n";
|
|
}
|
|
o << "</tr><tr><td port='st'>succ_tail</td>\n";
|
|
for (unsigned s = 0; s < send; ++s)
|
|
{
|
|
o << "<td port='st" << s;
|
|
if (states_[s].succ_tail)
|
|
o << "' bgcolor='cyan";
|
|
o << "'>" << states_[s].succ_tail << "</td>\n";
|
|
}
|
|
o << "</tr>\n";
|
|
}
|
|
if (dsi & DSI_StatesFooter)
|
|
o << "</table>>]\n";
|
|
unsigned eend = edges_.size();
|
|
if (dsi & DSI_EdgesHeader)
|
|
{
|
|
o << ("edges [label=<\n"
|
|
"<table border='0' cellborder='1' cellspacing='0'>\n"
|
|
"<tr><td sides='b' bgcolor='cyan' port='e'>edges</td>\n");
|
|
for (unsigned e = 1; e < eend; ++e)
|
|
{
|
|
o << "<td sides='b' bgcolor='"
|
|
<< (e != edges_[e].next_succ ? "cyan" : "gray")
|
|
<< "' port='e" << e << "'>" << e << "</td>\n";
|
|
}
|
|
o << "</tr>";
|
|
}
|
|
if (dsi & DSI_EdgesBody)
|
|
{
|
|
o << "<tr><td port='ed'>dst</td>\n";
|
|
for (unsigned e = 1; e < eend; ++e)
|
|
{
|
|
o << "<td port='ed" << e;
|
|
int d = edges_[e].dst;
|
|
if (d < 0)
|
|
o << "' bgcolor='pink'>~" << ~d;
|
|
else
|
|
o << "' bgcolor='yellow'>" << d;
|
|
o << "</td>\n";
|
|
}
|
|
o << "</tr><tr><td port='en'>next_succ</td>\n";
|
|
for (unsigned e = 1; e < eend; ++e)
|
|
{
|
|
o << "<td port='en" << e;
|
|
if (edges_[e].next_succ)
|
|
{
|
|
if (edges_[e].next_succ != e)
|
|
o << "' bgcolor='cyan";
|
|
else
|
|
o << "' bgcolor='gray";
|
|
}
|
|
o << "'>" << edges_[e].next_succ << "</td>\n";
|
|
}
|
|
o << "</tr><tr><td port='es'>src</td>\n";
|
|
for (unsigned e = 1; e < eend; ++e)
|
|
o << "<td port='es" << e << "' bgcolor='yellow'>"
|
|
<< edges_[e].src << "</td>\n";
|
|
o << "</tr>\n";
|
|
}
|
|
if (dsi & DSI_EdgesFooter)
|
|
o << "</table>>]\n";
|
|
if (!dests_.empty())
|
|
{
|
|
unsigned dend = dests_.size();
|
|
if (dsi & DSI_DestsHeader)
|
|
{
|
|
o << ("dests [label=<\n"
|
|
"<table border='0' cellborder='1' cellspacing='0'>\n"
|
|
"<tr><td sides='b' bgcolor='pink' port='d'>dests</td>\n");
|
|
unsigned d = 0;
|
|
while (d < dend)
|
|
{
|
|
o << "<td sides='b' bgcolor='pink' port='d"
|
|
<< d << "'>~" << d << "</td>\n";
|
|
unsigned cnt = dests_[d];
|
|
d += cnt + 1;
|
|
while (cnt--)
|
|
o << "<td sides='b'></td>\n";
|
|
}
|
|
o << "</tr>\n";
|
|
}
|
|
if (dsi & DSI_DestsBody)
|
|
{
|
|
o << "<tr><td port='dd'>#cnt/dst</td>\n";
|
|
unsigned d = 0;
|
|
while (d < dend)
|
|
{
|
|
unsigned cnt = dests_[d];
|
|
o << "<td port='d'>#" << cnt << "</td>\n";
|
|
++d;
|
|
while (cnt--)
|
|
{
|
|
o << "<td bgcolor='yellow' port='dd"
|
|
<< d << "'>" << dests_[d] << "</td>\n";
|
|
++d;
|
|
}
|
|
}
|
|
o << "</tr>\n";
|
|
}
|
|
if (dsi & DSI_DestsFooter)
|
|
o << "</table>>]\n";
|
|
}
|
|
if (dsi & DSI_GraphFooter)
|
|
o << "}\n";
|
|
}
|
|
|
|
/// \brief Remove all dead edges.
|
|
///
|
|
/// The edges_ vector is left in a state that is incorrect and
|
|
/// should eventually be fixed by a call to chain_edges_() before
|
|
/// any iteration on the successor of a state is performed.
|
|
void remove_dead_edges_()
|
|
{
|
|
if (killed_edge_ == 0)
|
|
return;
|
|
auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
|
|
[this](const edge_storage_t& t) {
|
|
return this->is_dead_edge(t);
|
|
});
|
|
edges_.erase(i, edges_.end());
|
|
killed_edge_ = 0;
|
|
}
|
|
|
|
/// \brief Sort all edges according to a predicate
|
|
///
|
|
/// This will invalidate all iterators, and also destroy edge
|
|
/// chains. Call chain_edges_() immediately afterwards unless you
|
|
/// know what you are doing.
|
|
template<class Predicate = std::less<edge_storage_t>>
|
|
void sort_edges_(Predicate p = Predicate())
|
|
{
|
|
//std::cerr << "\nbefore\n";
|
|
//dump_storage(std::cerr);
|
|
std::stable_sort(edges_.begin() + 1, edges_.end(), p);
|
|
}
|
|
|
|
/// \brief Sort all edges by src first, then, within edges of the same
|
|
/// source use the predicate
|
|
///
|
|
/// This will invalidate all iterators, and also destroy edge
|
|
/// chains. Call chain_edges_() immediately afterwards unless you
|
|
/// know what you are doing.
|
|
/// \note: for performance this will work in parallel (if enabled)
|
|
/// and make a temporary copy of the edges (needs more ram)
|
|
/// \pre This needs the edge_vector to be in a coherent state when called
|
|
template<class Predicate = std::less<edge_storage_t>>
|
|
void sort_edges_srcfirst_(Predicate p = Predicate(),
|
|
parallel_policy ppolicy = parallel_policy())
|
|
{
|
|
SPOT_ASSERT(!edges_.empty());
|
|
const unsigned ns = num_states();
|
|
std::vector<unsigned> idx_list(ns+1);
|
|
edge_vector_t new_edges;
|
|
new_edges.reserve(edges_.size());
|
|
new_edges.resize(1);
|
|
// This causes edge 0 to be considered as dead.
|
|
new_edges[0].next_succ = 0;
|
|
// Copy all edges so that they are sorted by src
|
|
for (unsigned s = 0; s < ns; ++s)
|
|
{
|
|
idx_list[s] = new_edges.size();
|
|
for (const auto& e : out(s))
|
|
new_edges.push_back(e);
|
|
}
|
|
idx_list[ns] = new_edges.size();
|
|
// New edge sorted by source
|
|
// If we have few edge or only one threads
|
|
// Benchmark few?
|
|
auto bne = new_edges.begin();
|
|
#ifndef SPOT_ENABLE_PTHREAD
|
|
(void) ppolicy;
|
|
#else
|
|
unsigned nthreads = ppolicy.nthreads();
|
|
if (nthreads <= 1)
|
|
#endif
|
|
{
|
|
for (unsigned s = 0u; s < ns; ++s)
|
|
std::stable_sort(bne + idx_list[s],
|
|
bne + idx_list[s+1], p);
|
|
}
|
|
#ifdef SPOT_ENABLE_PTHREAD
|
|
else
|
|
{
|
|
static std::vector<std::thread> tv;
|
|
SPOT_ASSERT(tv.empty());
|
|
tv.resize(nthreads);
|
|
// FIXME: Due to the way these thread advance into the state
|
|
// vector, they access very close memory location. It would
|
|
// seems more cache friendly to have threads work on blocks
|
|
// of continuous states.
|
|
for (unsigned id = 0; id < nthreads; ++id)
|
|
tv[id] = std::thread(
|
|
[bne, id, ns, &idx_list, p, nthreads]()
|
|
{
|
|
for (unsigned s = id; s < ns; s += nthreads)
|
|
std::stable_sort(bne + idx_list[s],
|
|
bne + idx_list[s+1], p);
|
|
return;
|
|
});
|
|
for (auto& t : tv)
|
|
t.join();
|
|
tv.clear();
|
|
}
|
|
#endif
|
|
std::swap(edges_, new_edges);
|
|
// Like after normal sort_edges, they need to be chained before usage
|
|
}
|
|
|
|
/// \brief Sort edges of the given states
|
|
///
|
|
/// \tparam Predicate : Comparison type
|
|
/// \param p : Comparison callable
|
|
/// \param to_sort_ptr : which states to sort. If null, all will be sorted
|
|
/// \note No need to call chain_edges_, they are in a coherent state.
|
|
/// todo: If pred does not involve bdd action other than id -> parallelize
|
|
template<bool Stable = false, class Predicate = std::less<edge_storage_t>>
|
|
void sort_edges_of_(Predicate p = Predicate(),
|
|
const std::vector<bool>* to_sort_ptr = nullptr)
|
|
{
|
|
SPOT_ASSERT((to_sort_ptr == nullptr)
|
|
|| (to_sort_ptr->size() == num_states()));
|
|
//std::cerr << "\nbefore\n";
|
|
//dump_storage(std::cerr);
|
|
auto pi = [&](unsigned t1, unsigned t2)
|
|
{return p(edges_[t1], edges_[t2]); };
|
|
|
|
// Sort the outgoing edges of each selected state according
|
|
// to predicate p. Do that in place.
|
|
std::vector<unsigned> sort_idx_;
|
|
unsigned ns = num_states();
|
|
for (unsigned i = 0; i < ns; ++i)
|
|
{
|
|
if (to_sort_ptr && !(*to_sort_ptr)[i])
|
|
continue;
|
|
unsigned t = states_[i].succ;
|
|
if (t == 0)
|
|
continue;
|
|
sort_idx_.clear();
|
|
do
|
|
{
|
|
sort_idx_.push_back(t);
|
|
t = edges_[t].next_succ;
|
|
} while (t != 0);
|
|
if constexpr (Stable)
|
|
std::stable_sort(sort_idx_.begin(), sort_idx_.end(), pi);
|
|
else
|
|
std::sort(sort_idx_.begin(), sort_idx_.end(), pi);
|
|
// Update the graph
|
|
states_[i].succ = sort_idx_.front();
|
|
states_[i].succ_tail = sort_idx_.back();
|
|
const unsigned n_outs_n1 = sort_idx_.size() - 1;
|
|
for (unsigned k = 0; k < n_outs_n1; ++k)
|
|
edges_[sort_idx_[k]].next_succ = sort_idx_[k+1];
|
|
edges_[sort_idx_.back()].next_succ = 0; // terminal
|
|
}
|
|
// Done
|
|
}
|
|
|
|
/// \brief Reconstruct the chain of outgoing edges
|
|
///
|
|
/// Should be called only when it is known that all edges
|
|
/// with the same source are consecutive in the vector.
|
|
void chain_edges_()
|
|
{
|
|
state last_src = -1U;
|
|
edge tend = edges_.size();
|
|
for (edge t = 1; t < tend; ++t)
|
|
{
|
|
state src = edges_[t].src;
|
|
if (src != last_src)
|
|
{
|
|
states_[src].succ = t;
|
|
if (last_src != -1U)
|
|
{
|
|
states_[last_src].succ_tail = t - 1;
|
|
edges_[t - 1].next_succ = 0;
|
|
}
|
|
while (++last_src != src)
|
|
{
|
|
states_[last_src].succ = 0;
|
|
states_[last_src].succ_tail = 0;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
edges_[t - 1].next_succ = t;
|
|
}
|
|
}
|
|
if (last_src != -1U)
|
|
{
|
|
states_[last_src].succ_tail = tend - 1;
|
|
edges_[tend - 1].next_succ = 0;
|
|
}
|
|
unsigned send = states_.size();
|
|
while (++last_src != send)
|
|
{
|
|
states_[last_src].succ = 0;
|
|
states_[last_src].succ_tail = 0;
|
|
}
|
|
//std::cerr << "\nafter\n";
|
|
//dump_storage(std::cerr);
|
|
}
|
|
|
|
/// \brief Rename all the states in the edge vector.
|
|
///
|
|
/// The edges_ vector is left in a state that is incorrect and
|
|
/// should eventually be fixed by a call to chain_edges_() before
|
|
/// any iteration on the successor of a state is performed.
|
|
void rename_states_(const std::vector<unsigned>& newst)
|
|
{
|
|
SPOT_ASSERT(newst.size() == states_.size());
|
|
unsigned tend = edges_.size();
|
|
for (unsigned t = 1; t < tend; t++)
|
|
{
|
|
edges_[t].dst = newst[edges_[t].dst];
|
|
edges_[t].src = newst[edges_[t].src];
|
|
}
|
|
}
|
|
|
|
/// \brief Rename and remove states.
|
|
///
|
|
/// This method is used to remove some states that have been
|
|
/// previously detected to be unreachable in order to "defragment"
|
|
/// the state vector. When a state is removed, all its outgoing
|
|
/// transition are removed as well. Removing reachable states
|
|
/// should NOT be attempted, because the incoming edges will be
|
|
/// 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.
|
|
///
|
|
/// \param used_states the number of states used (after
|
|
/// renumbering)
|
|
///
|
|
///@{
|
|
void defrag_states(const std::vector<unsigned>& newst, unsigned used_states)
|
|
{
|
|
SPOT_ASSERT(newst.size() >= states_.size());
|
|
SPOT_ASSERT(used_states > 0);
|
|
|
|
//std::cerr << "\nbefore defrag\n";
|
|
//dump_storage(std::cerr);
|
|
|
|
// Shift all states in states_, as indicated by newst.
|
|
unsigned send = states_.size();
|
|
for (state s = 0; 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]);
|
|
}
|
|
states_.resize(used_states);
|
|
|
|
// Shift all edges in edges_. The algorithm is
|
|
// similar to remove_if, but it also keeps the correspondence
|
|
// between the old and new index as newidx[old] = new.
|
|
unsigned tend = edges_.size();
|
|
std::vector<edge> newidx(tend);
|
|
unsigned dest = 1;
|
|
for (edge t = 1; t < tend; ++t)
|
|
{
|
|
if (is_dead_edge(t))
|
|
continue;
|
|
if (t != dest)
|
|
edges_[dest] = std::move(edges_[t]);
|
|
newidx[t] = dest;
|
|
++dest;
|
|
}
|
|
edges_.resize(dest);
|
|
killed_edge_ = 0;
|
|
|
|
// Adjust next_succ and dst pointers in all edges.
|
|
for (edge t = 1; t < dest; ++t)
|
|
{
|
|
auto& tr = edges_[t];
|
|
tr.src = newst[tr.src];
|
|
tr.dst = newst[tr.dst];
|
|
tr.next_succ = newidx[tr.next_succ];
|
|
}
|
|
|
|
// Adjust succ and succ_tails pointers in all states.
|
|
for (auto& s: states_)
|
|
{
|
|
s.succ = newidx[s.succ];
|
|
s.succ_tail = newidx[s.succ_tail];
|
|
}
|
|
|
|
//std::cerr << "\nafter defrag\n";
|
|
//dump_storage(std::cerr);
|
|
}
|
|
|
|
// prototype was changed in Spot 2.10
|
|
SPOT_DEPRECATED("use reference version of this method")
|
|
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
|
|
{
|
|
return defrag_states(newst, used_states);
|
|
}
|
|
///@}
|
|
};
|
|
}
|