Commit 65bfea0c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* m4/gspnlib.m4: Define LIBGSPNESRG_LDFLAGS.

* iface/gspn/Makefile.am (gspn_HEADERS): Add common.hh.
(libspotgspn_la_SOURCES): Add common.cc.
(libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS)
(libspotgspneesrg_la_SOURCES, ltlgspn_eesrg_SOURCES)
(dotty_eesrg_LDADD, dotty_eesrg_CPPFLAGS): New variables.
(lib_LTLIBRARIES): Add libspotgspneesrg.la.
(check_PROGRAMS): Add dottygspn-eesrg.
* iface/gspn/gspn.hh, iface/gspn/gspn.cc
(gspn_exeption, operator<<(gspn_exeption), gspn_environment): Move ...
* iface/gspn/common.hh, iface/gspn/common.cc: ... in these new files.
* iface/gspn/eesrg.hh, iface/gspn/eesrg.cc, iface/gspn/dottyeesrg.cc:
New files.
parent 66f05a26
2003-10-30 Alexandre Duret-Lutz <adl@src.lip6.fr>
* m4/gspnlib.m4: Define LIBGSPNESRG_LDFLAGS.
* iface/gspn/Makefile.am (gspn_HEADERS): Add common.hh.
(libspotgspn_la_SOURCES): Add common.cc.
(libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS)
(libspotgspneesrg_la_SOURCES, ltlgspn_eesrg_SOURCES)
(dotty_eesrg_LDADD, dotty_eesrg_CPPFLAGS): New variables.
(lib_LTLIBRARIES): Add libspotgspneesrg.la.
(check_PROGRAMS): Add dottygspn-eesrg.
* iface/gspn/gspn.hh, iface/gspn/gspn.cc
(gspn_exeption, operator<<(gspn_exeption), gspn_environment): Move ...
* iface/gspn/common.hh, iface/gspn/common.cc: ... in these new files.
* iface/gspn/eesrg.hh, iface/gspn/eesrg.cc, iface/gspn/dottyeesrg.cc:
New files.
2003-10-28 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
......
......@@ -4,16 +4,25 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
gspndir = $(pkgincludedir)/gspn
gspn_HEADERS = \
common.hh \
gspn.hh
lib_LTLIBRARIES = libspotgspn.la
lib_LTLIBRARIES = libspotgspn.la libspotgspneesrg.la
libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la
libspotgspn_la_SOURCES = \
common.cc \
gspn.cc
libspotgspneesrg_la_LIBADD = $(top_builddir)/src/libspot.la
libspotgspneesrg_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS)
libspotgspneesrg_la_SOURCES = \
common.cc \
eesrg.cc
check_PROGRAMS = \
dottygspn-rg \
dottygspn-srg \
dottygspn-eesrg \
ltlgspn-rg \
ltlgspn-srg
......@@ -23,6 +32,9 @@ dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
dottygspn_srg_SOURCES = dottygspn.cc
dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
dottygspn_eesrg_SOURCES = dottyeesrg.cc
dottygspn_eesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS)
ltlgspn_rg_SOURCES = ltlgspn.cc
ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
......
#include "common.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
std::ostream&
operator<<(std::ostream& os, const gspn_exeption& e)
{
os << e.get_where() << " exited with " << e.get_err();
return os;
}
// gspn_environment
//////////////////////////////////////////////////////////////////////
gspn_environment::gspn_environment()
{
}
gspn_environment::~gspn_environment()
{
for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i)
ltl::destroy(i->second);
}
bool
gspn_environment::declare(const std::string& prop_str)
{
if (props_.find(prop_str) != props_.end())
return false;
props_[prop_str] = ltl::atomic_prop::instance(prop_str, *this);
return true;
}
ltl::formula*
gspn_environment::require(const std::string& prop_str)
{
prop_map::iterator i = props_.find(prop_str);
if (i == props_.end())
return 0;
// It's an atomic_prop, so we do not have to use the clone() visitor.
return i->second->ref();
}
/// Get the name of the environment.
const std::string&
gspn_environment::name()
{
static std::string name("gspn environment");
return name;
}
const gspn_environment::prop_map&
gspn_environment::get_prop_map() const
{
return props_;
}
}
#ifndef SPOT_IFACE_GSPN_COMMON_HH
# define SPOT_IFACE_GSPN_COMMON_HH
# include <string>
# include <iostream>
# include "ltlast/atomic_prop.hh"
# include "ltlenv/environment.hh"
// Do not include gspnlib.h here, or it will polute the user's
// namespace with internal C symbols.
namespace spot
{
/// An exeption used to forward GSPN errors.
class gspn_exeption
{
public:
gspn_exeption(const std::string& where, int err)
: err_(err), where_(where)
{
}
int
get_err() const
{
return err_;
}
std::string
get_where() const
{
return where_;
}
private:
int err_;
std::string where_;
};
std::ostream& operator<<(std::ostream& os, const gspn_exeption& e);
class gspn_environment : public ltl::environment
{
public:
gspn_environment();
~gspn_environment();
/// Declare an atomic proposition. Return false iff the
/// proposition was already declared.
bool declare(const std::string& prop_str);
virtual ltl::formula* require(const std::string& prop_str);
/// Get the name of the environment.
virtual const std::string& name();
typedef std::map<const std::string, ltl::atomic_prop*> prop_map;
/// Get the map of atomic proposition known to this environment.
const prop_map& get_prop_map() const;
private:
prop_map props_;
};
}
#endif // SPOT_IFACE_GSPN_COMMON_HH
#include "eesrg.hh"
#include "tgbaalgos/dotty.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
int
main(int argc, char **argv)
try
{
spot::gspn_environment env;
if (argc <= 3)
{
std::cerr << "usage: " << argv[0] << " model automata props..."
<< std::endl;
exit(1);
}
while (argc > 3)
env.declare(argv[--argc]);
spot::gspn_eesrg_interface gspn(2, argv);
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[--argc], pel1,
dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
{
spot::tgba_gspn_eesrg a(dict, env, control);
spot::dotty_reachable(std::cout, &a);
}
delete control;
delete dict;
}
catch (spot::gspn_exeption e)
{
std::cerr << e << std::endl;
throw;
}
#include <sstream>
#include <cstring>
#include <map>
#include <cassert>
#include "eesrg.hh"
#include <gspnlib.h>
#include "misc/bddlt.hh"
#include <bdd.h>
namespace spot
{
gspn_eesrg_interface::gspn_eesrg_interface(int argc, char **argv)
{
int res = initialize(argc, argv);
if (res)
throw gspn_exeption("initialize()", res);
}
gspn_eesrg_interface::~gspn_eesrg_interface()
{
int res = finalize();
if (res)
throw gspn_exeption("finalize()", res);
}
// state_gspn_eesrg
//////////////////////////////////////////////////////////////////////
class state_gspn_eesrg: public state
{
public:
state_gspn_eesrg(State left, const state* right)
: left_(left), right_(right)
{
}
virtual
~state_gspn_eesrg()
{
delete right_;
}
virtual int
compare(const state* other) const
{
const state_gspn_eesrg* o = dynamic_cast<const state_gspn_eesrg*>(other);
assert(o);
int res = (reinterpret_cast<char*>(o->left())
- reinterpret_cast<char*>(left()));
if (res != 0)
return res;
return right_->compare(o->right());
}
virtual size_t
hash() const
{
return (reinterpret_cast<char*>(left())
- static_cast<char*>(0)) << 10 + right_->hash();
}
virtual state_gspn_eesrg* clone() const
{
return new state_gspn_eesrg(left(), right());
}
State
left() const
{
return left_;
}
const state*
right() const
{
return right_;
}
private:
State left_;
const state* right_;
}; // state_gspn_eesrg
// tgba_gspn_eesrg_private_
//////////////////////////////////////////////////////////////////////
struct tgba_gspn_eesrg_private_
{
int refs; // reference count
bdd_dict* dict;
typedef std::map<int, AtomicProp> prop_map;
prop_map prop_dict;
signed char* all_props;
size_t prop_count;
const tgba* operand;
tgba_gspn_eesrg_private_(bdd_dict* dict, const gspn_environment& env,
const tgba* operand)
: refs(1), dict(dict), all_props(0),
operand(operand)
{
const gspn_environment::prop_map& p = env.get_prop_map();
try
{
AtomicProp max_prop = 0;
for (gspn_environment::prop_map::const_iterator i = p.begin();
i != p.end(); ++i)
{
int var = dict->register_proposition(i->second, this);
AtomicProp index;
int err = prop_index(i->first.c_str(), &index);
if (err)
throw gspn_exeption("prop_index()", err);
prop_dict[var] = index;
max_prop = std::max(max_prop, index);
}
prop_count = 1 + max_prop;
all_props = new signed char[prop_count];
}
catch (...)
{
// If an exception occurs during the loop, we need to clean
// all BDD variables which have been registered so far.
dict->unregister_all_my_variables(this);
throw;
}
}
tgba_gspn_eesrg_private_::~tgba_gspn_eesrg_private_()
{
dict->unregister_all_my_variables(this);
if (all_props)
delete[] all_props;
}
};
// tgba_succ_iterator_gspn_eesrg
//////////////////////////////////////////////////////////////////////
class tgba_succ_iterator_gspn_eesrg: public tgba_succ_iterator
{
public:
tgba_succ_iterator_gspn_eesrg(State state,
tgba_gspn_eesrg_private_* data,
tgba_succ_iterator* operand)
: state_(state),
operand_(operand),
all_conds_(bddfalse),
successors_(0),
size_(0),
current_(0),
data_(data)
{
}
virtual
~tgba_succ_iterator_gspn_eesrg()
{
if (operand_)
delete operand_;
if (successors_)
succ_free(successors_);
}
void
step()
{
if (current_ < size_)
{
++current_;
return;
}
if (successors_)
succ_free(successors_);
current_ = 0;
if (all_conds_ == bddfalse)
{
// SUCCESSORS_ is 0 when step() is called from first().
if (successors_)
operand_->next();
all_conds_ = operand_->current_condition();
outside_ = !all_conds_;
}
bdd cond = bdd_satone(all_conds_);
cond = bdd_simplify(cond, cond | outside_);
all_conds_ -= cond;
// Translate COND into an array of properties.
signed char* props = data_->all_props;
memset(props, -1, data_->prop_count);
while (cond != bddtrue)
{
int var = bdd_var(cond);
tgba_gspn_eesrg_private_::prop_map::iterator i =
data_->prop_dict.find(var);
assert(i != data_->prop_dict.end());
bdd high = bdd_high(cond);
if (high == bddfalse)
{
cond = bdd_low(cond);
props[i->second] = 0;
}
else
{
cond = high;
props[i->second] = 1;
}
assert(cond != bddfalse);
}
succ(state_, props, &successors_, &size_);
}
virtual void
first()
{
size_ = 0;
all_conds_ = bddfalse;
operand_->first();
if (operand_->done())
{
delete operand_;
operand_ = 0;
return;
}
if (successors_)
{
delete successors_;
successors_ = 0;
}
step();
}
virtual void
next()
{
assert(!done());
step();
}
virtual bool
done() const
{
return (size_ <= current_
&& all_conds_ == bddfalse
&& operand_
&& operand_->done());
}
virtual state*
current_state() const
{
return new state_gspn_eesrg(successors_[current_],
operand_->current_state());
}
virtual bdd
current_condition() const
{
return bddtrue;
}
virtual bdd
current_accepting_conditions() const
{
// There is no acceptance conditions in GSPN systems, so we just
// return those from OPERAND_.
return operand_->current_accepting_conditions();
}
private:
State state_;
// Iterator on the right operand
tgba_succ_iterator* operand_;
// All conditions of the current successor of the right operand
// (We will iterate on all conjunctions in this.)
bdd all_conds_;
bdd outside_;
// All successors of STATE matching a selection conjunctions from
// ALL_CONDS.
State* successors_; /// array of successors
size_t size_; /// size of successors_
size_t current_; /// current position in successors_
tgba_gspn_eesrg_private_* data_;
}; // tgba_succ_iterator_gspn_eesrg
// tgba_gspn_eesrg
//////////////////////////////////////////////////////////////////////
tgba_gspn_eesrg::tgba_gspn_eesrg(bdd_dict* dict, const gspn_environment& env,
const tgba* operand)
{
data_ = new tgba_gspn_eesrg_private_(dict, env, operand);
}
tgba_gspn_eesrg::tgba_gspn_eesrg(const tgba_gspn_eesrg& other)
: tgba()
{
data_ = other.data_;
++data_->refs;
}
tgba_gspn_eesrg::~tgba_gspn_eesrg()
{
if (--data_->refs == 0)
delete data_;
}
tgba_gspn_eesrg&
tgba_gspn_eesrg::operator=(const tgba_gspn_eesrg& other)
{
if (&other == this)
return *this;
this->~tgba_gspn_eesrg();
new (this) tgba_gspn_eesrg(other);
return *this;
}
state* tgba_gspn_eesrg::get_init_state() const
{
State s;
int err = initial_state(&s);
if (err)
throw gspn_exeption("initial_state()", err);
return new state_gspn_eesrg(s, data_->operand->get_init_state());
}
tgba_succ_iterator*
tgba_gspn_eesrg::succ_iter(const state* state,
const state* global_state,
const tgba* global_automaton) const
{
const state_gspn_eesrg* s = dynamic_cast<const state_gspn_eesrg*>(state);
assert(s);
(void) global_state;
(void) global_automaton;
tgba_succ_iterator* i = data_->operand->succ_iter(s->right());
return new tgba_succ_iterator_gspn_eesrg(s->left(), data_, i);
}
bdd
tgba_gspn_eesrg::compute_support_conditions(const spot::state* state) const
{
(void) state;
return bddtrue;
}
bdd
tgba_gspn_eesrg::compute_support_variables(const spot::state* state) const
{
(void) state;
return bddtrue;
}
bdd_dict*
tgba_gspn_eesrg::get_dict() const
{
return data_->dict;
}
std::string
tgba_gspn_eesrg::format_state(const state* state) const
{
const state_gspn_eesrg* s = dynamic_cast<const state_gspn_eesrg*>(state);
assert(s);
std::ostringstream os;
char* str;
int err = print_state(s->left(), &str);
if (err)
throw gspn_exeption("print_state()", err);
// Rewrite all new lines as \\\n.
const char* pos = str;
while (*pos)
{
switch (*pos)
{
// Rewrite all new lines as \\n, and strip the last one.
case '\n':
if (pos[1])