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

Remove support for state-based alternating automata.

Browse source 
This was never actually used and we have a new implementation of
alternating automata coming.

* src/saba/, src/sabaalgos/, src/sabatest/: Remove.
* src/Makefile.am, configure.ac, README: Adjust.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2014-10-06 10:31:53 +02:00
parent 2c764fb3c7
commit 51fe5108fe
22 changed files with 6 additions and 2028 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -119,6 +119,9 @@ New in spot 1.99a (not yet released)
has been removed too, because it was only used by the KV
complementation.
- The unused implementation of state-based alternating Büchi automata
has been removed.
New in spot 1.2.5a (not yet released)
* New features:

3
README
View file

@ -166,9 +166,6 @@ src/ Sources for libspot.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/.
saba/ SABA (State-labeled Alternating Büchi Automata) objects.
sabaalgos/ Algorithms on SABA.
sabatest/ Tests for saba/, sabaalgos/.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
org/ Source of userdoc/ as org-mode files.

4
configure.ac
View file

@ -193,10 +193,6 @@ AC_CONFIG_FILES([
src/neverparse/Makefile
src/priv/Makefile
src/sanity/Makefile
src/saba/Makefile
src/sabaalgos/Makefile
src/sabatest/defs
src/sabatest/Makefile
src/tgbaalgos/gtec/Makefile
src/tgbaalgos/Makefile
src/tgba/Makefile

8
src/Makefile.am
View file

@ -26,9 +26,9 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \
tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
neverparse kripkeparse dstarparse . bin ltltest graphtest \
tgbatest sabatest kripketest sanity
tgbaalgos tgbaparse ta taalgos kripke neverparse \
kripkeparse dstarparse . bin ltltest graphtest tgbatest \
kripketest sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
@ -44,8 +44,6 @@ libspot_la_LIBADD = \
misc/libmisc.la \
neverparse/libneverparse.la \
priv/libpriv.la \
sabaalgos/libsabaalgos.la \
saba/libsaba.la \
taalgos/libtaalgos.la \
ta/libta.la \
tgbaalgos/libtgbaalgos.la \

36
src/saba/Makefile.am
View file

@ -1,36 +0,0 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2011, 2013 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/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(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

89
src/saba/explicitstateconjunction.cc
View file

@ -1,89 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 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 "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.

78
src/saba/explicitstateconjunction.hh
View file

@ -1,78 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013 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/>.
#ifndef SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
# define SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
#include "misc/common.hh"
#include "misc/hash.hh"
#include "sabasucciter.hh"
namespace spot
{
/// \ingroup saba_essentials
/// \brief Basic implementation of saba_state_conjunction.
///
/// This class provides a basic implementation to
/// iterate over a conjunction of states of a saba.
class SPOT_API 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 std::unordered_set<shared_saba_state,
saba_state_shared_ptr_hash,
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

49
src/saba/saba.cc
View file

@ -1,49 +0,0 @@
// Copyright (C) 2009 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 "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.

118
src/saba/saba.hh
View file

@ -1,118 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013, 2014 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/>.
#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
/// \ingroup saba_essentials
/// \brief A State-based Alternating (Generalized) Büchi Automaton.
///
/// 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 SPOT_API 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_ptr 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_;
};
typedef std::shared_ptr<saba> saba_ptr;
typedef std::shared_ptr<const saba> const_saba_ptr;
} // end namespace spot.
#endif // SPOT_SABA_SABA_HH

445
src/saba/sabacomplementtgba.cc
View file

@ -1,445 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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 <vector>
#include <cassert>
#include <sstream>
#include "bdd.h"
#include "tgba/bddprint.hh"
#include "tgba/tgba.hh"
#include "misc/hash.hh"
#include "misc/bddlt.hh"
#include "tgbaalgos/degen.hh"
#include "tgbaalgos/bfssteps.hh"
#include "misc/hashfunc.hh"
#include "ltlast/formula.hh"
#include "ltlast/constant.hh"
#include "priv/countstates.hh"
#include "sabacomplementtgba.hh"
#include "explicitstateconjunction.hh"
namespace spot
{
namespace
{
// typedefs.
typedef int rank_t;
////////////////////////////////////////
// saba_state_complement_tgba
/// States used by spot::saba_complement_tgba.
/// A state gather a spot::state* and a rank.
/// \ingroup saba_representation
class saba_state_complement_tgba : public saba_state
{
public:
saba_state_complement_tgba();
saba_state_complement_tgba(const saba_state_complement_tgba* state_taa);
saba_state_complement_tgba(shared_state state, rank_t rank,
bdd condition);
virtual ~saba_state_complement_tgba() {}
virtual int compare(const saba_state* other) const;
virtual size_t hash() const;
virtual saba_state_complement_tgba* clone() const;
virtual bdd acceptance_conditions() const;
const state* get_state() const;
rank_t get_rank() const;
private:
shared_state state_;
rank_t rank_;
bdd condition_;
};
saba_state_complement_tgba::saba_state_complement_tgba(shared_state state,
rank_t rank,
bdd condition)
: state_(state), rank_(rank), condition_(condition)
{
}
saba_state_complement_tgba::
saba_state_complement_tgba(const saba_state_complement_tgba* state_taa)
: state_(state_taa->state_), rank_(state_taa->rank_),
condition_(state_taa->condition_)
{
}
int
saba_state_complement_tgba::compare(const saba_state* o) const
{
const saba_state_complement_tgba* other =
dynamic_cast<const saba_state_complement_tgba*>(o);
int compare_value = get_state()->compare(other->get_state());
if (compare_value != 0)
return compare_value;
if (get_rank() != other->get_rank())
return get_rank() - other->get_rank();
return acceptance_conditions().id() -
other->acceptance_conditions().id();
}
size_t
saba_state_complement_tgba::hash() const
{
size_t hash = get_state()->hash() ^ wang32_hash(get_rank());
hash ^= wang32_hash(acceptance_conditions().id());
return hash;
}
saba_state_complement_tgba*
saba_state_complement_tgba::clone() const
{
return new saba_state_complement_tgba(*this);
}
bdd
saba_state_complement_tgba::acceptance_conditions() const
{
if ((get_rank() & 1) == 1)
return condition_;
else
return bddfalse;
}
const state*
saba_state_complement_tgba::get_state() const
{
return state_.get();
}
rank_t
saba_state_complement_tgba::get_rank() const
{
return rank_;
}
/// Successor iterators used by spot::saba_complement_tgba.
/// \ingroup saba_representation
///
/// Since the algorithm works on-the-fly, the key components of the
/// algorithm are implemented in this class.
///
class saba_complement_tgba_succ_iterator: public saba_succ_iterator
{
public:
typedef std::list<saba_state_conjunction*> state_conjunction_list_t;
typedef std::map<bdd, state_conjunction_list_t, bdd_less_than>
bdd_list_t;
saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr&
automaton,
bdd the_acceptance_cond,
const saba_state_complement_tgba*
origin);
virtual ~saba_complement_tgba_succ_iterator();
virtual void first();
virtual void next();
virtual bool done() const;
virtual saba_state_conjunction* current_conjunction() const;
virtual bdd current_condition() const;
private:
void get_atomics(std::set<int>& list, bdd c);
void get_conj_list();
void state_conjunction();
void delete_condition_list();
const_tgba_digraph_ptr automaton_;
bdd the_acceptance_cond_;
const saba_state_complement_tgba* origin_;
bdd_list_t condition_list_;
bdd_list_t::const_iterator current_condition_;
state_conjunction_list_t::const_iterator current_conjunction_;
state_conjunction_list_t::const_iterator current_end_conjunction_;
};
saba_complement_tgba_succ_iterator::
saba_complement_tgba_succ_iterator(const const_tgba_digraph_ptr& automaton,
bdd the_acceptance_cond,
const saba_state_complement_tgba* origin)
: automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
origin_(origin)
{
assert(automaton->is_sba());
// If state not accepting or rank is even
if (((origin_->get_rank() & 1) == 0) ||
!automaton_->state_is_accepting(origin_->get_state()))
{
get_conj_list();
state_conjunction();
}
}
saba_complement_tgba_succ_iterator::
~saba_complement_tgba_succ_iterator()
{
delete_condition_list();
}
void
saba_complement_tgba_succ_iterator::state_conjunction()
{
int max_rank = origin_->get_rank();
for (bdd_list_t::iterator it = condition_list_.begin();
it != condition_list_.end();
++it)
{
// Get successors states.
bdd condition = it->first;
std::vector<shared_state> state_list;
for (auto iterator: automaton_->succ(origin_->get_state()))
{
bdd c = iterator->current_condition();
if ((c & condition) != bddfalse)
state_list.push_back(shared_state(iterator->current_state(),
shared_state_deleter));
}
// Make the conjunction with ranks.
std::vector<int> current_ranks(state_list.size(), max_rank);
if (state_list.empty())
return;
do
{
explicit_state_conjunction* conj = new explicit_state_conjunction();
for (unsigned i = 0; i < state_list.size(); ++i)
{
conj->add(new saba_state_complement_tgba(state_list[i],
current_ranks[i],
the_acceptance_cond_));
}
it->second.push_back(conj);
if (current_ranks[0] <= 0)
break;
unsigned order = state_list.size() - 1;
while (current_ranks[order] == 0)
{
current_ranks[order] = max_rank;
--order;
}
--current_ranks[order];
}
while (1);
}
}
/// Insert in \a list atomic properties of the formula \a c.
void
saba_complement_tgba_succ_iterator::get_atomics(std::set<int>& list, bdd c)
{
bdd current = bdd_satone(c);
while (current != bddtrue && current != bddfalse)
{
list.insert(bdd_var(current));
bdd high = bdd_high(current);
if (high == bddfalse)
current = bdd_low(current);
else
current = high;
}
}
/// Free the conjunctions in the condition map.
void
saba_complement_tgba_succ_iterator::delete_condition_list()
{
for (bdd_list_t::iterator i = condition_list_.begin();
i != condition_list_.end();
++i)
{
for (state_conjunction_list_t::iterator j = i->second.begin();
j != i->second.end();
++j)
delete *j;
}
condition_list_.clear();
}
/// Create the conjunction of all the atomic properties from
/// the successors of the current state.
void
saba_complement_tgba_succ_iterator::get_conj_list()
{
std::set<int> atomics;
delete_condition_list();
for (auto iterator: automaton_->succ(origin_->get_state()))
{
bdd c = iterator->current_condition();
get_atomics(atomics, c);
}
// Compute the conjunction of all those atomic properties.
unsigned atomics_size = atomics.size();
assert(atomics_size < 32);
for (unsigned i = 1; i <= static_cast<unsigned>(1 << atomics_size); ++i)
{
bdd result = bddtrue;
unsigned position = 1;
for (std::set<int>::const_iterator a_it = atomics.begin();
a_it != atomics.end();
++a_it, position <<= 1)
{
bdd this_atomic;
if (position & i)
this_atomic = bdd_ithvar(*a_it);
else
this_atomic = bdd_nithvar(*a_it);
result = bdd_apply(result, this_atomic, bddop_and);
}
condition_list_[result] = state_conjunction_list_t();
}
}
void
saba_complement_tgba_succ_iterator::first()
{
current_condition_ = condition_list_.begin();
if (current_condition_ != condition_list_.end())
{
current_conjunction_ = current_condition_->second.begin();
current_end_conjunction_ = current_condition_->second.end();
}
}
void
saba_complement_tgba_succ_iterator::next()
{
if (++current_conjunction_ == current_end_conjunction_)
{
++current_condition_;
if (current_condition_ != condition_list_.end())
{
current_conjunction_ = current_condition_->second.begin();
current_end_conjunction_ = current_condition_->second.end();
}
}
}
bool
saba_complement_tgba_succ_iterator::done() const
{
return (current_condition_ == condition_list_.end());
}
saba_state_conjunction*
saba_complement_tgba_succ_iterator::current_conjunction() const
{
return (*current_conjunction_)->clone();
}
bdd
saba_complement_tgba_succ_iterator::current_condition() const
{
return current_condition_->first;
}
} // end namespace anonymous.
saba_complement_tgba::saba_complement_tgba(const const_tgba_ptr& a)
: automaton_(degeneralize(a))
{
get_dict()->register_all_variables_of(automaton_, this);
int v = get_dict()
->register_acceptance_variable(ltl::constant::true_instance(), this);
the_acceptance_cond_ = bdd_ithvar(v);
nb_states_ = automaton_->num_states();
}
saba_complement_tgba::~saba_complement_tgba()
{
get_dict()->unregister_all_my_variables(this);
}
saba_state*
saba_complement_tgba::get_init_state() const
{
state* original_init_state = automaton_->get_init_state();
saba_state_complement_tgba* new_init;
if (automaton_->state_is_accepting(original_init_state))
new_init =
new saba_state_complement_tgba(shared_state(original_init_state,
shared_state_deleter),
2 * nb_states_,
the_acceptance_cond_);
else
new_init =
new saba_state_complement_tgba(shared_state(original_init_state,
shared_state_deleter),
2 * nb_states_,
bddfalse);
return new_init;
}
saba_succ_iterator*
saba_complement_tgba::succ_iter(const saba_state* local_state) const
{
const saba_state_complement_tgba* state =
dynamic_cast<const saba_state_complement_tgba*>(local_state);
assert(state);
return new saba_complement_tgba_succ_iterator(automaton_,
the_acceptance_cond_,
state);
}
bdd_dict_ptr
saba_complement_tgba::get_dict() const
{
return automaton_->get_dict();
}
std::string
saba_complement_tgba::format_state(const saba_state* state) const
{
const saba_state_complement_tgba* s =
dynamic_cast<const saba_state_complement_tgba*>(state);
assert(s);
std::ostringstream ss;
ss << "{ original: " << automaton_->format_state(s->get_state())
<< "\n rank: " << s->get_rank()
<< "\n acc: " << bdd_format_accset(get_dict(),
s->acceptance_conditions())
<< " }";
return ss.str();
}
bdd
saba_complement_tgba::all_acceptance_conditions() const
{
return the_acceptance_cond_;
}
} // end namespace spot.

85
src/saba/sabacomplementtgba.hh
View file

@ -1,85 +0,0 @@
// Copyright (C) 2009, 2010, 2013, 2014 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/>.
#ifndef SPOT_SABA_SABACOMPLEMENTTGBA_HH
#define SPOT_SABA_SABACOMPLEMENTTGBA_HH
#include "tgba/fwd.hh"
#include "saba.hh"
namespace spot
{
/// \ingroup saba
/// \brief Complement a TGBA and produce a SABA.
///
/// The original TGBA is transformed into a States-based
/// Büchi Automaton.
///
/// Several techniques are supposed to by applied on the resulting
/// automaton before its transformation into a TGBA. Those techniques
/// are expected to reduce the size of the automaton.
///
/// This algorithm comes from:
/** \verbatim
@Article{ gurumurthy.03.lncs,
title = {On complementing nondeterministic {B\"uchi} automata},
author = {Gurumurthy, S. and Kupferman, O. and Somenzi, F. and
Vardi, M.Y.},
journal = {Lecture Notes in Computer Science},
pages = {96--110},
year = {2003},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// The construction is done on-the-fly, by the
/// \c saba_complement_succ_iterator class.
/// \see saba_complement_succ_iterator
class SPOT_API saba_complement_tgba : public saba
{
public:
saba_complement_tgba(const const_tgba_ptr& a);
virtual ~saba_complement_tgba();
// tgba interface
virtual saba_state* get_init_state() const;
virtual saba_succ_iterator*
succ_iter(const saba_state* local_state) const;
virtual bdd_dict_ptr get_dict() const;
virtual std::string format_state(const saba_state* state) const;
virtual bdd all_acceptance_conditions() const;
private:
const_tgba_digraph_ptr automaton_;
bdd the_acceptance_cond_;
unsigned nb_states_;
}; // end class tgba_saba_complement.
typedef std::shared_ptr<saba_complement_tgba> saba_complement_tgba_ptr;
typedef std::shared_ptr<const saba_complement_tgba>
const_saba_complement_tgba_ptr;
inline saba_complement_tgba_ptr make_saba_complement(const const_tgba_ptr& a)
{
return std::make_shared<saba_complement_tgba>(a);
}
} // end namespace spot.
#endif // SPOT_SABA_SABACOMPLEMENTTGBA_HH

247
src/saba/sabastate.hh
View file

@ -1,247 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 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/>.
#ifndef SPOT_SABA_SABASTATE_HH
# define SPOT_SABA_SABASTATE_HH
#include "misc/common.hh"
#include <bdd.h>
#include <functional>
#include <memory>
#include <cassert>
namespace spot
{
/// \ingroup saba_essentials
/// \brief Abstract class for saba states.
class SPOT_API 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 an \c unordered_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 an \c unordered_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()
{
}
};
/// \ingroup saba_essentials
/// \brief Strict Weak Ordering for \c saba_state*.
///
/// 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;
}
};
/// \ingroup saba_essentials
/// \brief An Equivalence Relation for \c saba_state*.
///
/// This is meant to be used as a comparison functor for
/// \c unordered_map whose keys 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::unordered_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);
}
};
/// \ingroup saba_essentials
/// \ingroup hash_funcs
/// \brief Hash Function for \c saba_state*.
///
/// This is meant to be used as a hash functor for
/// an \c unordered_map whose keys 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::unordered_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 std::shared_ptr<const saba_state> shared_saba_state;
/// \ingroup saba_essentials
/// \brief Strict Weak Ordering for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose keys 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;
}
};
/// \ingroup saba_essentials
/// \brief An Equivalence Relation for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
///
/// This is meant to be used as a comparison functor for
/// an \c unordred_map whose keys 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::unordered_map<shared_saba_state, int,
/// saba_state_shared_ptr_hash,
/// 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());
}
};
/// \ingroup saba_essentials
/// \ingroup hash_funcs
/// \brief Hash Function for \c shared_saba_state
/// (shared_ptr<const saba_state*>).
///
/// This is meant to be used as a hash functor for
/// \c unordered_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::unordered_map<shared_saba_state, int,
/// saba_state_shared_ptr_hash,
/// 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

158
src/saba/sabasucciter.hh
View file

@ -1,158 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 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/>.
#ifndef SPOT_SABA_SABASUCCITER_HH
# define SPOT_SABA_SABASUCCITER_HH
#include "sabastate.hh"
namespace spot
{
/// \ingroup saba_essentials
/// \brief Iterate over a conjunction of saba_state.
///
/// This class provides the basic functionalities required to
/// iterate over a conjunction of states of a saba.
class SPOT_API 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;
};
/// \ingroup saba_essentials
/// \brief Iterate over the successors of a saba_state.
///
/// 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 SPOT_API 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

28
src/sabaalgos/Makefile.am
View file

@ -1,28 +0,0 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2011, 2013 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/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
sabaalgosdir = $(pkgincludedir)/sabaalgos
sabaalgos_HEADERS = sabadotty.hh sabareachiter.hh
noinst_LTLIBRARIES = libsabaalgos.la
libsabaalgos_la_SOURCES = sabadotty.cc sabareachiter.cc

105
src/sabaalgos/sabadotty.cc
View file

@ -1,105 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2014 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 <ostream>
#include "sabadotty.hh"
#include "tgba/bddprint.hh"
#include "sabareachiter.hh"
#include "misc/escape.hh"
namespace spot
{
namespace
{
class saba_dotty_bfs : public saba_reachable_iterator_breadth_first
{
public:
saba_dotty_bfs(std::ostream& os, const const_saba_ptr& a)
: saba_reachable_iterator_breadth_first(a), os_(os)
{
}
void
start()
{
os_ << "digraph G {" << std::endl;
os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl;
os_ << " 0 -> 1;" << std::endl;
}
void
end()
{
os_ << '}' << std::endl;
}
void
process_state(const saba_state* s, int n)
{
std::string label =
escape_str(automata_->format_state(s))
+ "\\n"
+ bdd_format_accset(automata_->get_dict(),
s->acceptance_conditions());
os_ << " " << n << ' '
<< "[label=\"" << label << "\"];\n";
}
void
process_state_conjunction(const saba_state*, int in,
const saba_state_conjunction*,
int sc_id,
const saba_succ_iterator* si)
{
os_ << " s" << in << "sc" << sc_id
<< " [label=\"\", style=invis, height=0];" << std::endl;
std::string label =
bdd_format_formula(automata_->get_dict(),
si->current_condition());
os_ << " " << in << " -> s" << in << "sc" << sc_id
<< " [label=\"" << label << "\", arrowhead=\"none\"];\n";
}
void
process_link(const saba_state*, int in,
const saba_state*, int out,
const saba_state_conjunction*,
int sc_id,
const saba_succ_iterator*)
{
os_ << " s" << in << "sc" << sc_id << " -> " << out
<< " [label=\"\"];\n";
}
private:
std::ostream& os_;
};
}
std::ostream&
saba_dotty_reachable(std::ostream& os, const const_saba_ptr& g)
{
saba_dotty_bfs d(os, g);
d.run();
return os;
}
}

36
src/sabaalgos/sabadotty.hh
View file

@ -1,36 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013, 2014 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/>.
#ifndef SPOT_SABAALGOS_SABADOTTY_HH
# define SPOT_SABAALGOS_SABADOTTY_HH
#include "misc/common.hh"
#include <iosfwd>
#include "saba/saba.hh"
namespace spot
{
/// \ingroup saba_io
/// \brief Print reachable states in dot format.
SPOT_API std::ostream&
saba_dotty_reachable(std::ostream& os,
const const_saba_ptr& g);
}
#endif // SPOT_SABAALGOS_SABADOTTY_HH

187
src/sabaalgos/sabareachiter.cc
View file

@ -1,187 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2014 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 <cassert>
#include "sabareachiter.hh"
namespace spot
{
// saba_reachable_iterator
//////////////////////////////////////////////////////////////////////
saba_reachable_iterator::saba_reachable_iterator(const const_saba_ptr& a)
: automata_(a)
{
}
saba_reachable_iterator::~saba_reachable_iterator()
{
seen_map::const_iterator s = seen.begin();
while (s != seen.end())
{
// Advance the iterator before deleting the "key" pointer.
const saba_state* ptr = s->first;
++s;
delete ptr;
}
}
void
saba_reachable_iterator::run()
{
int n = 0;
int conjn = 0;
start();
saba_state* i = automata_->get_init_state();
if (want_state(i))
add_state(i);
seen[i] = ++n;
const saba_state* t;
while ((t = next_state()))
{
assert(seen.find(t) != seen.end());
int tn = seen[t];
saba_succ_iterator* si = automata_->succ_iter(t);
process_state(t, tn);
for (si->first(); !si->done(); si->next())
{
saba_state_conjunction* conj = si->current_conjunction();
++conjn;
process_state_conjunction(t, tn, conj, conjn, si);
for (conj->first(); !conj->done(); conj->next())
{
const saba_state* current = conj->current_state();
seen_map::const_iterator s = seen.find(current);
bool ws = want_state(current);
if (s == seen.end())
{
seen[current] = ++n;
if (ws)
{
add_state(current);
process_link(t, tn, current, n, conj, conjn, si);
}
}
else
{
if (ws)
process_link(t, tn, s->first, s->second, conj, conjn, si);
delete current;
}
}
delete conj;
}
delete si;
}
end();
}
bool
saba_reachable_iterator::want_state(const saba_state*) const
{
return true;
}
void
saba_reachable_iterator::start()
{
}
void
saba_reachable_iterator::end()
{
}
void
saba_reachable_iterator::process_state(const saba_state*, int)
{
}
void
saba_reachable_iterator::
process_state_conjunction(const saba_state*, int,
const saba_state_conjunction*,
int,
const saba_succ_iterator*)
{
}
void
saba_reachable_iterator::process_link(const saba_state*, int,
const saba_state*, int,
const saba_state_conjunction*,
int,
const saba_succ_iterator*)
{
}
// saba_reachable_iterator_depth_first
//////////////////////////////////////////////////////////////////////
saba_reachable_iterator_depth_first::
saba_reachable_iterator_depth_first(const const_saba_ptr& a)
: saba_reachable_iterator(a)
{
}
void
saba_reachable_iterator_depth_first::add_state(const saba_state* s)
{
todo.push(s);
}
const saba_state*
saba_reachable_iterator_depth_first::next_state()
{
if (todo.empty())
return 0;
const saba_state* s = todo.top();
todo.pop();
return s;
}
// saba_reachable_iterator_breadth_first
//////////////////////////////////////////////////////////////////////
saba_reachable_iterator_breadth_first::
saba_reachable_iterator_breadth_first(const const_saba_ptr& a)
: saba_reachable_iterator(a)
{
}
void
saba_reachable_iterator_breadth_first::add_state(const saba_state* s)
{
todo.push_back(s);
}
const saba_state*
saba_reachable_iterator_breadth_first::next_state()
{
if (todo.empty())
return 0;
const saba_state* s = todo.front();
todo.pop_front();
return s;
}
}

153
src/sabaalgos/sabareachiter.hh
View file

@ -1,153 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013, 2014 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/>.
#ifndef SPOT_SABAALGOS_SABAREACHITER_HH
# define SPOT_SABAALGOS_SABAREACHITER_HH
#include "misc/hash.hh"
#include "saba/saba.hh"
#include <stack>
#include <deque>
namespace spot
{
/// \ingroup saba_generic
/// \brief Iterate over all reachable states of a spot::saba.
class SPOT_API saba_reachable_iterator
{
public:
saba_reachable_iterator(const const_saba_ptr& a);
virtual ~saba_reachable_iterator();
/// \brief Iterate over all reachable states of a spot::saba.
///
/// This is a template method that will call add_state(), next_state(),
/// start(), end(), process_state(), process_state_conjunction() and
/// process_link(), while it iterates over states.
void run();
/// \name Todo list management.
///
/// spot::saba_reachable_iterator_depth_first and
/// spot::saba_reachable_iterator_breadth_first offer two precanned
/// implementations for these functions.
/// \{
/// \brief Called by run() to register newly discovered states.
virtual void add_state(const saba_state* s) = 0;
/// \brief Called by run() to obtain the next state to process.
virtual const saba_state* next_state() = 0;
/// \}
/// Called by add_state or next_states implementations to filter
/// states. Default implementation always return true.
virtual bool want_state(const saba_state* s) const;
/// Called by run() before starting its iteration.
virtual void start();
/// Called by run() once all states have been explored.
virtual void end();
/// Called by run() to process a state.
///
/// \param s The current state.
/// \param n A unique number assigned to \a s.
virtual void process_state(const saba_state* s, int n);
/// Called by run() to process a conjunction of states.
///
/// \param in_s The current state.
/// \param in An unique number assigned to \a in_s.
/// \param sc The spot::saba_state_conjunction positionned on the current
/// conjunction.
/// \param sc_id An unique number for the this transition assigned to \a sc.
/// \param si The spot::saba_succ_iterator positionned on the current
/// transition.
virtual void
process_state_conjunction(const saba_state* in_s, int in,
const saba_state_conjunction* sc,
int sc_id,
const saba_succ_iterator* si);
/// Called by run() to process a transition.
///
/// \param in_s The source state
/// \param in The source state number.
/// \param out_s The destination state
/// \param out The destination state number.
/// \param sc The spot::saba_state_conjunction positionned on the current
/// conjunction.
/// \param sc_id An unique number for the this transition assigned to \a sc.
/// \param si The spot::saba_succ_iterator positionned on the current
/// transition.
///
/// The in_s and out_s states are owned by the
/// spot::saba_reachable_iterator instance and destroyed when the
/// instance is destroyed.
virtual void
process_link(const saba_state* in_s, int in,
const saba_state* out_s, int out,
const saba_state_conjunction* sc,
int sc_id,
const saba_succ_iterator* si);
protected:
const_saba_ptr automata_; ///< The spot::saba to explore.
typedef
std::unordered_map<const saba_state*, int,
saba_state_ptr_hash, saba_state_ptr_equal> seen_map;
seen_map seen; ///< States already seen.
};
/// \ingroup saba_generic
/// \brief An implementation of spot::saba_reachable_iterator that browses
/// states depth first.
class SPOT_API saba_reachable_iterator_depth_first:
public saba_reachable_iterator
{
public:
saba_reachable_iterator_depth_first(const const_saba_ptr& a);
virtual void add_state(const saba_state* s);
virtual const saba_state* next_state();
protected:
std::stack<const saba_state*> todo; ///< A stack of states yet to explore.
};
/// \ingroup saba_generic
/// \brief An implementation of spot::saba_reachable_iterator that browses
/// states breadth first.
class SPOT_API saba_reachable_iterator_breadth_first:
public saba_reachable_iterator
{
public:
saba_reachable_iterator_breadth_first(const const_saba_ptr& a);
virtual void add_state(const saba_state* s);
virtual const saba_state* next_state();
protected:
std::deque<const saba_state*> todo; ///< A queue of states yet to explore.
};
}
#endif // SPOT_SABAALGOS_SABAREACHITER_HH

2
src/sabatest/.gitignore vendored
View file

@ -1,2 +0,0 @@
defs
sabacomplementtgba

37
src/sabatest/Makefile.am
View file

@ -1,37 +0,0 @@
## Copyright (C) 2009, 2011 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/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = ../libspot.la
# These are the most used test programs, and they are also useful
# to run manually outside the test suite. Always build them.
# noinst_PROGRAMS =
check_SCRIPTS = defs
# Keep this sorted alphabetically.
check_PROGRAMS = \
sabacomplementtgba
# Keep this sorted alphabetically.
sabacomplementtgba_SOURCES = sabacomplementtgba.cc
# Keep this sorted by STRENGTH. Test basic things first,
# because such failures will be easier to diagnose and fix.
# TESTS =

87
src/sabatest/defs.in
View file

@ -1,87 +0,0 @@
# -*- shell-script -*-
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2006 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 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/>.
# Ensure we are running from the right directory.
test -f ./defs || {
echo "defs: not found in current directory" 1>&2
exit 1
}
# If srcdir is not set, then we are not running from `make check'.
if test -z "$srcdir"; then
# compute $srcdir.
srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
test $srcdir = $0 && srcdir=.
fi
# Ensure $srcdir is set correctly.
test -f $srcdir/defs.in || {
echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
exit 1
}
echo "== Running test $0"
me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
testSubDir=$me.dir
chmod -R a+rwx $testSubDir > /dev/null 2>&1
rm -rf $testSubDir > /dev/null 2>&1
mkdir $testSubDir
cd $testSubDir
# Adjust srcdir now that we are in a subdirectory. We still want to
# source directory corresponding to the build directory that contains
# $testSubDir.
case $srcdir in
# I
[\\/$]* | ?:[\\/]* );;
*) srcdir=../$srcdir
esac
DOT='@DOT@'
top_builddir='../@top_builddir@'
LBTT="@LBTT@"
LBTT_TRANSLATE="@LBTT_TRANSLATE@"
VALGRIND='@VALGRIND@'
run()
{
expected_exitcode=$1
shift
exitcode=0
if test -n "$VALGRIND"; then
exec 6>valgrind.err
GLIBCPP_FORCE_NEW=1 \
../../../libtool --mode=execute \
$VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" ||
exitcode=$?
cat valgrind.err 1>&2
test -z "`sed 1q valgrind.err`" || exit 50
rm -f valgrind.err
else
"$@" || exitcode=$?
fi
test $exitcode = $expected_exitcode || exit 1
}
set -x

76
src/sabatest/sabacomplementtgba.cc
View file

@ -1,76 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2014 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 <iostream>
#include <cstring>
#include <saba/saba.hh>
#include <saba/sabacomplementtgba.hh>
#include <tgba/tgba.hh>
#include <tgbaparse/public.hh>
#include <sabaalgos/sabadotty.hh>
#include <tgbaalgos/ltl2tgba_fm.hh>
#include <ltlparse/public.hh>
void usage(const std::string& argv0)
{
std::cerr
<< "usage " << argv0 << " [options]" << std::endl
<< "options:" << std::endl
<< "-f formula display the saba of !forumula"
<< std::endl;
}
int main(int argc, char* argv[])
{
std::string formula;
for (int i = 1; i < argc; ++i)
{
if (!strcmp(argv[i], "-f"))
{
if (i + 1 >= argc)
{
usage(argv[0]);
return 1;
}
formula = argv[++i];
}
else
{
usage(argv[0]);
return 1;
}
}
if (formula.empty())
{
usage(argv[0]);
return 1;
}
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1);
if (spot::ltl::format_parse_errors(std::cerr, formula, p1))
return 2;
auto a = spot::ltl_to_tgba_fm(f1, spot::make_bdd_dict());
auto complement = spot::make_saba_complement(a);
spot::saba_dotty_reachable(std::cout, complement);
f1->destroy();
}