Commit c5f8eafb authored by Guillaume Sadegh's avatar Guillaume Sadegh
Browse files

Add an algorithm to complement Büchi automata.

	* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New
	files. The complementation algorithm.
	* src/tgba/Makefile.am: Adjust.
	* src/tgbatest/complementation.test,
	src/tgbatest/complementation.cc: New files. Test suite for the
	complementation algorithm.
	* src/tgbatest/Makefile.am: Adjust.
	* src/tgbaalgos/Makefile.am: Reformat the header using 80
	columns.
parent e48338e8
2009-06-05 Guillaume Sadegh <sadegh@lrde.epita.fr>
Add an algorithm to complement Bchi automata.
* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New
files. The complementation algorithm.
* src/tgba/Makefile.am: Adjust.
* src/tgbatest/complementation.test,
src/tgbatest/complementation.cc: New files. Test suite for the
complementation algorithm.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbaalgos/Makefile.am: Reformat the header using 80
columns.
2009-06-05 Damien Lefortier <dam@lrde.epita.fr>
Modify the ELTL parser to be able to support PSL operators. Add a
......
## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
## dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
## et Marie Curie.
##
......@@ -41,6 +41,7 @@ tgba_HEADERS = \
tgbabddcoredata.hh \
tgbabddfactory.hh \
tgbascc.hh \
tgbacomplement.hh \
tgbaexplicit.hh \
tgbaproduct.hh \
tgbatba.hh \
......@@ -60,6 +61,7 @@ libtgba_la_SOURCES = \
tgbabddconcreteproduct.cc \
tgbabddcoredata.cc \
tgbascc.cc \
tgbacomplement.cc \
tgbaexplicit.cc \
tgbaproduct.cc \
tgbatba.cc \
......
// Copyright (C) 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <set>
#include <map>
#include <deque>
#include <cassert>
#include <sstream>
#include <boost/dynamic_bitset.hpp>
#include "bdd.h"
#include "misc/bddlt.hh"
#include "tgba/tgbatba.hh"
#include "tgba/bdddict.hh"
#include "tgba/state.hh"
#include "misc/hashfunc.hh"
#include "ltlast/formula.hh"
#include "ltlast/constant.hh"
#include "tgbaalgos/dotty.hh"
#include "tgba/tgbacomplement.hh"
namespace spot
{
typedef boost::dynamic_bitset<> bitset_t;
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;
};
} // anonymous.
/// \brief Automaton with Safra's tree as states.
struct safra_tree_automaton
{
safra_tree_automaton(const tgba* 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);
private:
mutable int max_nb_pairs_;
safra_tree* initial_state;
const tgba* a_;
};
namespace
{
/// \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();
const safra_tree& operator=(const safra_tree& other);
int compare(const safra_tree* other) const;
void add_node(const state* s);
int max_name() const;
// Operations to get successors of a tree.
safra_tree* branch_accepting(const tgba_sba_proxy& 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(bitset_t& bitset) const;
void getU(bitset_t& bitset) const;
/// \brief Does this node the root of the tree?
bool is_parent() const
{
return parent == 0;
}
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 = 0;
}
/// \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;
parent = 0;
nodes = other.nodes;
for (child_list::const_iterator i = other.children.begin();
i != other.children.end(); ++i)
{
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 (child_list::iterator i = children.begin(); i != children.end(); ++i)
delete *i;
for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
delete *i;
}
const safra_tree&
safra_tree::operator=(const safra_tree& other)
{
if (this != &other)
{
this->~safra_tree();
new (this) safra_tree(other);
}
return *this;
}
/// \brief Compare two safra trees.
///
/// \param other
///
/// \return 0 if the trees are the same. Otherwise
/// a signed value.
int safra_tree::compare(const safra_tree* other) const
{
int subset_compare = 0;
subset_t::const_iterator in1 = nodes.begin();
subset_t::const_iterator in2 = other->nodes.begin();
if (nodes.size() != other->nodes.size())
return (nodes.size() - other->nodes.size());
if (name != other->name)
return name - other->name;
for (; in1 != nodes.end() && in2 != other->nodes.end(); ++in1, ++in2)
if ((subset_compare = (*in1)->compare(*in2)) != 0)
break;
if (subset_compare != 0)
return subset_compare;
child_list::const_iterator ic1 = children.begin();
child_list::const_iterator ic2 = other->children.begin();
if (children.size() != other->children.size())
return (children.size() - other->children.size());
for (; ic1 != children.end() && ic2 != other->children.end();
++ic1, ++ic2)
{
int compare_value = (*ic1)->compare(*ic2);
if (compare_value != 0)
return compare_value;
}
if (marked != other->marked)
return (marked) ? -1 : 1;
return 0;
}
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 (child_list::const_iterator i = children.begin();
i != children.end(); ++i)
max_name = std::max(max_name, (*i)->max_name());
return max_name;
}
/// \brief Get an 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 == 0)
{
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 (child_list::const_iterator i = current->children.begin();
i != current->children.end(); ++i)
queue.push_back(*i);
}
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 tgba_sba_proxy& a)
{
for (child_list::iterator i = children.begin(); i != children.end(); ++i)
(*i)->branch_accepting(a);
subset_t subset;
for(subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
if (a.state_is_accepting(*i))
subset.insert(*i);
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 (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
{
if (cache_transition.find(*i) == cache_transition.end())
continue;
tr_cache_t transitions = cache_transition[*i];
for (tr_cache_t::const_iterator t_it = transitions.begin();
t_it != transitions.end();
++t_it)
{
if (((*t_it).first & condition) != bddfalse)
{
if (new_subset.find((*t_it).second) == new_subset.end())
{
const state* s = (*t_it).second->clone();
new_subset.insert(s);
}
}
}
}
nodes = new_subset;
for (child_list::iterator i = children.begin(); i != children.end(); ++i)
(*i)->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 (child_list::iterator child_it = children.begin();
child_it != children.end();
++child_it)
{
subset_t::iterator node_it = (*child_it)->nodes.begin();
while (node_it != (*child_it)->nodes.end())
{
if (node_set.find(*node_it) != node_set.end())
{
const state* s = *node_it;
(*child_it)->remove_node_from_children(*node_it);
(*child_it)->nodes.erase(node_it++);
delete s;
}
else
{
node_set.insert(*node_it);
++node_it;
}
}
(*child_it)->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 (child_list::iterator child_it = children.begin();
child_it != children.end();
++child_it)
{
subset_t::iterator it = (*child_it)->nodes.find(state);
if (it != (*child_it)->nodes.end())
{
const spot::state* s = *it;
(*child_it)->nodes.erase(it);
delete s;
}
(*child_it)->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 (child_list::const_iterator child_it = children.begin();
child_it != children.end();
++child_it)
{
node_set.insert((*child_it)->nodes.begin(), (*child_it)->nodes.end());
(*child_it)->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 (child_list::iterator i = children.begin();
i != children.end();
++i)
delete *i;
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.
/// \return bitset[i] will be true if this state-tree is included in L_i
void
safra_tree::getL(bitset_t& bitset) const
{
assert(bitset.size() > static_cast<unsigned>(name));
if (marked && !nodes.empty())
bitset[name] = true;
for (child_list::const_iterator i = children.begin();
i != children.end();
++i)
(*i)->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.
/// \return bitset[i] will be true if this state-tree is included in U_i
void
safra_tree::getU(bitset_t& bitset) const
{
assert(bitset.size() > static_cast<unsigned>(name));
if (!nodes.empty())
bitset[name] = false;
for (child_list::const_iterator i = children.begin();
i != children.end();
++i)
(*i)->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 tgba* 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, tgba_sba_proxy* sba,
</