Commit 6a662a6d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

get read of twa_safra_complement

* spot/twa/twasafracomplement.cc, spot/twa/twasafracomplement.hh,
tests/core/complementation.cc: Delete.
* tests/Makefile.am, spot/twa/Makefile.am: Adjust.
* tests/core/complementation.test: Rewrite using the new determinization
code.
* python/spot/impl.i: Do not mention twa_safra_complement anymore.
* NEWS: Mention the removal.
parent df0f9941
......@@ -68,6 +68,9 @@ New in spot 1.99.7a (not yet released)
in facts works on transition-based Büchi automaton, and will first
degeneralize any automaton with generalized Büchi acceptance.
* The twa_safra_complement class has been removed. Use
tgba_determinize() and dtwa_complement() instead.
Python:
* The ltsmin interface has been binded in Python. See
......
......@@ -61,7 +61,6 @@
%shared_ptr(spot::taa_tgba)
%shared_ptr(spot::taa_tgba_string)
%shared_ptr(spot::taa_tgba_formula)
%shared_ptr(spot::twa_safra_complement)
%shared_ptr(spot::twa_run)
%shared_ptr(spot::twa_word)
%shared_ptr(spot::emptiness_check_result)
......
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
## de Recherche et Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -34,8 +34,7 @@ twa_HEADERS = \
taatgba.hh \
twa.hh \
twagraph.hh \
twaproduct.hh \
twasafracomplement.hh
twaproduct.hh
noinst_LTLIBRARIES = libtwa.la
libtwa_la_SOURCES = \
......@@ -46,5 +45,4 @@ libtwa_la_SOURCES = \
taatgba.cc \
twa.cc \
twagraph.cc \
twaproduct.cc \
twasafracomplement.cc
twaproduct.cc
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
//
// 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/>.
#include <set>
#include <map>
#include <deque>
#include <cassert>
#include <sstream>
#include <algorithm>
#include <spot/misc/bitvect.hh>
#include <bddx.h>
#include <spot/misc/hash.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/twa.hh>
#include <spot/misc/hashfunc.hh>
#include <spot/tl/formula.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twa/twasafracomplement.hh>
#include <spot/twaalgos/degen.hh>
namespace spot
{
namespace
{
// forward decl.
struct safra_tree;
struct safra_tree_ptr_less_than:
public std::binary_function<const safra_tree*, const safra_tree*, bool>
{
bool
operator()(const safra_tree* left,
const safra_tree* right) const;
};
/// \brief Automaton with Safra's tree as states.
struct safra_tree_automaton
{
safra_tree_automaton(const const_twa_graph_ptr& sba);
~safra_tree_automaton();
typedef std::map<bdd, const safra_tree*, bdd_less_than> transition_list;
typedef
std::map<safra_tree*, transition_list, safra_tree_ptr_less_than>
automaton_t;
automaton_t automaton;
/// \brief The number of acceptance pairs of this Rabin (Streett)
/// automaton.
int get_nb_acceptance_pairs() const;
safra_tree* get_initial_state() const;
void set_initial_state(safra_tree* s);
const const_twa_graph_ptr& get_sba(void) const
{
return a_;
}
private:
mutable int max_nb_pairs_;
safra_tree* initial_state;
const_twa_graph_ptr a_;
};
/// \brief A Safra tree, used as state during the determinization
/// of a Büchi automaton
///
/// It is the key structure of the construction.
/// Each node of the tree has:
/// - A \a name,
/// - A subset of states of the original Büchi automaton (\a nodes),
/// - A flag that is \a marked to denote vertical merge of nodes,
/// - A list of \a children.
///
/// This class implements operations:
/// - To compute the successor of this tree,
/// - To retrive acceptance condition on this tree.
/// \see safra_determinisation.
struct safra_tree
{
typedef std::set<const state*, state_ptr_less_than> subset_t;
typedef std::list<safra_tree*> child_list;
typedef std::multimap<bdd, const state*, bdd_less_than> tr_cache_t;
typedef std::map<const state*, tr_cache_t,
state_ptr_less_than> cache_t;
safra_tree();
safra_tree(const safra_tree& other);
safra_tree(const subset_t& nodes, safra_tree* p, int n);
~safra_tree();
safra_tree& operator=(const safra_tree& other);
int compare(const safra_tree* other) const;
size_t hash() const;
void add_node(const state* s);
int max_name() const;
// Operations to get successors of a tree.
safra_tree* branch_accepting(const twa_graph& a);
safra_tree* succ_create(const bdd& condition,
cache_t& cache_transition);
safra_tree* normalize_siblings();
safra_tree* remove_empty();
safra_tree* mark();
// To get Rabin/Streett acceptance conditions.
void getL(bitvect& bitset) const;
void getU(bitvect& bitset) const;
/// \brief Is this node the root of the tree?
bool is_root() const
{
return parent == nullptr;
}
bool marked;
int name;
subset_t nodes;
child_list children;
private:
void remove_node_from_children(const state* state);
int get_new_name() const;
mutable std::deque<int> free_names_; // Some free names.
safra_tree* parent;
};
safra_tree::safra_tree()
: marked(false), name(0)
{
parent = nullptr;
}
/// \brief Copy the tree \a other, and set \c marked to false.
safra_tree::safra_tree(const safra_tree& other)
: marked(false), name(other.name), nodes(other.nodes)
{
parent = nullptr;
for (auto i: other.children)
{
safra_tree* c = new safra_tree(*i);
c->parent = this;
children.push_back(c);
}
}
safra_tree::safra_tree(const subset_t& nodes, safra_tree* p, int n)
: marked(false), name(n), nodes(nodes)
{
parent = p;
}
safra_tree::~safra_tree()
{
for (auto c: children)
delete c;
for (auto n: nodes)
n->destroy();
}
/// \brief Compare two safra trees.
///
/// \param other the tree to compare too.
///
/// \return 0 if the trees are the same. Otherwise
/// a signed value.
int safra_tree::compare(const safra_tree* other) const
{
int res = name - other->name;
if (res != 0)
return res;
if (marked != other->marked)
return (marked) ? -1 : 1;
res = nodes.size() - other->nodes.size();
if (res != 0)
return res;
res = children.size() - other->children.size();
if (res != 0)
return res;
// Call compare() only as a last resort, because it takes time.
subset_t::const_iterator in1 = nodes.begin();
subset_t::const_iterator in2 = other->nodes.begin();
for (; in1 != nodes.end(); ++in1, ++in2)
if ((res = (*in1)->compare(*in2)) != 0)
return res;
child_list::const_iterator ic1 = children.begin();
child_list::const_iterator ic2 = other->children.begin();
for (; ic1 != children.end(); ++ic1, ++ic2)
if ((res = (*ic1)->compare(*ic2)) != 0)
return res;
return 0;
}
/// \brief Hash a safra tree.
size_t
safra_tree::hash() const
{
size_t hash = 0;
hash ^= wang32_hash(name);
hash ^= wang32_hash(marked);
for (auto n: nodes)
hash ^= n->hash();
for (auto c: children)
hash ^= c->hash();
return hash;
}
void
safra_tree::add_node(const state* s)
{
nodes.insert(s);
}
/*---------------------------------.
| Operations to compute successors |
`---------------------------------*/
int
safra_tree::max_name() const
{
int max_name = name;
for (auto c: children)
max_name = std::max(max_name, c->max_name());
return max_name;
}
/// \brief Get a unused name in the tree for a new node.
///
/// The root of the tree maintains a list of unused names.
/// When this list is empty, new names are computed.
int
safra_tree::get_new_name() const
{
if (parent == nullptr)
{
if (free_names_.empty())
{
std::set<int> used_names;
std::deque<const safra_tree*> queue;
queue.push_back(this);
while (!queue.empty())
{
const safra_tree* current = queue.front();
queue.pop_front();
used_names.insert(current->name);
for (auto c: current->children)
queue.push_back(c);
}
int l = 0;
int nb_found = 0;
std::set<int>::const_iterator i = used_names.begin();
while (i != used_names.end() && nb_found != 3)
{
if (l != *i)
{
free_names_.push_back(l);
++nb_found;
}
else
++i;
++l;
}
while (nb_found++ < 3)
free_names_.push_back(l++);
}
int result = free_names_.front();
free_names_.pop_front();
return result;
}
else
return parent->get_new_name();
}
/// If the node has an accepting state in its label, a new child
/// is inserted with the set of all accepting states of \c nodes
/// as label and an unused name.
safra_tree*
safra_tree::branch_accepting(const twa_graph& a)
{
for (auto c: children)
c->branch_accepting(a);
subset_t subset;
for (auto n: nodes)
if (a.state_is_accepting(n))
subset.insert(n);
if (!subset.empty())
children.push_back(new safra_tree(subset, this, get_new_name()));
return this;
}
/// \brief A powerset construction.
///
/// The successors of each state in \c nodes with \a condition
/// as atomic property remplace the current \c nodes set.
///
/// @param cache_transition is a map of the form: state -> bdd -> state.
/// Only states present in \c nodes are keys of the map.
/// @param condition is an atomic property. We are looking for successors
/// of this atomic property.
safra_tree*
safra_tree::succ_create(const bdd& condition,
cache_t& cache_transition)
{
subset_t new_subset;
for (auto n: nodes)
{
cache_t::const_iterator it = cache_transition.find(n);
if (it == cache_transition.end())
continue;
const tr_cache_t& transitions = it->second;
for (auto t: transitions)
{
if ((t.first & condition) != bddfalse)
{
if (new_subset.find(t.second) == new_subset.end())
{
const state* s = t.second->clone();
new_subset.insert(s);
}
}
}
}
std::swap(nodes, new_subset);
for (auto c: children)
c->succ_create(condition, cache_transition);
return this;
}
/// \brief Horizontal Merge
///
/// If many children share the same state in their labels, we must keep
/// only one occurrence (in the older node).
safra_tree*
safra_tree::normalize_siblings()
{
std::set<const state*, state_ptr_less_than> node_set;
for (auto c: children)
{
subset_t::iterator node_it = c->nodes.begin();
while (node_it != c->nodes.end())
{
if (!node_set.insert(*node_it).second)
{
const state* s = *node_it;
c->remove_node_from_children(*node_it);
c->nodes.erase(node_it++);
s->destroy();
}
else
{
++node_it;
}
}
c->normalize_siblings();
}
return this;
}
/// \brief Remove recursively all the occurrences of \c state in the label.
void
safra_tree::remove_node_from_children(const state* state)
{
for (auto c: children)
{
subset_t::iterator it = c->nodes.find(state);
if (it != c->nodes.end())
{
const spot::state* s = *it;
c->nodes.erase(it);
s->destroy();
}
c->remove_node_from_children(state);
}
}
/// \brief Remove empty nodes
///
/// If a child of the node has an empty label, we remove this child.
safra_tree*
safra_tree::remove_empty()
{
child_list::iterator child_it = children.begin();
while (child_it != children.end())
{
if ((*child_it)->nodes.empty())
{
safra_tree* to_delete = *child_it;
child_it = children.erase(child_it);
delete to_delete;
}
else
{
(*child_it)->remove_empty();
++child_it;
}
}
return this;
}
/// \brief Vertical merge
///
/// If a parent has the same states as its childen in its label,
/// All the children a deleted and the node is marked. This mean
/// an accepting infinite run is found.
safra_tree*
safra_tree::mark()
{
std::set<const state*, state_ptr_less_than> node_set;
for (auto c: children)
{
node_set.insert(c->nodes.begin(), c->nodes.end());
c->mark();
}
char same = node_set.size() == nodes.size();
if (same)
{
subset_t::const_iterator i = node_set.begin();
subset_t::const_iterator j = nodes.begin();
while (i != node_set.end() && j != nodes.end())
{
if ((*i)->compare(*j) != 0)
{
same = 0;
break;
}
++i;
++j;
}
}
if (same)
{
marked = true;
for (auto c: children)
delete c;
children = child_list();
}
return this;
}
/*-----------------------.
| Acceptances conditions |
`-----------------------*/
/// Returns in which sets L (the semantic differs according to Rabin or
/// Streett) the state-tree is included.
///
/// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
/// filled with FALSE bits.
/// On return bitset[i] will be set if this state-tree is included in L_i.
void
safra_tree::getL(bitvect& bitset) const
{
assert(bitset.size() > static_cast<unsigned>(name));
if (marked && !nodes.empty())
bitset.set(name);
for (auto c: children)
c->getL(bitset);
}
/// Returns in which sets U (the semantic differs according to Rabin or
/// Streett) the state-tree is included.
///
/// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
/// filled with TRUE bits.
/// On return bitset[i] will be set if this state-tree is included in U_i.
void
safra_tree::getU(bitvect& bitset) const
{
assert(bitset.size() > static_cast<unsigned>(name));
if (!nodes.empty())
bitset.clear(name);
for (auto c: children)
c->getU(bitset);
}
bool
safra_tree_ptr_less_than::operator()(const safra_tree* left,
const safra_tree* right) const
{
assert(left);
return left->compare(right) < 0;
}
struct safra_tree_ptr_equal:
public std::unary_function<const safra_tree*, bool>
{
safra_tree_ptr_equal(const safra_tree* left)
: left_(left) {}
bool
operator()(const safra_tree* right) const
{
return left_->compare(right) == 0;
}
private:
const safra_tree* left_;
};
/// \brief Algorithm to determinize Büchi automaton.
///
/// Determinization of a Büchi automaton into a Rabin automaton
/// using the Safra's construction.
///
/// This construction is presented in:
/// @PhDThesis{ safra.89.phd,
/// author = {Shmuel Safra},
/// title = {Complexity of Automata on Infinite Objects},
/// school = {The Weizmann Institute of Science},
/// year = {1989},
/// address = {Rehovot, Israel},
/// month = mar
/// }
///
class safra_determinisation
{
public:
static safra_tree_automaton*
create_safra_automaton(const const_twa_graph_ptr& a);
private:
typedef std::set<int> atomic_list_t;
typedef std::set<bdd, bdd_less_than> conjunction_list_t;
static void retrieve_atomics(const safra_tree* node,
twa_graph_ptr sba_aut,
safra_tree::cache_t& cache,
atomic_list_t& atomic_list);
static void set_atomic_list(atomic_list_t& list, bdd condition);
static conjunction_list_t
get_conj_list(const atomic_list_t& atomics);
};
/// \brief The body of Safra's construction.
safra_tree_automaton*
safra_determinisation::create_safra_automaton
(const const_twa_graph_ptr& a)
{
// initialization.
auto sba_aut = degeneralize(a);
safra_tree_automaton* st = new safra_tree_automaton(sba_aut