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

Add a new type of automata: State-labeled Alternating Büchi

Browse source 
Automata (SABA).

* src/saba/saba.hh, src/saba/saba.cc, src/saba/sabastate.hh,
src/saba/sabasucciter.hh: New.  Interface for
SABA (State-labeled Alternating Büchi Automata).
* src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh: New.  Default
implementation for a conjunction of states.
* src/saba/Makefile.am: New.
* src/Makefile.am, configure.ac: Adjust.
* src/sabaalgos/sabareachiter.cc,
src/sabaalgos/sabareachiter.hh: New.  Iterate over all reachable
states of a spot::saba.
* src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh: New.
Print reachable states in dot format.
* src/sabaalgos/Makefile.am: New.
This commit is contained in:
Guillaume Sadegh 2009-11-30 23:22:13 +01:00
parent f00aa49dc3
commit 7cb6ff331d
15 changed files with 1331 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/saba/Makefile.am Normal file
View file

@ -0,0 +1,38 @@
## 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.
AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
sabadir = $(pkgincludedir)/saba
saba_HEADERS = \
explicitstateconjunction.hh \
saba.hh \
sabastate.hh \
sabasucciter.hh \
sabacomplementtgba.hh
noinst_LTLIBRARIES = libsaba.la
libsaba_la_SOURCES = \
explicitstateconjunction.cc \
saba.cc \
sabacomplementtgba.cc

91
src/saba/explicitstateconjunction.cc Normal file
View file

@ -0,0 +1,91 @@
// 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 "explicitstateconjunction.hh"
namespace spot
{
/// explicit_state_conjunction
////////////////////////////////////////
explicit_state_conjunction::explicit_state_conjunction()
{
}
explicit_state_conjunction::
explicit_state_conjunction(const explicit_state_conjunction* other)
: set_(other->set_)
{
}
explicit_state_conjunction*
explicit_state_conjunction::operator=(const explicit_state_conjunction& o)
{
if (this != &o)
{
this->~explicit_state_conjunction();
new (this) explicit_state_conjunction(&o);
}
return this;
}
explicit_state_conjunction::~explicit_state_conjunction()
{
}
void
explicit_state_conjunction::first()
{
it_ = set_.begin();
}
void
explicit_state_conjunction::next()
{
++it_;
}
bool
explicit_state_conjunction::done() const
{
return it_ == set_.end();
}
explicit_state_conjunction*
explicit_state_conjunction::clone() const
{
return new explicit_state_conjunction(this);
}
saba_state*
explicit_state_conjunction::current_state() const
{
return (*it_)->clone();
}
void
explicit_state_conjunction::add(saba_state* state)
{
set_.insert(shared_saba_state(state));
}
} // end namespace spot.

79
src/saba/explicitstateconjunction.hh Normal file
View file

@ -0,0 +1,79 @@
// 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.
#ifndef SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
# define SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
#include <misc/hash.hh>
#include "sabasucciter.hh"
namespace spot
{
/// \brief Basic implementation of saba_state_conjunction.
/// \ingroup saba_essentials
///
/// This class provides a basic implementation to
/// iterate over a conjunction of states of a saba.
class explicit_state_conjunction : public saba_state_conjunction
{
public:
explicit_state_conjunction();
explicit_state_conjunction(const explicit_state_conjunction* other);
virtual ~explicit_state_conjunction();
explicit_state_conjunction* operator=(const explicit_state_conjunction& o);
/// \name Iteration
//@{
virtual void first();
virtual void next();
virtual bool done() const;
//@}
/// \name Inspection
//@{
/// Duplicate a this conjunction.
explicit_state_conjunction* clone() const;
/// Return the a new instance on the current state.
/// This is the caller responsibility to delete the returned state.
virtual saba_state* current_state() const;
//@}
/// Add a new state in the conjunction.
/// The class becomes owner of \a state.
void add(saba_state* state);
private:
typedef Sgi::hash_set<shared_saba_state,
spot::saba_state_shared_ptr_hash,
spot::saba_state_shared_ptr_equal> saba_state_set_t;
saba_state_set_t set_;
saba_state_set_t::iterator it_;
};
} // end namespace spot.
#endif // SPOT_SABA_EXPLICITSTATECONJUNCTION_HH

52
src/saba/saba.cc Normal file
View file

@ -0,0 +1,52 @@
// 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 "saba.hh"
namespace spot
{
saba::saba()
: num_acc_(-1)
{
}
saba::~saba()
{
}
unsigned int
saba::number_of_acceptance_conditions() const
{
if (num_acc_ < 0)
{
bdd all = all_acceptance_conditions();
unsigned int n = 0;
while (all != bddfalse)
{
++n;
all -= bdd_satone(all);
}
num_acc_ = n;
}
return num_acc_;
}
} // end namespace spot.

117
src/saba/saba.hh Normal file
View file

@ -0,0 +1,117 @@
// 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.
#ifndef SPOT_SABA_SABA_HH
# define SPOT_SABA_SABA_HH
#include "sabastate.hh"
#include "sabasucciter.hh"
#include <tgba/bdddict.hh>
namespace spot
{
/// \defgroup saba SABA (State-based Alternating Büchi Automata)
///
/// Spot was centered around non-deterministic \ref tgba.
/// Alternating automata are an extension to non-deterministic
/// automata, and are presented with spot::saba.
/// This type and its cousins are listed \ref saba_essentials "here".
/// This is an abstract interface.
/// \addtogroup saba_essentials Essential SABA types
/// \ingroup saba
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
/// \ingroup saba_essentials
///
/// Browsing such automaton can be achieved using two functions:
/// \c get_init_state, and \c succ_iter. The former returns
/// the initial state while the latter lists the
/// successor states of any state.
///
/// Note that although this is a transition-based automata,
/// we never represent transitions! Transition informations are
/// obtained by querying the iterator over the successors of
/// a state.
class saba
{
protected:
saba();
public:
virtual ~saba();
/// \brief Get the initial state of the automaton.
///
/// The state has been allocated with \c new. It is the
/// responsability of the caller to \c delete it when no
/// longer needed.
virtual saba_state* get_init_state() const = 0;
/// \brief Get an iterator over the successors of \a local_state.
///
/// The iterator has been allocated with \c new. It is the
/// responsability of the caller to \c delete it when no
/// longer needed.
///
/// \param local_state The state whose successors are to be explored.
/// This pointer is not adopted in any way by \c succ_iter, and
/// it is still the caller's responsability to delete it when
/// appropriate (this can be done during the lifetime of
/// the iterator).
virtual saba_succ_iterator*
succ_iter(const saba_state* local_state) const = 0;
/// \brief Get the dictionary associated to the automaton.
///
/// State are represented as BDDs. The dictionary allows
/// to map BDD variables back to formulae, and vice versa.
/// This is useful when dealing with several automata (which
/// may use the same BDD variable for different formula),
/// or simply when printing.
virtual bdd_dict* get_dict() const = 0;
/// \brief Format the state as a string for printing.
///
/// This formating is the responsability of the automata
/// that owns the state.
virtual std::string format_state(const saba_state* state) const = 0;
/// \brief Return the set of all acceptance conditions used
/// by this automaton.
///
/// The goal of the emptiness check is to ensure that
/// a strongly connected component walks through each
/// of these acceptiong conditions. I.e., the union
/// of the acceptiong conditions of all transition in
/// the SCC should be equal to the result of this function.
virtual bdd all_acceptance_conditions() const = 0;
/// The number of acceptance conditions.
virtual unsigned int number_of_acceptance_conditions() const;
private:
mutable int num_acc_;
};
} // end namespace spot.
#endif // SPOT_SABA_SABA_HH

246
src/saba/sabastate.hh Normal file
View file

@ -0,0 +1,246 @@
// 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.
#ifndef SPOT_SABA_SABASTATE_HH
# define SPOT_SABA_SABASTATE_HH
#include <bdd.h>
#include <functional>
#include <boost/shared_ptr.hpp>
namespace spot
{
/// \brief Abstract class for saba states.
/// \ingroup saba_essentials
class saba_state
{
public:
/// \brief Compares two states (that come from the same automaton).
///
/// This method returns an integer less than, equal to, or greater
/// than zero if \a this is found, respectively, to be less than, equal
/// to, or greater than \a other according to some implicit total order.
///
/// This method should not be called to compare states from
/// different automata.
///
/// \sa spot::saba_state_ptr_less_than
virtual int compare(const saba_state* other) const = 0;
/// \brief Hash a state.
///
/// This method returns an integer that can be used as a
/// hash value for this state.
///
/// Note that the hash value is guaranteed to be unique for all
/// equal states (in compare()'s sense) for only has long has one
/// of these states exists. So it's OK to use a spot::saba_state as a
/// key in a \c hash_map because the mere use of the state as a
/// key in the hash will ensure the state continues to exist.
///
/// However if you create the state, get its hash key, delete the
/// state, recreate the same state, and get its hash key, you may
/// obtain two different hash keys if the same state were not
/// already used elsewhere. In practice this weird situation can
/// occur only when the state is BDD-encoded, because BDD numbers
/// (used to build the hash value) can be reused for other
/// formulas. That probably doesn't matter, since the hash value
/// is meant to be used in a \c hash_map, but it had to be noted.
virtual size_t hash() const = 0;
/// Duplicate a state.
virtual saba_state* clone() const = 0;
/// \brief Get the acceptance condition.
///
/// saba are state-labeled automata, then their acceptance conditions
/// are labeled on states.
virtual bdd acceptance_conditions() const = 0;
virtual ~saba_state()
{
}
};
/// \brief Strict Weak Ordering for \c saba_state*.
/// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c saba_state*.
///
/// For instance here is how one could declare
/// a map of \c saba_state*.
/// \code
/// // Remember how many times each state has been visited.
/// std::map<spot::saba_state*, int, spot::saba_state_ptr_less_than> seen;
/// \endcode
struct saba_state_ptr_less_than:
public std::binary_function<const saba_state*, const saba_state*, bool>
{
bool
operator()(const saba_state* left, const saba_state* right) const
{
assert(left);
return left->compare(right) < 0;
}
};
/// \brief An Equivalence Relation for \c saba_state*.
/// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c saba_state*.
///
/// For instance here is how one could declare
/// a map of \c saba_state*.
/// \code
/// // Remember how many times each state has been visited.
/// Sgi::hash_map<spot::saba_state*, int, spot::saba_state_ptr_hash,
/// spot::saba_state_ptr_equal> seen;
/// \endcode
struct saba_state_ptr_equal:
public std::binary_function<const saba_state*, const saba_state*, bool>
{
bool
operator()(const saba_state* left, const saba_state* right) const
{
assert(left);
return 0 == left->compare(right);
}
};
/// \brief Hash Function for \c saba_state*.
/// \ingroup saba_essentials
/// \ingroup hash_funcs
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type \c saba_state*.
///
/// For instance here is how one could declare
/// a map of \c saba_state*.
/// \code
/// // Remember how many times each state has been visited.
/// Sgi::hash_map<spot::saba_state*, int, spot::saba_state_ptr_hash,
/// spot::saba_state_ptr_equal> seen;
/// \endcode
struct saba_state_ptr_hash:
public std::unary_function<const saba_state*, size_t>
{
size_t
operator()(const saba_state* that) const
{
assert(that);
return that->hash();
}
};
// Functions related to shared_ptr.
//////////////////////////////////////////////////
typedef boost::shared_ptr<const saba_state> shared_saba_state;
/// \brief Strict Weak Ordering for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
/// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c shared_saba_state.
///
/// For instance here is how one could declare
/// a map of \c shared_saba_state.
/// \code
/// // Remember how many times each state has been visited.
/// std::map<shared_saba_state, int, spot::saba_state_shared_ptr_less_than>
/// seen;
/// \endcode
struct saba_state_shared_ptr_less_than:
public std::binary_function<shared_saba_state,
shared_saba_state, bool>
{
bool
operator()(shared_saba_state left,
shared_saba_state right) const
{
assert(left);
return left->compare(right.get()) < 0;
}
};
/// \brief An Equivalence Relation for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
/// \ingroup saba_essentials
///
/// This is meant to be used as a comparison functor for
/// Sgi \c hash_map whose key are of type \c shared_saba_state.
///
/// For instance here is how one could declare
/// a map of \c shared_saba_state
/// \code
/// // Remember how many times each state has been visited.
/// Sgi::hash_map<shared_saba_state, int,
/// spot::saba_state_shared_ptr_hash,
/// spot::saba_state_shared_ptr_equal> seen;
/// \endcode
struct saba_state_shared_ptr_equal:
public std::binary_function<shared_saba_state,
shared_saba_state, bool>
{
bool
operator()(shared_saba_state left,
shared_saba_state right) const
{
assert(left);
return 0 == left->compare(right.get());
}
};
/// \brief Hash Function for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
/// \ingroup saba_essentials
/// \ingroup hash_funcs
///
/// This is meant to be used as a hash functor for
/// Sgi's \c hash_map whose key are of type
/// \c shared_saba_state.
///
/// For instance here is how one could declare
/// a map of \c shared_saba_state.
/// \code
/// // Remember how many times each state has been visited.
/// Sgi::hash_map<shared_saba_state, int,
/// spot::saba_state_shared_ptr_hash,
/// spot::saba_state_shared_ptr_equal> seen;
/// \endcode
struct saba_state_shared_ptr_hash:
public std::unary_function<shared_saba_state, size_t>
{
size_t
operator()(shared_saba_state that) const
{
assert(that);
return that->hash();
}
};
}
#endif // SPOT_SABA_SABASTATE_HH

160
src/saba/sabasucciter.hh Normal file
View file

@ -0,0 +1,160 @@
// 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.
#ifndef SPOT_SABA_SABASUCCITER_HH
# define SPOT_SABA_SABASUCCITER_HH
#include "sabastate.hh"
namespace spot
{
/// \brief Iterate over a conjunction of saba_state.
/// \ingroup saba_essentials
///
/// This class provides the basic functionalities required to
/// iterate over a conjunction of states of a saba.
class saba_state_conjunction
{
public:
virtual
~saba_state_conjunction()
{
}
/// \name Iteration
//@{
/// \brief Position the iterator on the first successor of the conjunction
/// (if any).
///
/// This method can be called several times to make multiple
/// passes over successors.
///
/// \warning One should always call \c done() to
/// ensure there is a successor, even after \c first(). A
/// common trap is to assume that there is at least one
/// successor: this is wrong.
virtual void first() = 0;
/// \brief Jump to the next successor (if any).
///
/// \warning Again, one should always call \c done() to ensure
/// there is a successor.
virtual void next() = 0;
/// \brief Check whether the iteration over a conjunction of states
/// is finished.
///
/// This function should be called after any call to \c first()
/// or \c next() and before any enquiry about the current state.
virtual bool done() const = 0;
//@}
/// \name Inspection
//@{
/// \brief Get the state of the current successor.
///
/// Note that the same state may occur at different points
/// in the iteration. These actually correspond to the same
/// destination. It just means there were several transitions,
/// with different conditions, leading to the same state.
///
/// \warning the state is allocated with new, its deletion is
/// the responsibility of the caller.
virtual saba_state* current_state() const = 0;
//@}
/// Duplicate a saba_state conjunction.
virtual saba_state_conjunction* clone() const = 0;
};
/// \brief Iterate over the successors of a saba_state.
/// \ingroup saba_essentials
///
/// This class provides the basic functionalities required to
/// iterate over the successors of a state of a saba. Since
/// transitions of an alternating automaton are defined as a
/// boolean function with conjunctions (universal) and
/// disjunctions (non-deterministic),
class saba_succ_iterator
{
public:
virtual
~saba_succ_iterator()
{
}
/// \name Iteration
//@{
/// \brief Position the iterator on the first conjunction
/// of successors (if any).
///
/// This method can be called several times to make multiple
/// passes over successors.
///
/// \warning One should always call \c done() to
/// ensure there is a successor, even after \c first(). A
/// common trap is to assume that there is at least one
/// successor: this is wrong.
virtual void first() = 0;
/// \brief Jump to the next conjunction of successors (if any).
///
/// \warning Again, one should always call \c done() to ensure
/// there is a successor.
virtual void next() = 0;
/// \brief Check whether the iteration is finished.
///
/// This function should be called after any call to \c first()
/// or \c next() and before any enquiry about the current state.
///
/// The usual way to do this is with a \c for loop.
/// \code
/// for (s->first(); !s->done(); s->next())
/// ...
/// \endcode
virtual bool done() const = 0;
//@}
/// \name Inspection
//@{
/// \brief Get current conjunction of successor states.
virtual saba_state_conjunction* current_conjunction() const = 0;
/// \brief Get the condition on the transition leading to this successor.
///
/// This is a boolean function of atomic propositions.
virtual bdd current_condition() const = 0;
//@}
};
}
#endif // SPOT_TGBA_SUCCITER_HH