diff --git a/ChangeLog b/ChangeLog index 979871062..b2dd6e453 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2011-03-05 Alexandre Duret-Lutz + + Setup build system for a new dve2 interface. + + * iface/dve2/dve2.cc, iface/dve2/dve2.hh: New dummy files. + * iface/dve2/Makefile.am: New file. + * iface/Makefile.am (SUBDIRS): Add dve2. + * configure.ac: Build iface/dve2/Makefile. + * README: Mention the new directory. + 2011-03-05 Alexandre Duret-Lutz Using double borders for acceptance states in SBAs. diff --git a/README b/README index 6d19add82..8a7eb2f41 100644 --- a/README +++ b/README @@ -145,6 +145,7 @@ wrap/ Wrappers for other languages. cgi-bin/ Python-based CGI script (ltl-to-tgba translator) ajax/ Moderner LTL-to-TGBA translator, using Ajax. iface/ Interfaces to other libraries. + dve2/ Interface with DiVinE2. gspn/ GreatSPN interface. examples/ Supporting models used by the test cases. nips/ NIPS interface (to use Promela models). diff --git a/configure.ac b/configure.ac index 56d5e8066..7d4403158 100644 --- a/configure.ac +++ b/configure.ac @@ -96,6 +96,7 @@ AC_CONFIG_FILES([ bench/wdba/defs doc/Doxyfile doc/Makefile + iface/dve2/Makefile iface/gspn/defs iface/gspn/Makefile iface/Makefile @@ -139,7 +140,7 @@ AC_CONFIG_FILES([ wrap/python/tests/Makefile ]) AC_CONFIG_FILES([bench/ltl2tgba/ltl2baw.pl:bench/ltl2tgba/ltl2baw.in], - [chmod +x bench/ltl2tgba/ltl2baw.pl]) + [chmod +x bench/ltl2tgba/ltl2baw.pl]) AC_CONFIG_FILES([doc/dot], [chmod +x doc/dot]) AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run]) AC_OUTPUT diff --git a/iface/Makefile.am b/iface/Makefile.am index 446180654..982417a32 100644 --- a/iface/Makefile.am +++ b/iface/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2008 Laboratoire de Recherche et Développement +## Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -21,7 +21,7 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -SUBDIRS = nips +SUBDIRS = nips dve2 if WITH_GSPN SUBDIRS += gspn diff --git a/iface/dve2/Makefile.am b/iface/dve2/Makefile.am new file mode 100644 index 000000000..9b74ddab9 --- /dev/null +++ b/iface/dve2/Makefile.am @@ -0,0 +1,30 @@ +## Copyright (C) 2011 Laboratoire de Recherche et Developpement 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 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$(top_srcdir)/src $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +dve2dir = $(pkgincludedir)/iface/dve2 + +dve2_HEADERS = dve2.hh + +lib_LTLIBRARIES = libspotdve2.la +libspotdve2_la_LIBADD = $(top_builddir)/src/libspot.la +libspotdve2_la_SOURCES = dve2.cc diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc new file mode 100644 index 000000000..fdce4e936 --- /dev/null +++ b/iface/dve2/dve2.cc @@ -0,0 +1,30 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement 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 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 "dve2.hh" + +namespace spot +{ + kripke* load_dve2(const std::string& file) + { + (void) file; + return 0; + } +} diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh new file mode 100644 index 000000000..a25f9977e --- /dev/null +++ b/iface/dve2/dve2.hh @@ -0,0 +1,31 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement +// 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 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_IFACE_DVE2_DVE2_HH +# define SPOT_IFACE_DVE2_DVE2_HH + +#include "kripke/kripke.hh" + +namespace spot +{ + kripke* load_dve2(const std::string& file); +} + +#endif // SPOT_IFACE_DVE2_DVE2_HH