* m4/gspnlib.m4: New file.
* configure.ac: Call AX_CHECK_GSPNLIB. * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, dottygspn_LDADD): New variables. * iface/gspn/gspn.hh (gspn_interface): New class. (gspn_exeption): Take a string argument and adjust all callers. (operator<<): Define for gspn_exeption. * iface/gspn/gspn.cc (gspn_interface::gspn_interface, gspn_interface::~gspn_interface): New. * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. * iface/gspn/dottygspn.cc: New file.
This commit is contained in:
Alexandre Duret-Lutz
parent
49fd9579da
commit
4ac192ac1e
9 changed files with 137 additions and 120 deletions
|
|
@ -1,8 +1,14 @@
|
|||
AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS)
|
||||
AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) $(LIBGSPN_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
lib_LTLIBRARIES = libspotgspn.la
|
||||
libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la
|
||||
libspotgspn_la_SOURCES = \
|
||||
gspn.hh \
|
||||
gspn.cc \
|
||||
gspnlib.h
|
||||
|
||||
check_PROGRAMS = dottygspn
|
||||
|
||||
dottygspn_SOURCES = dottygspn.cc
|
||||
dottygspn_LDADD = libspotgspn.la $(LIBGSPN_LDFLAGS)
|
||||
|
|
|
|||
26
iface/gspn/dottygspn.cc
Normal file
26
iface/gspn/dottygspn.cc
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
#include "gspn.hh"
|
||||
#include "tgbaalgos/dotty.hh"
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
try
|
||||
{
|
||||
spot::gspn_interface gspn(argc, argv);
|
||||
|
||||
spot::gspn_environment env;
|
||||
env.declare("obs");
|
||||
|
||||
spot::bdd_dict* dict = new spot::bdd_dict();
|
||||
|
||||
spot::tgba_gspn a(dict, env);
|
||||
|
||||
spot::dotty_reachable(std::cout, &a);
|
||||
|
||||
delete dict;
|
||||
}
|
||||
catch (spot::gspn_exeption e)
|
||||
{
|
||||
std::cerr << e << std::endl;
|
||||
throw;
|
||||
}
|
||||
|
||||
|
|
@ -8,6 +8,21 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
gspn_interface::gspn_interface(int argc, char **argv)
|
||||
{
|
||||
int res = initialize(argc, argv);
|
||||
if (res)
|
||||
throw gspn_exeption("initialize()", res);
|
||||
}
|
||||
|
||||
gspn_interface::~gspn_interface()
|
||||
{
|
||||
int res = finalize();
|
||||
if (res)
|
||||
throw gspn_exeption("finalize()", res);
|
||||
}
|
||||
|
||||
|
||||
// tgba_gspn_private_
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -36,11 +51,11 @@ namespace spot
|
|||
AtomicProp index;
|
||||
int err = prop_index(i->first.c_str(), &index);
|
||||
if (err)
|
||||
throw gspn_exeption(err);
|
||||
throw gspn_exeption("prop_index()", err);
|
||||
AtomicPropKind kind;
|
||||
err = prop_kind(index, &kind);
|
||||
if (err)
|
||||
throw gspn_exeption(err);
|
||||
throw gspn_exeption("prop_kind()", err);
|
||||
|
||||
prop_dict[index] = ab_pair(kind, bdd_ithvar(var));
|
||||
}
|
||||
|
|
@ -97,7 +112,8 @@ namespace spot
|
|||
{
|
||||
const state_gspn* o = dynamic_cast<const state_gspn*>(other);
|
||||
assert(o);
|
||||
return o->get_state() - get_state();
|
||||
return reinterpret_cast<char*>(o->get_state())
|
||||
- reinterpret_cast<char*>(get_state());
|
||||
}
|
||||
|
||||
virtual state_gspn* clone() const
|
||||
|
|
@ -130,11 +146,9 @@ namespace spot
|
|||
current_(0),
|
||||
data_(data)
|
||||
{
|
||||
AtomicProp want[] = { EVENT_TRUE };
|
||||
int res = succ(state, want, sizeof(want) / sizeof(*want),
|
||||
&successors_, &size_);
|
||||
int res = succ(state, &successors_, &size_);
|
||||
if (res)
|
||||
throw res;
|
||||
throw gspn_exeption("succ()", res);
|
||||
assert(successors_);
|
||||
// GSPN is expected to return a looping "dead" transition where
|
||||
// there is no successor,
|
||||
|
|
@ -188,7 +202,7 @@ namespace spot
|
|||
private:
|
||||
bdd state_conds_; /// All conditions known on STATE.
|
||||
EventPropSucc* successors_; /// array of successors
|
||||
size_t size_; /// size of successors_
|
||||
size_t size_; /// size of successors_
|
||||
size_t current_; /// current position in successors_
|
||||
tgba_gspn_private_* data_;
|
||||
}; // tgba_succ_iterator_gspn
|
||||
|
|
@ -278,7 +292,7 @@ namespace spot
|
|||
State s;
|
||||
int err = initial_state(&s);
|
||||
if (err)
|
||||
throw gspn_exeption(err);
|
||||
throw gspn_exeption("initial_state()", err);
|
||||
return new state_gspn(s);
|
||||
}
|
||||
|
||||
|
|
@ -293,7 +307,7 @@ namespace spot
|
|||
int res = satisfy(s->get_state(),
|
||||
data_->all_indexes, &cube, data_->index_count);
|
||||
if (res)
|
||||
throw res;
|
||||
throw gspn_exeption("satisfy()", res);
|
||||
assert(cube);
|
||||
bdd state_conds = bddtrue;
|
||||
for (size_t i = 0; i < data_->index_count; ++i)
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
// Try not to include gspnlib.h here, or it will polute the user's
|
||||
// namespace with internal C symbols.
|
||||
|
||||
# include <iostream>
|
||||
# include <string>
|
||||
# include "tgba/tgba.hh"
|
||||
# include "ltlast/atomic_prop.hh"
|
||||
|
|
@ -12,24 +13,46 @@
|
|||
namespace spot
|
||||
{
|
||||
|
||||
class gspn_interface
|
||||
{
|
||||
public:
|
||||
gspn_interface(int argc, char **argv);
|
||||
~gspn_interface();
|
||||
tgba* get_automata();
|
||||
};
|
||||
|
||||
|
||||
/// An exeption used to forward GSPN errors.
|
||||
class gspn_exeption
|
||||
{
|
||||
public:
|
||||
gspn_exeption(int err)
|
||||
: err(err)
|
||||
gspn_exeption(const std::string& where, int err)
|
||||
: err_(err), where_(where)
|
||||
{
|
||||
}
|
||||
|
||||
int
|
||||
get_err() const
|
||||
{
|
||||
return err;
|
||||
return err_;
|
||||
}
|
||||
|
||||
std::string
|
||||
get_where() const
|
||||
{
|
||||
return where_;
|
||||
}
|
||||
|
||||
private:
|
||||
int err;
|
||||
int err_;
|
||||
std::string where_;
|
||||
};
|
||||
|
||||
std::ostream& operator<<(std::ostream& os, const gspn_exeption& e)
|
||||
{
|
||||
os << e.get_where() << " exited with " << e.get_err();
|
||||
return os;
|
||||
}
|
||||
|
||||
class gspn_environment : public ltl::environment
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,104 +0,0 @@
|
|||
#ifndef __GSPN_LIB_H__
|
||||
#define __GSPN_LIB_H__
|
||||
|
||||
/* Header file defining functions for Spot API */
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
/* -------------- Interface type definitions -------------- */
|
||||
|
||||
typedef unsigned long AtomicProp;
|
||||
typedef AtomicProp * pAtomicProp;
|
||||
typedef enum {STATE_PROP,EVENT_PROP} AtomicPropKind;
|
||||
typedef AtomicPropKind * pAtomicPropKind;
|
||||
|
||||
typedef unsigned long State;
|
||||
typedef State * pState;
|
||||
|
||||
typedef struct EventPropSucc {
|
||||
State s;
|
||||
AtomicProp p;
|
||||
} EventPropSucc;
|
||||
|
||||
#define EVENT_TRUE 0
|
||||
|
||||
|
||||
/* ----------------- Utility Functions --------------------*/
|
||||
|
||||
/* Initialize data structures to work with model and properties
|
||||
MANDATORY : should be called before any other function in this library
|
||||
Non 0 return correspond to errors in initialization
|
||||
Call with arguments similar to WNRG/WNSRG/WNERG
|
||||
*/
|
||||
int initialize (int argc, char **argv);
|
||||
/* Close and cleanup after using the library */
|
||||
int finalize (void);
|
||||
|
||||
|
||||
/* ----------------- Property related Functions ----------------*/
|
||||
|
||||
/* Returns the index of the property given as "name"
|
||||
Non zero return = error codes */
|
||||
int prop_index (const char * name, pAtomicProp propindex);
|
||||
|
||||
/* Returns the type of "prop" in "kind"
|
||||
non zero return = error codes
|
||||
*/
|
||||
int prop_kind (const AtomicProp prop, pAtomicPropKind kind);
|
||||
|
||||
|
||||
/* ------------------ State Space Exploration -----------------*/
|
||||
|
||||
/* Returns the identifier of the initial marking state */
|
||||
int initial_state (pState M0);
|
||||
|
||||
/* Given a state "s" and a list of "props_size" property indexes
|
||||
"props" checks the truth value of every atomic property in "props"
|
||||
and returns in "truth" the truth value of these properties in the
|
||||
same order as the input, ONE CHAR PER TRUTH VALUE
|
||||
(i.e. sizeof(truth[]) = props_size).
|
||||
|
||||
NB : the vector "truth" is allocated in this function
|
||||
*/
|
||||
int satisfy (const State s, const AtomicProp props [],
|
||||
unsigned char ** truth, size_t props_size);
|
||||
|
||||
/* free the "truth" vector allocated by satisfy
|
||||
!!! NB: Don't forget to call me, or you will get a memory leak !!!
|
||||
*/
|
||||
int satisfy_free (unsigned char * truth);
|
||||
|
||||
|
||||
/* Calculates successors of a state "s" that can be reached by
|
||||
verifying at least one event property specified in
|
||||
"enabled_events". In our first implementation enabled events is
|
||||
discarded, and ALL successors will be returned. This behavior is
|
||||
also obtained by giving "TRUE" in the list of enabled events. Each
|
||||
successor is returned in a struct that gives the Event property
|
||||
verified by the transition fired to reach this marking; If a
|
||||
marking is reached by firing a transition observed by more than one
|
||||
event property, it will be returned in many copies: i.e. E1 and E2
|
||||
observe different firngs of transition t1; M1 is reached from M0
|
||||
by firing t1 with a binding observable by both E1 and E2 : succ
|
||||
(M0, [E1,E2] , ...) will return {[M1,E1],[M1,E2]}
|
||||
|
||||
NB : "succ" vector is allocated in the function, use succ_free for
|
||||
memory release
|
||||
*/
|
||||
int succ (const State s,
|
||||
const AtomicProp enabled_events [], size_t enabled_events_size,
|
||||
EventPropSucc ** succ, size_t * succ_size);
|
||||
|
||||
/* free the "succ" vector allocated by succ
|
||||
!!! NB: Don't forget to call me, or you will get a memory leak !!!
|
||||
*/
|
||||
int succ_free (EventPropSucc * succ);
|
||||
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif /* __cplusplus */
|
||||
#endif /* __GSPN_LIB_H__ */
|
||||
Loading…
Add table
Add a link
Reference in a new issue