diff --git a/README b/README index a5a87d5e8..b6d127ee5 100644 --- a/README +++ b/README @@ -61,16 +61,6 @@ should read the file INSTALL for generic instructions. In addition to its usual options, ./configure will accept some flags specific to Spot: - --with-gspn=DIR - Turns on GreatSPN support. DIR should designate the root of - GreatSPN source tree. (./configure will then run - DIR/SOURCES/contrib/version.sh to find the GreatSPN build tree.) - - GreatSPN had to be modified in order to be used as a library - (thanks Soheib Baarir and Yann Thierry-Mieg for this work), and - presently these modifications are only available on the GreatSPN - CVS repository hosted by the Università di Torino. - --with-included-buddy After you have installed Spot the first time, a modified version of BuDDy will be installed. The next time you reconfigure Spot, @@ -201,8 +191,6 @@ wrap/ Wrappers for other languages. ajax/ LTL-to-TGBA translator with web interface, using Ajax. iface/ Interfaces to other libraries. dve2/ Interface with DiVinE2. - gspn/ GreatSPN interface. - examples/ Supporting models used by the test cases. Third party software -------------------- diff --git a/configure.ac b/configure.ac index d296b0aa6..690129e36 100644 --- a/configure.ac +++ b/configure.ac @@ -107,7 +107,6 @@ if ! "${stdpass-false}"; then fi AX_CHECK_BUDDY -AX_CHECK_GSPNLIB AC_CHECK_HEADERS([sys/times.h]) AC_CHECK_FUNCS([times kill alarm]) @@ -173,8 +172,6 @@ AC_CONFIG_FILES([ doc/org/init.el iface/dve2/defs iface/dve2/Makefile - iface/gspn/defs - iface/gspn/Makefile iface/Makefile lib/Makefile src/bin/Makefile diff --git a/iface/Makefile.am b/iface/Makefile.am index c5f5346a4..743d3e53a 100644 --- a/iface/Makefile.am +++ b/iface/Makefile.am @@ -1,8 +1,6 @@ -## Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement +## -*- coding: utf-8 -*- +## Copyright (C) 2011, 2014 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 -## et Marie Curie. ## ## This file is part of Spot, a model checking library. ## @@ -20,7 +18,3 @@ ## along with this program. If not, see . SUBDIRS = dve2 - -if WITH_GSPN - SUBDIRS += gspn -endif diff --git a/iface/gspn/.cvsignore b/iface/gspn/.cvsignore deleted file mode 100644 index 9b1222407..000000000 --- a/iface/gspn/.cvsignore +++ /dev/null @@ -1,8 +0,0 @@ -Makefile.in -Makefile -*.lo -*.o -*.la -.deps -.libs -defs diff --git a/iface/gspn/.gitignore b/iface/gspn/.gitignore deleted file mode 100644 index 02de6c55d..000000000 --- a/iface/gspn/.gitignore +++ /dev/null @@ -1,15 +0,0 @@ -Makefile.in -Makefile -*.lo -*.o -*.la -.deps -.libs -defs -dottygspn-rg -dottygspn-srg -dottygspn-ssp -ltlgspn-rg -ltlgspn-srg -ltlgspn-ssp -testSubDir diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am deleted file mode 100644 index d8e5861d5..000000000 --- a/iface/gspn/Makefile.am +++ /dev/null @@ -1,103 +0,0 @@ -## Copyright (C) 2008 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). -## Copyright (C) 2003, 2004 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 . - -AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) $(LIBGSPN_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -gspndir = $(pkgincludedir)/iface/gspn - -gspn_HEADERS = \ - common.hh \ - gspn.hh - -lib_LTLIBRARIES = libspotgspn.la libspotgspnssp.la -libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la -libspotgspn_la_SOURCES = \ - common.cc \ - gspn.cc - -noinst_PROGRAMS = \ - dottygspn-rg \ - dottygspn-srg \ - ltlgspn-rg \ - ltlgspn-srg - -if WITH_GSPN_SSP -gspn_HEADERS += ssp.hh -noinst_PROGRAMS += \ - dottygspn-ssp \ - ltlgspn-ssp - -libspotgspnssp_la_LIBADD = $(top_builddir)/src/libspot.la -libspotgspnssp_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS) -libspotgspnssp_la_SOURCES = \ - common.cc \ - ssp.cc -endif - - -dottygspn_rg_SOURCES = dottygspn.cc -dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) - -dottygspn_srg_SOURCES = dottygspn.cc -dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) - -dottygspn_ssp_SOURCES = dottyssp.cc -dottygspn_ssp_LDADD = libspotgspnssp.la $(LIBGSPNSSP_LDFLAGS) - -ltlgspn_rg_SOURCES = ltlgspn.cc -ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) - -ltlgspn_srg_SOURCES = ltlgspn.cc -ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) - -ltlgspn_ssp_SOURCES = ltlgspn.cc -ltlgspn_ssp_LDADD = libspotgspnssp.la $(LIBGSPNSSP_LDFLAGS) -ltlgspn_ssp_CPPFLAGS = -DSSP=1 $(AM_CPPFLAGS) - -EXTRA_DIST = \ - examples/DCSwave/DCSWave.def \ - examples/DCSwave/DCSWave.net \ - examples/DCSwave/DCSWave.tobs \ - examples/simple/simple.def \ - examples/simple/simple.net \ - examples/simple/simple.tobs \ - examples/udcs/udcs.def \ - examples/udcs/udcs.net \ - examples/udcs/udcs.tobs \ - $(TESTS) - -TESTS = \ - simple.test \ - dcswave.test \ - dcswaveltl.test \ - dcswavefm.test \ - dcswaveeltl.test \ - udcsltl.test \ - udcseltl.test \ - udcsfm.test \ - udcsefm.test - -# Each test case depends on defs. -check_SCRIPTS = defs - -distclean-local: - -rm -rf testSubDir diff --git a/iface/gspn/common.cc b/iface/gspn/common.cc deleted file mode 100644 index 8f2dd033f..000000000 --- a/iface/gspn/common.cc +++ /dev/null @@ -1,33 +0,0 @@ -// 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 . - -#include "common.hh" -#include - -namespace spot -{ - - std::ostream& - operator<<(std::ostream& os, const gspn_exception& e) - { - os << e.get_where() << " exited with " << e.get_err(); - return os; - } - -} diff --git a/iface/gspn/common.hh b/iface/gspn/common.hh deleted file mode 100644 index 45ce9c95b..000000000 --- a/iface/gspn/common.hh +++ /dev/null @@ -1,61 +0,0 @@ -// 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 . - -#ifndef SPOT_IFACE_GSPN_COMMON_HH -# define SPOT_IFACE_GSPN_COMMON_HH - -# include -# include - -// Do not include gspnlib.h here, or it will polute the user's -// namespace with internal C symbols. - -namespace spot -{ - - /// An exception used to forward GSPN errors. - class gspn_exception - { - public: - gspn_exception(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_exception& e); -} - -#endif // SPOT_IFACE_GSPN_COMMON_HH diff --git a/iface/gspn/dcswave.test b/iface/gspn/dcswave.test deleted file mode 100755 index 20319ecc9..000000000 --- a/iface/gspn/dcswave.test +++ /dev/null @@ -1,32 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/DCSwave . -chmod +w DCSwave - -# Run this if you want, it builds approximately 3,600,000 states. -# ../dottygspn-rg DCSwave/DCSWave ATTiIDLj SCi SCj >output - -# Only 5,579 states. -../dottygspn-srg DCSwave/DCSWave ATTiIDLj SCi SCj >output diff --git a/iface/gspn/dcswaveeltl.test b/iface/gspn/dcswaveeltl.test deleted file mode 100755 index 11c3d4c5a..000000000 --- a/iface/gspn/dcswaveeltl.test +++ /dev/null @@ -1,40 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/DCSwave . -chmod +w DCSwave - -# G(ATTiIDLj => F(!SCj U SCi)) is true -../ltlgspn-srg -c -l -e DCSwave/DCSWave \ - '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj >output -../ltlgspn-srg -c -f -e2 DCSwave/DCSWave \ - '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj >output - -# G(F(!SCj U SCi)) is false -../ltlgspn-srg -c -l -e DCSwave/DCSWave \ - '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output && exit 1 -../ltlgspn-srg -c -f -e2 DCSwave/DCSWave \ - '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output && exit 1 - -: diff --git a/iface/gspn/dcswavefm.test b/iface/gspn/dcswavefm.test deleted file mode 100755 index 8677bdcc1..000000000 --- a/iface/gspn/dcswavefm.test +++ /dev/null @@ -1,36 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/DCSwave . -chmod +w DCSwave - -# G(ATTiIDLj => F(!SCj U SCi)) is true -../ltlgspn-srg -c -f -m DCSwave/DCSWave \ - '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj >output - -# G(F(!SCj U SCi)) is false -../ltlgspn-srg -c -f -m DCSwave/DCSWave \ - '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output && exit 1 - -: diff --git a/iface/gspn/dcswaveltl.test b/iface/gspn/dcswaveltl.test deleted file mode 100755 index a93d3813b..000000000 --- a/iface/gspn/dcswaveltl.test +++ /dev/null @@ -1,36 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/DCSwave . -chmod +w DCSwave - -# G(ATTiIDLj => F(!SCj U SCi)) is true -../ltlgspn-srg -c -l -m DCSwave/DCSWave \ - '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj >output - -# G(F(!SCj U SCi)) is false -../ltlgspn-srg -c -l -m DCSwave/DCSWave \ - '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj >output && exit 1 - -: diff --git a/iface/gspn/defs.in b/iface/gspn/defs.in deleted file mode 100644 index c2dd7b4ec..000000000 --- a/iface/gspn/defs.in +++ /dev/null @@ -1,53 +0,0 @@ -# -*- shell-script -*- - -# 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 - -# Always use an absolute srcdir. Otherwise symlinks made in subdirs -# of the test dir just won't work. -case "$srcdir" in - [\\/]* | ?:[\\/]*) - ;; - - *) - srcdir=`CDPATH=: && cd "$srcdir" && pwd` - ;; -esac - -# Ensure $srcdir is set correctly. -test -f $srcdir/defs.in || { - echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 - exit 1 -} - -# User can set VERBOSE to see all output. -test -z "$VERBOSE" && exec >/dev/null 2>&1 - -DOT='@DOT@' - - -# Create a test subdirectory. - -chmod -R a+rwx testSubDir > /dev/null 2>&1 -rm -rf testSubDir > /dev/null 2>&1 -mkdir testSubDir -cd testSubDir - -echo "== Running test $0" - -# Turn on shell traces when VERBOSE=x. -if test "x$VERBOSE" = xx; then - set -x -else - : -fi diff --git a/iface/gspn/dottygspn.cc b/iface/gspn/dottygspn.cc deleted file mode 100644 index 983d400b7..000000000 --- a/iface/gspn/dottygspn.cc +++ /dev/null @@ -1,54 +0,0 @@ -// 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 . - -#include "gspn.hh" -#include "tgbaalgos/dotty.hh" - -int -main(int argc, char **argv) - try - { - spot::ltl::declarative_environment env; - - if (argc <= 2) - { - std::cerr << "usage: " << argv[0] << " model props..." << std::endl; - exit(1); - } - - while (argc > 2) - { - env.declare(argv[argc - 1]); - --argc; - } - - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::gspn_interface gspn(2, argv, dict, env); - spot::tgba* a = gspn.automaton(); - - spot::dotty_reachable(std::cout, a); - - delete a; - delete dict; - } - catch (spot::gspn_exception e) - { - std::cerr << e << std::endl; - throw; - } diff --git a/iface/gspn/dottyssp.cc b/iface/gspn/dottyssp.cc deleted file mode 100644 index 2a6277cba..000000000 --- a/iface/gspn/dottyssp.cc +++ /dev/null @@ -1,61 +0,0 @@ -// 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 . - -#include "ssp.hh" -#include "tgbaalgos/dotty.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaparse/public.hh" - -int -main(int argc, char **argv) - try - { - spot::ltl::declarative_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::bdd_dict* dict = new spot::bdd_dict(); - spot::gspn_ssp_interface gspn(2, argv, dict, env); - - 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, argv[argc], pel1)) - return 2; - - spot::tgba* a = gspn.automaton(control); - spot::dotty_reachable(std::cout, a); - - delete a; - delete control; - delete dict; - } - catch (spot::gspn_exception e) - { - std::cerr << e << std::endl; - throw; - } diff --git a/iface/gspn/examples/DCSwave/DCSWave.def b/iface/gspn/examples/DCSwave/DCSWave.def deleted file mode 100644 index 82f7d172d..000000000 --- a/iface/gspn/examples/DCSwave/DCSWave.def +++ /dev/null @@ -1,66 +0,0 @@ -|256 -% -| -(proc c 1.0 1.0 (@c -u proc_0,proc_1,proc_2 -)) -(proc_0 c 1.0 1.0 (@c -proc{1-1} -)) -(proc_1 c 1.0 1.0 (@c -proc{2-2} -)) -(proc_2 c 1.0 1.0 (@c -proc{3-10} -)) -(M_Idle m 1.0 1.0 (@m - + + -)) -(F5 f 1.0 1.0 (@f -

-)) -(F6 f 1.0 1.0 (@f -

-)) -(F7 f 1.0 1.0 (@f -

-)) -(F8 f 1.0 1.0 (@f -

-)) -(F9 f 1.0 1.0 (@f -

-)) -(F10 f 1.0 1.0 (@f -

-)) -(F11 f 1.0 1.0 (@f -++ -)) -(F12 f 1.0 1.0 (@f -

-)) -(F13 f 1.0 1.0 (@f -

-)) -(F14 f 1.0 1.0 (@f -

-)) -(F15 f 1.0 1.0 (@f -

-)) -(F16 f 1.0 1.0 (@f -++ -)) -(F17 f 1.0 1.0 (@f - -)) -(F18 f 1.0 1.0 (@f - -)) -(F19 f 1.0 1.0 (@f - -)) -(F20 f 1.0 1.0 (@f - -)) diff --git a/iface/gspn/examples/DCSwave/DCSWave.net b/iface/gspn/examples/DCSwave/DCSWave.net deleted file mode 100644 index b9855fe0a..000000000 --- a/iface/gspn/examples/DCSwave/DCSWave.net +++ /dev/null @@ -1,38 +0,0 @@ -|0| -| -f 0 6 0 5 0 0 0 -Idle -10005 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -SC 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Dem 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -inWave 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Att 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -mutex 1 1.0 1.0 1.0 1.0 0 -t3 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 4 0 0 1.0 1.0 F7 - 1 - 1 5 0 0 1.0 1.0 F8 - 0 -t4 1.0 1 0 2 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 5 0 0 1.0 1.0 F9 - 1 6 0 0 - 1 - 1 2 0 0 1.0 1.0 F10 - 1 - 1 4 0 0 1.0 1.0 F11 -t1 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 1 0 0 1.0 1.0 F5 - 1 - 1 3 0 0 1.0 1.0 F6 - 0 -t2 1.0 1 1 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 3 0 0 1.0 1.0 F14 - 1 - 1 4 0 0 1.0 1.0 F15 - 1 - 1 5 0 0 1.0 1.0 F16 -t5 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 F12 - 2 - 1 1 0 0 1.0 1.0 F13 - 1 6 0 0 - 0 diff --git a/iface/gspn/examples/DCSwave/DCSWave.tobs b/iface/gspn/examples/DCSwave/DCSWave.tobs deleted file mode 100644 index 5eadc5431..000000000 --- a/iface/gspn/examples/DCSwave/DCSWave.tobs +++ /dev/null @@ -1,14 +0,0 @@ -3 -ATTiIDLj 1.0 1 0 2 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 1 0 0 1.0 1.0 - 1 5 0 0 1.0 1.0 - 0 - 0 -SCj 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 - 0 - 0 -SCi 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 - 0 - 0 \ No newline at end of file diff --git a/iface/gspn/examples/simple/.cvsignore b/iface/gspn/examples/simple/.cvsignore deleted file mode 100644 index 1f2ec0b48..000000000 --- a/iface/gspn/examples/simple/.cvsignore +++ /dev/null @@ -1,9 +0,0 @@ -simple.cap -simple.cc -simple.mark -simple.minval -simple.outtype -simple.parse -simple.sc -simple.string -simple.val diff --git a/iface/gspn/examples/simple/.gitignore b/iface/gspn/examples/simple/.gitignore deleted file mode 100644 index 1f2ec0b48..000000000 --- a/iface/gspn/examples/simple/.gitignore +++ /dev/null @@ -1,9 +0,0 @@ -simple.cap -simple.cc -simple.mark -simple.minval -simple.outtype -simple.parse -simple.sc -simple.string -simple.val diff --git a/iface/gspn/examples/simple/simple.def b/iface/gspn/examples/simple/simple.def deleted file mode 100644 index 6f63f89d2..000000000 --- a/iface/gspn/examples/simple/simple.def +++ /dev/null @@ -1,30 +0,0 @@ -|256 -% -| -(C c 1.0 1.0 (@c -u C_0 -)) -(C_0 c 1.0 1.0 (@c -num{1-10} -)) -(M_a m 1.0 1.0 (@m - -)) -(F3 f 1.0 1.0 (@f - -)) -(F4 f 1.0 1.0 (@f - -)) -(F5 f 1.0 1.0 (@f - -)) -(F6 f 1.0 1.0 (@f - -)) -(F7 f 1.0 1.0 (@f - -)) -(F8 f 1.0 1.0 (@f - -)) diff --git a/iface/gspn/examples/simple/simple.net b/iface/gspn/examples/simple/simple.net deleted file mode 100644 index dc1f1deee..000000000 --- a/iface/gspn/examples/simple/simple.net +++ /dev/null @@ -1,15 +0,0 @@ -|0| -| -f 0 2 0 2 0 0 0 -a -10003 1.0 1.0 1.0 1.0 0 1.0 1.0 C -b 0 1.0 1.0 1.0 1.0 0 1.0 1.0 C -x 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 1 0 0 1.0 1.0 F3 - 1 - 1 2 0 0 1.0 1.0 F4 - 0 -y 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 F5 - 1 - 1 1 0 0 1.0 1.0 F6 - 0 diff --git a/iface/gspn/examples/simple/simple.tobs b/iface/gspn/examples/simple/simple.tobs deleted file mode 100644 index 2ac82ed52..000000000 --- a/iface/gspn/examples/simple/simple.tobs +++ /dev/null @@ -1,5 +0,0 @@ -1 -obs 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 1 0 0 1.0 1.0 - 0 - 0 diff --git a/iface/gspn/examples/udcs/udcs.def b/iface/gspn/examples/udcs/udcs.def deleted file mode 100644 index 5bf74dd90..000000000 --- a/iface/gspn/examples/udcs/udcs.def +++ /dev/null @@ -1,78 +0,0 @@ -|256 -% -| -(proc c 1.0 1.0 (@c -u proc_0,proc_1 -)) -(proc_0 c 1.0 1.0 (@c -p{1-1} -)) -(proc_1 c 1.0 1.0 (@c -p{2-3} -)) -(M_Id m 1.0 1.0 (@m - + -)) -(F4 f 1.0o 1.0 (@f - -)) -(F5 f 1.0 1.0 (@f - -)) -(F6 f 1.0 1.0 (@f -

-)) -(F7 f 1.0 1.0 (@f -

-)) -(F8 f 1.0 1.0 (@f -

-)) -(F9 f 1.0 1.0 (@f -

-)) -(F10 f 1.0 1.0 (@f -

-)) -(F11 f 1.0 1.0 (@f -

-)) -(F12 f 1.0 1.0 (@f -+-

-)) -(F13 f 1.0 1.0 (@f -

-)) -(F14 f 1.0 1.0 (@f -

+ -)) -(F15 f 1.0 1.0 (@f - -)) -(F16 f 1.0 1.0 (@f -

-)) -(F17 f 1.0 1.0 (@f - -)) -(F18 f 1.0 1.0 (@f -

-)) -(F19 f 1.0 1.0 (@f -

-)) -(F20 f 1.0 1.0 (@f -+ -)) -(F21 f 1.0 1.0 (@f -

-)) -(F22 f 1.0 1.0 (@f - -)) -(F23 f 1.0 1.0 (@f - -)) -(F24 f 1.0 1.0 (@f -

-)) diff --git a/iface/gspn/examples/udcs/udcs.net b/iface/gspn/examples/udcs/udcs.net deleted file mode 100644 index 90922624e..000000000 --- a/iface/gspn/examples/udcs/udcs.net +++ /dev/null @@ -1,46 +0,0 @@ -|0| -| -f 0 6 0 6 0 0 0 -Id -10004 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Re 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Tr 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Gs 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Aut -10004 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -Fdr 0 1.0 1.0 1.0 1.0 0 1.0 1.0 proc -t3 1.0 1 0 2 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 3 0 0 1.0 1.0 F11 - 1 6 0 0 1.0 1.0 F12 - 1 - 1 4 0 0 1.0 1.0 F13 - 0 -t4 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 3 0 0 1.0 1.0 F14 - 3 - 1 1 0 0 1.0 1.0 F15 - 1 3 0 0 1.0 1.0 F16 - 1 6 0 0 1.0 1.0 F17 - 0 -t1 1.0 1 0 2 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 1 0 0 1.0 1.0 F6 - 1 5 0 0 1.0 1.0 F7 - 1 - 1 2 0 0 1.0 1.0 F8 - 0 -t2 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 F9 - 1 - 1 3 0 0 1.0 1.0 F10 - 0 -t6 1.0 1 1 2 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 3 0 0 1.0 1.0 F21 - 1 5 0 0 1.0 1.0 F22 - 2 - 1 6 0 0 1.0 1.0 F23 - 1 3 0 0 1.0 1.0 F24 - 0 -t5 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 4 0 0 1.0 1.0 F18 - 2 - 1 1 0 0 1.0 1.0 F19 - 1 5 0 0 1.0 1.0 F20 - 0 diff --git a/iface/gspn/examples/udcs/udcs.tobs b/iface/gspn/examples/udcs/udcs.tobs deleted file mode 100644 index 666e34ee3..000000000 --- a/iface/gspn/examples/udcs/udcs.tobs +++ /dev/null @@ -1,9 +0,0 @@ -2 -ReP1 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 2 0 0 1.0 1.0 - 0 - 0 -gsP1 1.0 1 0 1 0 1.0 1.0 1.0 1.0 1.0 1.0 0 - 1 4 0 0 1.0 1.0 - 0 - 0 diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc deleted file mode 100644 index 6ff1089be..000000000 --- a/iface/gspn/gspn.cc +++ /dev/null @@ -1,493 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006, 2007 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 . - -#include -#include -#include -#include "gspn.hh" -#include - -namespace spot -{ - - namespace - { - // state_gspn - ////////////////////////////////////////////////////////////////////// - - class state_gspn: public state - { - public: - state_gspn(State s) - : state_(s) - { - } - - virtual - ~state_gspn() - { - } - - virtual int - compare(const state* other) const - { - const state_gspn* o = down_cast(other); - assert(o); - return reinterpret_cast(o->get_state()) - - reinterpret_cast(get_state()); - } - - virtual size_t - hash() const - { - return reinterpret_cast(get_state()) - static_cast(0); - } - - virtual state_gspn* clone() const - { - return new state_gspn(get_state()); - } - - State - get_state() const - { - return state_; - } - - private: - State state_; - }; // state_gspn - - - // tgba_gspn_private_ - ////////////////////////////////////////////////////////////////////// - - struct tgba_gspn_private_ - { - int refs; // reference count - - bdd_dict* dict; - typedef std::pair ab_pair; - typedef std::map prop_map; - prop_map prop_dict; - AtomicProp *all_indexes; - size_t index_count; - const state_gspn* last_state_conds_input; - bdd last_state_conds_output; - bdd alive_prop; - bdd dead_prop; - - tgba_gspn_private_(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead) - : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) - { - const ltl::declarative_environment::prop_map& p = env.get_prop_map(); - - try - { - for (ltl::declarative_environment::prop_map::const_iterator i - = p.begin(); i != p.end(); ++i) - { - // Skip the DEAD proposition, GreatSPN knows nothing - // about it. - if (i->first == dead) - continue; - - int var = dict->register_proposition(i->second, this); - AtomicProp index; - int err = prop_index(i->first.c_str(), &index); - if (err) - throw gspn_exception("prop_index(" + i->first + ")", err); - AtomicPropKind kind; - err = prop_kind(index, &kind); - if (err) - throw gspn_exception("prop_kind(" + i->first + ")", err); - - prop_dict[index] = ab_pair(kind, bdd_ithvar(var)); - } - - index_count = prop_dict.size(); - all_indexes = new AtomicProp[index_count]; - - unsigned idx = 0; - for (prop_map::const_iterator i = prop_dict.begin(); - i != prop_dict.end(); ++i) - all_indexes[idx++] = i->first; - } - 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; - } - - // Register the "dead" proposition. There are three cases to - // consider: - // * If DEAD is "false", it means we are not interested in finite - // sequences of the system. - // * If DEAD is "true", we want to check finite sequences as well - // as infinite sequences, but do not need to distinguish them. - // * If DEAD is any other string, this is the name a property - // that should be true when looping on a dead state, and false - // otherwise. - // We handle these three cases by setting ALIVE_PROP and DEAD_PROP - // appropriately. ALIVE_PROP is the bdd that should be ANDed - // to all transitions leaving a live state, while DEAD_PROP should - // be ANDed to all transitions leaving a dead state. - if (!strcasecmp(dead.c_str(), "false")) - { - alive_prop = bddtrue; - dead_prop = bddfalse; - } - else if (!strcasecmp(dead.c_str(), "true")) - { - alive_prop = bddtrue; - dead_prop = bddtrue; - } - else - { - ltl::formula* f = env.require(dead); - assert(f); - int var = dict->register_proposition(f, this); - dead_prop = bdd_ithvar(var); - alive_prop = bdd_nithvar(var); - } - } - - ~tgba_gspn_private_() - { - dict->unregister_all_my_variables(this); - delete last_state_conds_input; - delete[] all_indexes; - } - - bdd index_to_bdd(AtomicProp index) const - { - if (index == EVENT_TRUE) - return bddtrue; - prop_map::const_iterator i = prop_dict.find(index); - assert(i != prop_dict.end()); - return i->second.second; - } - - bdd state_conds(const state_gspn* s) - { - // Use cached value if possible. - if (!last_state_conds_input || - last_state_conds_input->compare(s) != 0) - { - // Build the BDD of the conditions available on this state. - unsigned char* cube = 0; - // FIXME: This is temporary. We ought to ask only what we need. - AtomicProp* want = all_indexes; - size_t count = index_count; - int res = satisfy(s->get_state(), want, &cube, count); - if (res) - throw gspn_exception("satisfy()", res); - assert(cube); - last_state_conds_output = bddtrue; - for (size_t i = 0; i < count; ++i) - { - bdd v = index_to_bdd(want[i]); - last_state_conds_output &= cube[i] ? v : !v; - } - satisfy_free(cube); - - delete last_state_conds_input; - last_state_conds_input = s->clone(); - } - return last_state_conds_output; - } - }; - - - // tgba_succ_iterator_gspn - ////////////////////////////////////////////////////////////////////// - - class tgba_succ_iterator_gspn: public tgba_succ_iterator - { - public: - tgba_succ_iterator_gspn(bdd state_conds, State state, - tgba_gspn_private_* data) - : state_conds_(state_conds), - successors_(0), - size_(0), - current_(0), - data_(data), - from_state_(state) - { - int res = succ(state, &successors_, &size_); - if (res) - throw gspn_exception("succ()", res); - // GreatSPN should return successors_ == 0 and size_ == 0 when a - // state has no successors. - assert((size_ <= 0) ^ (successors_ != 0)); - // If we have to stutter on a dead state, we have one successor. - if (size_ <= 0 && data_->dead_prop != bddfalse) - size_ = 1; - } - - virtual - ~tgba_succ_iterator_gspn() - { - if (successors_) - succ_free(successors_); - } - - virtual void - first() - { - current_ = 0; - } - - virtual void - next() - { - assert(!done()); - ++current_; - } - - virtual bool - done() const - { - return current_ >= size_; - } - - virtual state* - current_state() const - { - // If GreatSPN returned no successor, we stutter on the dead state. - return - new state_gspn(successors_ ? successors_[current_].s : from_state_); - } - - virtual bdd - current_condition() const - { - if (successors_) - { - bdd p = data_->index_to_bdd(successors_[current_].p); - return state_conds_ & p & data_->alive_prop; - } - else - { - return state_conds_ & data_->dead_prop; - } - } - - virtual bdd - current_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems. - return bddfalse; - } - private: - bdd state_conds_; /// All conditions known on STATE. - EventPropSucc* successors_; /// array of successors - size_t size_; /// size of successors_ - size_t current_; /// current position in successors_ - tgba_gspn_private_* data_; - State from_state_; - }; // tgba_succ_iterator_gspn - - - // tgba_gspn - ////////////////////////////////////////////////////////////////////// - - - - - /// Data private to tgba_gspn. - struct tgba_gspn_private_; - - class tgba_gspn: public tgba - { - public: - tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead); - tgba_gspn(const tgba_gspn& other); - tgba_gspn& operator=(const tgba_gspn& other); - virtual ~tgba_gspn(); - virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; - virtual bdd_dict* get_dict() const; - virtual std::string format_state(const state* state) const; - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - protected: - virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; - private: - tgba_gspn_private_* data_; - }; - - - tgba_gspn::tgba_gspn(bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead) - { - data_ = new tgba_gspn_private_(dict, env, dead); - } - - tgba_gspn::tgba_gspn(const tgba_gspn& other) - : tgba() - { - data_ = other.data_; - ++data_->refs; - } - - tgba_gspn::~tgba_gspn() - { - if (--data_->refs == 0) - delete data_; - } - - tgba_gspn& - tgba_gspn::operator=(const tgba_gspn& other) - { - if (&other == this) - return *this; - this->~tgba_gspn(); - new (this) tgba_gspn(other); - return *this; - } - - state* tgba_gspn::get_init_state() const - { - State s; - int err = initial_state(&s); - if (err) - throw gspn_exception("initial_state()", err); - return new state_gspn(s); - } - - tgba_succ_iterator* - tgba_gspn::succ_iter(const state* local_state, - const state* global_state, - const tgba* global_automaton) const - { - const state_gspn* s = down_cast(local_state); - assert(s); - (void) global_state; - (void) global_automaton; - // FIXME: Should pass global_automaton->support_variables(state) - // to state_conds. - bdd state_conds = data_->state_conds(s); - return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_); - } - - bdd - tgba_gspn::compute_support_conditions(const spot::state* state) const - { - const state_gspn* s = down_cast(state); - assert(s); - return data_->state_conds(s); - } - - bdd - tgba_gspn::compute_support_variables(const spot::state* state) const - { - // FIXME: At the time of writing, only tgba_gspn calls - // support_variables on the root of a product to gather the - // variables used by all other automata and let GPSN compute only - // these. Because support_variables() is recursive over the - // product treee, tgba_gspn::support_variables should not output - // all the variables known by GSPN; this would ruin the sole - // purpose of this function. - // However this works because we assume there is at most one - // tgba_gspn automata in a product (a legitimate assumption - // since the GSPN API is not re-entrant) and only this automata - // need to call support_variables (now _this_ is shady). - (void) state; - return bddtrue; - } - - bdd_dict* - tgba_gspn::get_dict() const - { - return data_->dict; - } - - std::string - tgba_gspn::format_state(const state* state) const - { - const state_gspn* s = down_cast(state); - assert(s); - char* str; - int err = print_state(s->get_state(), &str); - if (err) - throw gspn_exception("print_state()", err); - // Strip trailing \n... - unsigned len = strlen(str); - while (str[--len] == '\n') - str[len] = 0; - std::string res(str); - free(str); - return res; - } - - bdd - tgba_gspn::all_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems. - return bddfalse; - } - - bdd - tgba_gspn::neg_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems. - return bddtrue; - } - - } // anonymous - - // gspn_interface - ////////////////////////////////////////////////////////////////////// - - gspn_interface::gspn_interface(int argc, char **argv, - bdd_dict* dict, - ltl::declarative_environment& env, - const std::string& dead) - : dict_(dict), env_(env), dead_(dead) - { - int res = initialize(argc, argv); - if (res) - throw gspn_exception("initialize()", res); - } - - gspn_interface::~gspn_interface() - { - int res = finalize(); - if (res) - throw gspn_exception("finalize()", res); - } - - tgba* - gspn_interface::automaton() const - { - return new tgba_gspn(dict_, env_, dead_); - } - -} diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh deleted file mode 100644 index 76754d97e..000000000 --- a/iface/gspn/gspn.hh +++ /dev/null @@ -1,49 +0,0 @@ -// Copyright (C) 2003, 2004 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 . - -#ifndef SPOT_IFACE_GSPN_GSPN_HH -# define SPOT_IFACE_GSPN_GSPN_HH - -// Do not include gspnlib.h here, or it will polute the user's -// namespace with internal C symbols. - -# include -# include "tgba/tgba.hh" -# include "common.hh" -# include "ltlenv/declenv.hh" - -namespace spot -{ - - class gspn_interface - { - public: - gspn_interface(int argc, char **argv, - bdd_dict* dict, ltl::declarative_environment& env, - const std::string& dead = "true"); - ~gspn_interface(); - tgba* automaton() const; - private: - bdd_dict* dict_; - ltl::declarative_environment& env_; - const std::string dead_; - }; -} - -#endif // SPOT_IFACE_GSPN_GSPN_HH diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc deleted file mode 100644 index 47c9bbdbf..000000000 --- a/iface/gspn/ltlgspn.cc +++ /dev/null @@ -1,430 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE) -// Copyright (C) 2003, 2004, 2006, 2007 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 . - -#ifndef SSP -#include "gspn.hh" -#define MIN_ARG 3 -#else -#include "ssp.hh" -#define MIN_ARG 4 -#include "tgba/tgbaexplicit.hh" -#include "tgbaparse/public.hh" -#endif -#include "ltlparse/public.hh" -#include "tgba/tgbatba.hh" -#include "tgba/tgbaproduct.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgbaalgos/magic.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/gtec/ce.hh" -#include "tgbaalgos/projrun.hh" - - -void -syntax(char* prog) -{ - std::cerr << "Usage: "<< prog -#ifndef SSP - << " [OPTIONS...] model formula props..." << std::endl -#else - << " [OPTIONS...] model formula automata props..." << std::endl -#endif - << std::endl -#ifdef SSP - << " -1 do not use a double hash (for inclusion check)" - << std::endl - << " -L use LIFO ordering for inclusion check" - << std::endl -#endif - << " -c compute an example" << std::endl - << " (instead of just checking for emptiness)" << std::endl - << std::endl -#ifndef SSP - << " -d DEAD" << std::endl - << " use DEAD as property for marking dead states" - << " (by default DEAD=true)" << std::endl -#endif - - << " -e use Couvreur's emptiness-check (default)" << std::endl - << " -e2 use Couvreur's emptiness-check's shy variant" << std::endl -#ifdef SSP - << " -e3 use semi-d. incl. Couvreur's emptiness-check" - << std::endl - << " -e4 use semi-d. incl. Couvreur's emptiness-check's " - << "shy variant" - << std::endl - << " -e45 mix of -e4 and -e5 (semi.d. incl. before d.incl.)" - << std::endl - << " -e54 mix of -e5 and -e4 (the other way around)" << std::endl - << " -e5 use d. incl. Couvreur's emptiness-check's shy variant" - << std::endl - << " -e6 like -e5, but without inclusion checks in the " - << "search stack" << std::endl -#endif - << " -m degeneralize and perform a magic-search" << std::endl - << std::endl -#ifdef SSP - << " -n do not perform any decomposition" << std::endl -#endif - << " -l use Couvreur's LaCIM algorithm for translation (default)" - << std::endl - << " -f use Couvreur's FM algorithm for translation" << std::endl - << " -P do not project example on model" << std::endl; - exit(2); -} - - -void -display_stats(const spot::unsigned_statistics* s) -{ - assert(s); - spot::unsigned_statistics::stats_map::const_iterator i; - for (i = s->stats.begin(); i != s->stats.end(); ++i) - std::cout << i->first << " = " << (s->*i->second)() << std::endl; -} - -int -main(int argc, char **argv) - try - { - int formula_index = 1; - enum { Couvreur, Couvreur2, Couvreur3, - Couvreur4, Couvreur5, Magic } check = Couvreur; - enum { Lacim, Fm } trans = Lacim; - bool compute_counter_example = false; - bool proj = true; -#ifdef SSP - bool doublehash = true; - bool stack_inclusion = true; - bool pushfront = false; - bool double_inclusion = false; - bool reversed_double_inclusion = false; - bool no_decomp = false; -#endif - std::string dead = "true"; - - spot::ltl::declarative_environment env; - - while (formula_index < argc && *argv[formula_index] == '-') - { -#ifdef SSP - if (!strcmp(argv[formula_index], "-1")) - { - doublehash = false; - } - else if (!strcmp(argv[formula_index], "-L")) - { - pushfront = true; - } - else -#endif - if (!strcmp(argv[formula_index], "-c")) - { - compute_counter_example = true; - } -#ifndef SSP - else if (!strcmp(argv[formula_index], "-d")) - { - if (formula_index + 1 >= argc) - syntax(argv[0]); - dead = argv[++formula_index]; - if (strcasecmp(dead.c_str(), "true") - && strcasecmp(dead.c_str(), "false")) - env.declare(dead); - } -#endif - else if (!strcmp(argv[formula_index], "-e")) - { - check = Couvreur; - } - else if (!strcmp(argv[formula_index], "-e2")) - { - check = Couvreur2; - } -#ifdef SSP - else if (!strcmp(argv[formula_index], "-e3")) - { - check = Couvreur3; - } - else if (!strcmp(argv[formula_index], "-e4")) - { - check = Couvreur4; - } - else if (!strcmp(argv[formula_index], "-e45")) - { - check = Couvreur5; - double_inclusion = true; - } - else if (!strcmp(argv[formula_index], "-e54")) - { - check = Couvreur5; - double_inclusion = true; - reversed_double_inclusion = true; - } - else if (!strcmp(argv[formula_index], "-e5")) - { - check = Couvreur5; - } - else if (!strcmp(argv[formula_index], "-e6")) - { - check = Couvreur5; - stack_inclusion = false; - } -#endif - else if (!strcmp(argv[formula_index], "-m")) - { - check = Magic; - } -#ifdef SSP - else if (!strcmp(argv[formula_index], "-n")) - { - no_decomp = true; - } -#endif - else if (!strcmp(argv[formula_index], "-l")) - { - trans = Lacim; - } - else if (!strcmp(argv[formula_index], "-f")) - { - trans = Fm; - } - else if (!strcmp(argv[formula_index], "-P")) - { - proj = 0; - } - else - { - syntax(argv[0]); - } - ++formula_index; - } - if (argc < formula_index + MIN_ARG) - syntax(argv[0]); - - - while (argc >= formula_index + MIN_ARG) - { - env.declare(argv[argc - 1]); - --argc; - } - - spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = - spot::ltl::parse(argv[formula_index + 1], pel, env); - - if (spot::ltl::format_parse_errors(std::cerr, - argv[formula_index + 1], pel)) - exit(2); - - argv[1] = argv[formula_index]; - spot::bdd_dict* dict = new spot::bdd_dict(); - -#if SSP - bool inclusion = (check != Couvreur && check != Couvreur2); - spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion, - doublehash, pushfront); - - spot::tgba_parse_error_list pel1; - spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], - pel1, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[formula_index + 2], - pel1)) - return 2; -#else - spot::gspn_interface gspn(2, argv, dict, env, dead); -#endif - - spot::tgba* a_f = 0; - switch (trans) - { - case Fm: - a_f = spot::ltl_to_tgba_fm(f, dict); - break; - case Lacim: - a_f = spot::ltl_to_tgba_lacim(f, dict); - break; - } - f->destroy(); - -#ifndef SSP - spot::tgba* model = gspn.automaton(); - spot::tgba_product* prod = new spot::tgba_product(model, a_f); -#else - spot::tgba_product* ca = new spot::tgba_product(control, a_f); - spot::tgba* model = gspn.automaton(ca); - spot::tgba* prod = model; -#endif - - switch (check) - { - case Couvreur: - case Couvreur2: - case Couvreur3: - case Couvreur4: - case Couvreur5: - { - spot::couvreur99_check* ec; - - switch (check) - { - case Couvreur: - ec = new spot::couvreur99_check(prod); - break; - case Couvreur2: - ec = new spot::couvreur99_check_shy(prod); - break; -#ifdef SSP - case Couvreur3: - ec = spot::couvreur99_check_ssp_semi(prod); - break; - case Couvreur4: - ec = spot::couvreur99_check_ssp_shy_semi(prod); - break; - case Couvreur5: - ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion, - double_inclusion, - reversed_double_inclusion, - no_decomp); - break; -#endif - default: - assert(0); - // Assign something so that GCC does not complains - // EC might be used uninitialized if assert is disabled. - ec = 0; - } - - spot::emptiness_check_result* res = ec->check(); - const spot::couvreur99_check_status* ecs = ec->result(); - if (res) - { - if (compute_counter_example) - { - spot::couvreur99_check_result* ce; -#ifndef SSP - ce = new spot::couvreur99_check_result(ecs); -#else - switch (check) - { - case Couvreur: - case Couvreur2: - case Couvreur5: - ce = new spot::couvreur99_check_result(ecs); - break; - default: - // ce = spot::counter_example_ssp(ecs); - std::cerr - << "counter_example_ssp() is no longer supported" - << std::endl; - exit(1); - } -#endif - spot::tgba_run* run = ce->accepting_run(); - if (proj) - { - spot::tgba_run* p = project_tgba_run(prod, model, run); - spot::print_tgba_run(std::cout, model, p); - delete p; - } - else - { - spot::print_tgba_run(std::cout, prod, run); - } - ce->print_stats(std::cout); - display_stats(ec); - delete run; - delete ce; - } - else - { - std::cout << "non empty" << std::endl; - ecs->print_stats(std::cout); - display_stats(ec); - } - delete res; - } - else - { - std::cout << "empty" << std::endl; - ecs->print_stats(std::cout); - display_stats(ec); - } - std::cout << std::endl; - delete ec; - if (res) - exit(1); - } - break; - case Magic: - { - spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); - spot::emptiness_check* ec = spot::explicit_magic_search(d); - - spot::emptiness_check_result* res = ec->check(); - if (res) - { - if (compute_counter_example) - { - spot::tgba_run* run = res->accepting_run(); - if (proj) - { - spot::tgba_run* p = project_tgba_run(prod, model, run); - spot::print_tgba_run(std::cout, model, p); - delete p; - } - else - { - spot::print_tgba_run(std::cout, prod, run); - } - delete run; - } - else - std::cout << "non-empty" << std::endl; - delete res; - exit(1); - } - else - { - std::cout << "empty" << std::endl; - } - delete ec; - delete d; - } - } -#ifndef SSP - delete prod; - delete model; -#else - delete model; - delete control; - delete ca; -#endif - delete a_f; - delete dict; - } - catch (spot::gspn_exception e) - { - std::cerr << e << std::endl; - throw; - } diff --git a/iface/gspn/simple.test b/iface/gspn/simple.test deleted file mode 100755 index 1c0b8363c..000000000 --- a/iface/gspn/simple.test +++ /dev/null @@ -1,42 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/simple . -chmod +w simple - -# Unknown properties should be flagged. -../dottygspn-rg simple/simple unknown && exit 1 - - -../dottygspn-rg simple/simple obs >output -# We expect exactly 1024 states. -grep ' 1024 ' output -grep ' 1025 ' output && exit 1 - - -../dottygspn-srg simple/simple obs >output -# We expect exactly 11 states. -grep ' 11 ' output -grep ' 12 ' output && exit 1 -: diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc deleted file mode 100644 index 4adebdb92..000000000 --- a/iface/gspn/ssp.cc +++ /dev/null @@ -1,1358 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005, 2006, 2007 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 . - -#include -#include -#include -#include -#include "ssp.hh" -#include "misc/bddlt.hh" -#include "misc/hash.hh" -#include -#include "tgbaalgos/gtec/explscc.hh" -#include "tgbaalgos/gtec/nsheap.hh" - -namespace spot -{ - - namespace - { - static bdd* - bdd_realloc(bdd* t, int size, int new_size) - { - assert(new_size); - bdd* tmp = new bdd[new_size]; - - for (int i = 0; i < size; i++) - tmp[i] = t[i]; - - delete[] t; - return tmp; - } - - static bool doublehash; - static bool pushfront; - } - - // state_gspn_ssp - ////////////////////////////////////////////////////////////////////// - - class state_gspn_ssp: public state - { - public: - state_gspn_ssp(State left, const state* right) - : left_(left), right_(right) - { - } - - virtual - ~state_gspn_ssp() - { - right_->destroy(); - } - - virtual int - compare(const state* other) const - { - const state_gspn_ssp* o = down_cast(other); - assert(o); - if (o->left() == left()) - return right_->compare(o->right()); - if (o->left() < left()) - return -1; - else - return 1; - } - - virtual size_t - hash() const - { - return ((reinterpret_cast(left()) - - static_cast(0)) << 10) + right_->hash(); - } - - virtual state_gspn_ssp* clone() const - { - return new state_gspn_ssp(left(), right()->clone()); - } - - State - left() const - { - return left_; - } - - const state* - right() const - { - return right_; - } - - private: - State left_; - const state* right_; - }; // state_gspn_ssp - - // tgba_gspn_ssp_private_ - ////////////////////////////////////////////////////////////////////// - - struct tgba_gspn_ssp_private_ - { - int refs; // reference count - - bdd_dict* dict; - typedef std::map prop_map; - prop_map prop_dict; - - signed char* all_props; - - size_t prop_count; - const tgba* operand; - - tgba_gspn_ssp_private_(bdd_dict* dict, - const ltl::declarative_environment& env, - const tgba* operand) - : refs(1), dict(dict), all_props(0), - operand(operand) - { - const ltl::declarative_environment::prop_map& p = env.get_prop_map(); - - try - { - AtomicProp max_prop = 0; - - for (ltl::declarative_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_exception("prop_index(" + i->first + ")", 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_ssp_private_() - { - dict->unregister_all_my_variables(this); - delete[] all_props; - } - }; - - - // tgba_succ_iterator_gspn_ssp - ////////////////////////////////////////////////////////////////////// - - class tgba_succ_iterator_gspn_ssp: public tgba_succ_iterator - { - public: - tgba_succ_iterator_gspn_ssp(Succ_* succ_tgba, - size_t size_tgba, - bdd* bdd_array, - state** state_array, - size_t size_states, - Props_* prop, - int size_prop) - : successors_(succ_tgba), - size_succ_(size_tgba), - current_succ_(0), - bdd_array_(bdd_array), - state_array_(state_array), - size_states_(size_states), - props_(prop), - size_prop_(size_prop) - { - } - - virtual - ~tgba_succ_iterator_gspn_ssp() - { - - for (size_t i = 0; i < size_states_; i++) - state_array_[i]->destroy(); - - delete[] bdd_array_; - free(state_array_); - - if (props_) - { - for (int i = 0; i < size_prop_; i++) - free(props_[i].arc); - free(props_); - } - - if (size_succ_ != 0) - succ_free(successors_); - - } - - virtual void - first() - { - if (!successors_) - return; - current_succ_=0; - } - - virtual void - next() - { - ++current_succ_; - } - - virtual bool - done() const - { - return current_succ_ + 1 > size_succ_; - } - - virtual state* - current_state() const - { - state_gspn_ssp* s = - new state_gspn_ssp(successors_[current_succ_].succ_, - (state_array_[successors_[current_succ_] - .arc->curr_state])->clone()); - return s; - } - - virtual bdd - current_condition() const - { - return bddtrue; - } - - virtual bdd - current_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems, so we just - // return those from operand_. - return bdd_array_[successors_[current_succ_].arc->curr_acc_conds]; - } - private: - - // All successors of STATE matching a selection conjunctions from - // ALL_CONDS. - Succ_* successors_; /// array of successors - size_t size_succ_; /// size of successors_ - size_t current_succ_; /// current position in successors_ - - bdd * bdd_array_; - state** state_array_; - size_t size_states_; - Props_* props_; - int size_prop_; - }; // tgba_succ_iterator_gspn_ssp - - - // tgba_gspn_ssp - ////////////////////////////////////////////////////////////////////// - - class tgba_gspn_ssp: public tgba - { - public: - tgba_gspn_ssp(bdd_dict* dict, const ltl::declarative_environment& env, - const tgba* operand); - tgba_gspn_ssp(const tgba_gspn_ssp& other); - tgba_gspn_ssp& operator=(const tgba_gspn_ssp& other); - virtual ~tgba_gspn_ssp(); - virtual state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const state* local_state, - const state* global_state = 0, - const tgba* global_automaton = 0) const; - virtual bdd_dict* get_dict() const; - virtual std::string format_state(const state* state) const; - virtual state* project_state(const state* s, const tgba* t) const; - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - protected: - virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; - private: - tgba_gspn_ssp_private_* data_; - }; - - tgba_gspn_ssp::tgba_gspn_ssp(bdd_dict* dict, - const ltl::declarative_environment& env, - const tgba* operand) - { - data_ = new tgba_gspn_ssp_private_(dict, env, operand); - } - - tgba_gspn_ssp::tgba_gspn_ssp(const tgba_gspn_ssp& other) - : tgba() - { - data_ = other.data_; - ++data_->refs; - } - - tgba_gspn_ssp::~tgba_gspn_ssp() - { - if (--data_->refs == 0) - delete data_; - } - - tgba_gspn_ssp& - tgba_gspn_ssp::operator=(const tgba_gspn_ssp& other) - { - if (&other == this) - return *this; - this->~tgba_gspn_ssp(); - new (this) tgba_gspn_ssp(other); - return *this; - } - - state* tgba_gspn_ssp::get_init_state() const - { - // Use 0 as initial state for the SSP side. State 0 does not - // exists, but when passed to succ() it will produce the list - // of initial states. - return new state_gspn_ssp(0, data_->operand->get_init_state()); - } - - tgba_succ_iterator* - tgba_gspn_ssp::succ_iter(const state* state_, - const state* global_state, - const tgba* global_automaton) const - { - const state_gspn_ssp* s = down_cast(state_); - assert(s); - (void) global_state; - (void) global_automaton; - - bdd all_conds_; - bdd outside_; - bdd cond; - - Props_* props_ = 0; - int nb_arc_props = 0; - bdd* bdd_array = 0; - int size_bdd = 0; - state** state_array = 0; - size_t size_states = 0; - - for (auto i: data_->operand->succ(s)) - { - all_conds_ = i->current_condition(); - outside_ = !all_conds_; - - if (all_conds_ != bddfalse) - { - props_ = (Props_*) realloc(props_, - (nb_arc_props + 1) * sizeof(Props_)); - - props_[nb_arc_props].nb_conj = 0; - props_[nb_arc_props].prop = 0; - props_[nb_arc_props].arc = - (Arc_Ident_*) malloc(sizeof(Arc_Ident_)); - - bdd_array = bdd_realloc(bdd_array, size_bdd, size_bdd + 1); - bdd_array[size_bdd] = i->current_acceptance_conditions(); - props_[nb_arc_props].arc->curr_acc_conds = size_bdd; - ++size_bdd; - - state_array = - (state**) realloc(state_array, - (size_states + 1) * sizeof(state*)); - state_array[size_states] = i->current_state(); - props_[nb_arc_props].arc->curr_state = size_states; - ++size_states; - - while (all_conds_ != bddfalse) - { - cond = bdd_satone(all_conds_); - cond = bdd_simplify(cond, cond | outside_); - all_conds_ -= cond; - - props_[nb_arc_props].prop = - (signed char **) realloc(props_[nb_arc_props].prop, - (props_[nb_arc_props].nb_conj + 1) - * sizeof(signed char *)); - - props_[nb_arc_props].prop[props_[nb_arc_props].nb_conj] - = (signed char*) calloc(data_->prop_count, - sizeof(signed char)); - memset(props_[nb_arc_props].prop[props_[nb_arc_props].nb_conj], - -1, data_->prop_count); - - while (cond != bddtrue) - { - int var = bdd_var(cond); - bdd high = bdd_high(cond); - int res; - - if (high == bddfalse) - { - cond = bdd_low(cond); - res = 0; - } - else - { - cond = high; - res = 1; - } - - tgba_gspn_ssp_private_::prop_map::iterator k - = data_->prop_dict.find(var); - - if (k != data_->prop_dict.end()) - props_[nb_arc_props] - .prop[props_[nb_arc_props].nb_conj][k->second] = res; - - assert(cond != bddfalse); - } - ++props_[nb_arc_props].nb_conj; - } - ++nb_arc_props; - } - } - Succ_* succ_tgba_ = 0; - size_t size_tgba_ = 0; - int j, conj; - - succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_); - - for (j = 0; j < nb_arc_props; j++) - { - for (conj = 0; conj < props_[j].nb_conj; conj++) - free(props_[j].prop[conj]); - free(props_[j].prop); - } - return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_, - bdd_array, state_array, - size_states, props_, - nb_arc_props); - } - - bdd - tgba_gspn_ssp::compute_support_conditions(const spot::state* state) const - { - (void) state; - return bddtrue; - } - - bdd - tgba_gspn_ssp::compute_support_variables(const spot::state* state) const - { - (void) state; - return bddtrue; - } - - bdd_dict* - tgba_gspn_ssp::get_dict() const - { - return data_->dict; - } - - std::string - tgba_gspn_ssp::format_state(const state* state) const - { - const state_gspn_ssp* s = down_cast(state); - assert(s); - char* str; - State gs = s->left(); - if (gs) - { - int err = print_state(gs, &str); - if (err) - throw gspn_exception("print_state()", err); - // Strip trailing \n... - unsigned len = strlen(str); - while (str[--len] == '\n') - str[len] = 0; - } - else - { - str = strdup("-1"); - } - - std::string res(str); - free(str); - return res + " * " + data_->operand->format_state(s->right()); - } - - state* - tgba_gspn_ssp::project_state(const state* s, const tgba* t) const - { - const state_gspn_ssp* s2 = down_cast(s); - assert(s2); - if (t == this) - return s2->clone(); - return data_->operand->project_state(s2->right(), t); - } - - bdd - tgba_gspn_ssp::all_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems, they all - // come from the operand automaton. - return data_->operand->all_acceptance_conditions(); - } - - bdd - tgba_gspn_ssp::neg_acceptance_conditions() const - { - // There is no acceptance conditions in GSPN systems, they all - // come from the operand automaton. - return data_->operand->neg_acceptance_conditions(); - } - - // gspn_ssp_interface - ////////////////////////////////////////////////////////////////////// - - gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv, - bdd_dict* dict, - const - ltl::declarative_environment& env, - bool inclusion, - bool doublehash_, - bool pushfront_) - : dict_(dict), env_(env) - { - doublehash = doublehash_; - pushfront = pushfront_; - if (inclusion) - inclusion_version(); - - int res = initialize(argc, argv); - if (res) - throw gspn_exception("initialize()", res); - } - - gspn_ssp_interface::~gspn_ssp_interface() - { - int res = finalize(); - if (res) - throw gspn_exception("finalize()", res); - } - - tgba* - gspn_ssp_interface::automaton(const tgba* operand) const - { - return new tgba_gspn_ssp(dict_, env_, operand); - } - - - ////////////////////////////////////////////////////////////////////// - - class connected_component_ssp: public explicit_connected_component - { - public: - virtual - ~connected_component_ssp() - { - } - - virtual const state* - has_state(const state* s) const - { - set_type::const_iterator i; - - for (i = states.begin(); i != states.end(); ++i) - { - const state_gspn_ssp* old_state = (const state_gspn_ssp*)(*i); - const state_gspn_ssp* new_state = (const state_gspn_ssp*)(s); - - if ((old_state->right())->compare(new_state->right()) == 0 - && old_state->left() - && new_state->left()) - if (spot_inclusion(new_state->left(), old_state->left())) - { - if (*i != s) - s->destroy(); - return *i; - } - } - return 0; - } - - virtual void - insert(const state* s) - { - states.insert(s); - } - - protected: - typedef std::unordered_set set_type; - set_type states; - }; - - class connected_component_ssp_factory : - public explicit_connected_component_factory - { - public: - virtual connected_component_ssp* - build() const - { - return new connected_component_ssp(); - } - - /// Get the unique instance of this class. - static const connected_component_ssp_factory* - instance() - { - static connected_component_ssp_factory f; - return &f; - } - - protected: - virtual - ~connected_component_ssp_factory() - { - } - /// Construction is forbiden. - connected_component_ssp_factory() - { - } - }; - - ////////////////////////////////////////////////////////////////////// - - namespace - { - inline void* - container_(const State s) - { - return doublehash ? container(s) : 0; - } - } - - class numbered_state_heap_ssp_semi : public numbered_state_heap - { - public: - numbered_state_heap_ssp_semi() - : numbered_state_heap(), inclusions(0) - { - } - - virtual - ~numbered_state_heap_ssp_semi() - { - // Free keys in H. - hash_type::iterator i = h.begin(); - while (i != h.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - s->destroy(); - } - } - - virtual numbered_state_heap::state_index - find(const state* s) const - { - const state_gspn_ssp* s_ = down_cast(s); - const void* cont = container_(s_->left()); - contained_map::const_iterator i = contained.find(cont); - if (i != contained.end()) - { - f_map::const_iterator k = i->second.find(s_->right()); - if (k != i->second.end()) - { - const state_list& l = k->second; - - state_list::const_iterator j; - for (j = l.begin(); j != l.end(); ++j) - { - const state_gspn_ssp* old_state = - down_cast(*j); - const state_gspn_ssp* new_state = - down_cast(s); - assert(old_state); - assert(new_state); - - if (old_state->left() == new_state->left()) - break; - - if (old_state->left() - && new_state->left() - && spot_inclusion(new_state->left(), old_state->left())) - { - ++inclusions; - break; - } - } - if (j != l.end()) - { - if (s != *j) - { - s->destroy(); - s = *j; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - - state_index res; - - if (s == 0) - { - res.first = 0; - res.second = 0; - } - else - { - hash_type::const_iterator i = h.find(s); - assert(i != h.end()); - assert(s == i->first); - res.first = i->first; - res.second = i->second; - } - return res; - } - - virtual numbered_state_heap::state_index_p - find(const state* s) - { - const state_gspn_ssp* s_ = down_cast(s); - const void* cont = container_(s_->left()); - contained_map::const_iterator i = contained.find(cont); - if (i != contained.end()) - { - f_map::const_iterator k = i->second.find(s_->right()); - if (k != i->second.end()) - { - const state_list& l = k->second; - - state_list::const_iterator j; - for (j = l.begin(); j != l.end(); ++j) - { - const state_gspn_ssp* old_state = - down_cast(*j); - const state_gspn_ssp* new_state = - down_cast(s); - assert(old_state); - assert(new_state); - - if (old_state->left() == new_state->left()) - break; - - if (old_state->left() - && new_state->left() - && spot_inclusion(new_state->left(), old_state->left())) - { - ++inclusions; - break; - } - } - if (j != l.end()) - { - if (s != *j) - { - s->destroy(); - s = *j; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - - state_index_p res; - - if (s == 0) - { - res.first = 0; - res.second = 0; - } - else - { - hash_type::iterator i = h.find(s); - assert(i != h.end()); - assert(s == i->first); - res.first = i->first; - res.second = &i->second; - } - return res; - } - - virtual numbered_state_heap::state_index - index(const state* s) const - { - state_index res; - hash_type::const_iterator i = h.find(s); - if (i == h.end()) - { - res.first = 0; - res.second = 0; - } - else - { - res.first = i->first; - res.second = i->second; - - if (s != i->first) - s->destroy(); - } - return res; - } - - virtual numbered_state_heap::state_index_p - index(const state* s) - { - state_index_p res; - hash_type::iterator i = h.find(s); - if (i == h.end()) - { - res.first = 0; - res.second = 0; - } - else - { - res.first = i->first; - res.second = &i->second; - - if (s != i->first) - s->destroy(); - } - return res; - } - - virtual void - insert(const state* s, int index) - { - h[s] = index; - - const state_gspn_ssp* s_ = down_cast(s); - State sg = s_->left(); - if (sg) - { - const void* cont = container_(sg); - if (pushfront) - contained[cont][s_->right()].push_front(s); - else - contained[cont][s_->right()].push_back(s); - } - } - - virtual int - size() const - { - return h.size(); - } - - virtual numbered_state_heap_const_iterator* iterator() const; - - protected: - typedef std::unordered_map hash_type; - hash_type h; ///< Map of visited states. - - typedef std::list state_list; - typedef std::unordered_map f_map; - typedef std::unordered_map > contained_map; - contained_map contained; - - friend class numbered_state_heap_ssp_const_iterator; - friend class couvreur99_check_shy_ssp; - friend class couvreur99_check_shy_semi_ssp; - - mutable unsigned inclusions; - }; - - - class numbered_state_heap_ssp_const_iterator : - public numbered_state_heap_const_iterator - { - public: - numbered_state_heap_ssp_const_iterator - (const numbered_state_heap_ssp_semi::hash_type& h) - : numbered_state_heap_const_iterator(), h(h) - { - } - - ~numbered_state_heap_ssp_const_iterator() - { - } - - virtual void - first() - { - i = h.begin(); - } - - virtual void - next() - { - ++i; - } - - virtual bool - done() const - { - return i == h.end(); - } - - virtual const state* - get_state() const - { - return i->first; - } - - virtual int - get_index() const - { - return i->second; - } - - private: - numbered_state_heap_ssp_semi::hash_type::const_iterator i; - const numbered_state_heap_ssp_semi::hash_type& h; - }; - - - numbered_state_heap_const_iterator* - numbered_state_heap_ssp_semi::iterator() const - { - return new numbered_state_heap_ssp_const_iterator(h); - } - - - /// \brief Factory for numbered_state_heap_ssp_semi - /// - /// This class is a singleton. Retrieve the instance using instance(). - class numbered_state_heap_ssp_factory_semi: - public numbered_state_heap_factory - { - public: - virtual numbered_state_heap_ssp_semi* - build() const - { - return new numbered_state_heap_ssp_semi(); - } - - /// Get the unique instance of this class. - static const numbered_state_heap_ssp_factory_semi* - instance() - { - static numbered_state_heap_ssp_factory_semi f; - return &f; - } - - protected: - virtual - ~numbered_state_heap_ssp_factory_semi() - { - } - - numbered_state_heap_ssp_factory_semi() - { - } - }; - - - class couvreur99_check_shy_ssp : public couvreur99_check_shy - { - public: - couvreur99_check_shy_ssp(const tgba* a, bool stack_inclusion, - bool double_inclusion, - bool reversed_double_inclusion, - bool no_decomp) - : couvreur99_check_shy(a, - option_map(), - numbered_state_heap_ssp_factory_semi::instance()), - inclusion_count_heap(0), - inclusion_count_stack(0), - stack_inclusion(stack_inclusion), - double_inclusion(double_inclusion), - reversed_double_inclusion(reversed_double_inclusion), - no_decomp(no_decomp) - { - onepass_ = true; - - stats["inclusion count heap"] = - static_cast - (&couvreur99_check_shy_ssp::get_inclusion_count_heap); - stats["inclusion count stack"] = - static_cast - (&couvreur99_check_shy_ssp::get_inclusion_count_stack); - stats["contained map size"] = - static_cast - (&couvreur99_check_shy_ssp::get_contained_map_size); - } - - private: - unsigned inclusion_count_heap; - unsigned inclusion_count_stack; - bool stack_inclusion; - bool double_inclusion; - bool reversed_double_inclusion; - bool no_decomp; - - protected: - unsigned - get_inclusion_count_heap() const - { - return inclusion_count_heap; - }; - unsigned - get_inclusion_count_stack() const - { - return inclusion_count_stack; - }; - unsigned - get_contained_map_size() const - { - return - down_cast(ecs_->h)->contained.size(); - } - - // If a new state includes an older state, we may have to add new - // children to the list of children of that older state. We cannot - // to this by sub-classing numbered_state_heap since TODO is not - // available. So we override find_state() instead. - virtual numbered_state_heap::state_index_p - find_state(const state* s) - { - typedef numbered_state_heap_ssp_semi::hash_type hash_type; - hash_type& h = down_cast(ecs_->h)->h; - typedef numbered_state_heap_ssp_semi::contained_map contained_map; - typedef numbered_state_heap_ssp_semi::f_map f_map; - typedef numbered_state_heap_ssp_semi::state_list state_list; - const contained_map& contained = - down_cast(ecs_->h)->contained; - - const state_gspn_ssp* s_ = down_cast(s); - const void* cont = container_(s_->left()); - contained_map::const_iterator i = contained.find(cont); - - if (i != contained.end()) - { - f_map::const_iterator k = i->second.find(s_->right()); - if (k != i->second.end()) - { - const state_list& l = k->second; - state_list::const_iterator j; - - // Make a first pass looking for identical states. - for (j = l.begin(); j != l.end(); ++j) - { - const state_gspn_ssp* old_state = - down_cast(*j); - const state_gspn_ssp* new_state = - down_cast(s); - assert(old_state); - assert(new_state); - - if (old_state->left() == new_state->left()) - goto found_match; - } - - // Now, check for inclusions. - for (j = l.begin(); j != l.end(); ++j) - { - const state_gspn_ssp* old_state = - down_cast(*j); - const state_gspn_ssp* new_state = - down_cast(s); - assert(old_state); - assert(new_state); - - if (old_state->left() && new_state->left()) - { - hash_type::const_iterator i = h.find(*j); - assert(i != h.end()); - if (i->second == -1) - { - if (spot_inclusion(new_state->left(), - old_state->left())) - { - ++inclusion_count_heap; - break; - } - } - else - { - if (stack_inclusion - && double_inclusion - && !reversed_double_inclusion - && spot_inclusion(new_state->left(), - old_state->left())) - break; - if (stack_inclusion - && spot_inclusion(old_state->left(), - new_state->left())) - { - ++inclusion_count_stack; - - succ_queue& queue = todo.back().q; - succ_queue::iterator old; - if (pos == queue.end()) - old = queue.begin(); - else - { - old = pos; - // Should not happen, because onepass_ == 1 - assert(0); - } - - if (no_decomp) - { - queue.push_back // why not push_front? - (successor(old->acc, - old_state->clone())); - - assert(pos == queue.end()); - - inc_depth(); - - // If we had not done the first loop - // over the container to check for - // equal states, we would have to do - // one here to make sure that state - // s is not equal to another known - // state. (We risk some intricate - // memory corruption if we don't - // destroy "clone states" at this - // point.) - - // Since we have that first loop and - // we therefore know that state s is - // genuinely new, position j so that - // we won't destroy it. - j = l.end(); - } - else - { - State* succ_tgba_ = 0; - size_t size_tgba_ = 0; - - Diff_succ(old_state->left(), - new_state->left(), - &succ_tgba_, &size_tgba_); - - for (size_t i = 0; i < size_tgba_; i++) - { - state_gspn_ssp* s = - new state_gspn_ssp - (succ_tgba_[i], - old_state->right()->clone()); - // why not push_front? - queue.push_back(successor(old->acc, s)); - inc_depth(); - } - if (size_tgba_ != 0) - diff_succ_free(succ_tgba_); - } - - break; - } - if (stack_inclusion - && double_inclusion - && reversed_double_inclusion - && spot_inclusion(new_state->left(), - old_state->left())) - break; - } - } - } - found_match: - if (j != l.end()) - { - if (s != *j) - { - s->destroy(); - s = *j; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - } - else - { - s = 0; - } - - // s points to the resulting state, or to 0 if we didn't find - // the state in the list. - - numbered_state_heap::state_index_p res; - if (s == 0) - { - res.first = 0; - res.second = 0; - } - else - { - hash_type::iterator k = h.find(s); - assert(k != h.end()); - assert(s == k->first); - res.first = k->first; - res.second = &k->second; - } - - return res; - } - }; - - - // The only purpose of this class is the inclusion_count counter. - class couvreur99_check_shy_semi_ssp : public couvreur99_check_shy - { - public: - couvreur99_check_shy_semi_ssp(const tgba* a) - : couvreur99_check_shy(a, - option_map(), - numbered_state_heap_ssp_factory_semi::instance()), - find_count(0) - { - onepass_ = true; - - stats["find_state count"] = - static_cast - (&couvreur99_check_shy_semi_ssp::get_find_count); - stats["contained map size"] = - static_cast - (&couvreur99_check_shy_semi_ssp::get_contained_map_size); - stats["inclusion count"] = - static_cast - (&couvreur99_check_shy_semi_ssp::get_inclusion_count); - - //down_cast(ecs_->h)->stats = this; - } - - private: - unsigned find_count; - - protected: - unsigned - get_find_count() const - { - return find_count; - }; - - unsigned - get_inclusion_count() const - { - return - down_cast(ecs_->h)->inclusions; - - }; - - unsigned - get_contained_map_size() const - { - return - down_cast(ecs_->h)->contained.size(); - } - - virtual numbered_state_heap::state_index_p - find_state(const state* s) - { - ++find_count; - return couvreur99_check_shy::find_state(s); - } - }; - - - couvreur99_check* - couvreur99_check_ssp_semi(const tgba* ssp_automata) - { - assert(dynamic_cast(ssp_automata)); - return - new couvreur99_check(ssp_automata, - option_map(), - numbered_state_heap_ssp_factory_semi::instance()); - } - - couvreur99_check* - couvreur99_check_ssp_shy_semi(const tgba* ssp_automata) - { - assert(dynamic_cast(ssp_automata)); - return - new couvreur99_check_shy_semi_ssp(ssp_automata); - } - - couvreur99_check* - couvreur99_check_ssp_shy(const tgba* ssp_automata, bool stack_inclusion, - bool double_inclusion, - bool reversed_double_inclusion, - bool no_decomp) - { - assert(dynamic_cast(ssp_automata)); - return new couvreur99_check_shy_ssp(ssp_automata, stack_inclusion, - double_inclusion, - reversed_double_inclusion, - no_decomp); - } - -#if 0 - // I rewrote couvreur99_check_result today, and it no longer uses - // connected_component_ssp_factory. So this cannot work anymore. - // -- adl 2004-12-10. - couvreur99_check_result* - counter_example_ssp(const couvreur99_check_status* status) - { - return new - couvreur99_check_result(status, - connected_component_ssp_factory::instance()); - } -#endif -} diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh deleted file mode 100644 index 93e9c68c8..000000000 --- a/iface/gspn/ssp.hh +++ /dev/null @@ -1,74 +0,0 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006, 2007 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 . - -#ifndef SPOT_IFACE_GSPN_SSP_HH -# define SPOT_IFACE_GSPN_SSP_HH - -// Do not include gspnlib.h here, or it will polute the user's -// namespace with internal C symbols. - -# include -# include "tgba/tgba.hh" -# include "common.hh" -# include "tgbaalgos/gtec/gtec.hh" -# include "tgbaalgos/gtec/ce.hh" -# include "ltlenv/declenv.hh" - -namespace spot -{ - - class gspn_ssp_interface - { - public: - gspn_ssp_interface(int argc, char **argv, - bdd_dict* dict, const ltl::declarative_environment& env, - bool inclusion = false, - bool doublehash = true, - bool pushfront = false); - ~gspn_ssp_interface(); - tgba* automaton(const tgba* operand) const; - private: - bdd_dict* dict_; - const ltl::declarative_environment& env_; - }; - - /// \defgroup emptiness_check_ssp Emptiness-check algorithms for SSP - /// \ingroup emptiness_check - /// @{ - couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata); - couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); - couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata, - bool stack_inclusion = true, - bool double_inclusion = false, - bool reversed_double_inclusion - = false, - bool no_decomp = false); - - /// @} - - // I rewrote couvreur99_check_result today, and it no longer use - // connected_component_ssp_factory. So this cannot work anymore. - // -- adl 2004-12-10. - // couvreur99_check_result* - // counter_example_ssp(const couvreur99_check_status* status); -} - -#endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH diff --git a/iface/gspn/udcsefm.test b/iface/gspn/udcsefm.test deleted file mode 100755 index bb89150f2..000000000 --- a/iface/gspn/udcsefm.test +++ /dev/null @@ -1,44 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/udcs . -chmod +w udcs - -# F(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -f -e udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -../ltlgspn-srg -c -f -e2 udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -# !F(ReP1 => F(gsP1)) is true -../ltlgspn-srg -c -f -e udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output -../ltlgspn-srg -c -f -e2 udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output - -# !G(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -f -e udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -../ltlgspn-srg -c -f -e2 udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -: diff --git a/iface/gspn/udcseltl.test b/iface/gspn/udcseltl.test deleted file mode 100755 index 46ee000e6..000000000 --- a/iface/gspn/udcseltl.test +++ /dev/null @@ -1,45 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/udcs . -chmod +w udcs - -# F(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -l -e udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -../ltlgspn-srg -c -l -e2 udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -# !F(ReP1 => F(gsP1)) is true -../ltlgspn-srg -c -l -e udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output -../ltlgspn-srg -c -l -e2 udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output - -# !G(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -l -e udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -../ltlgspn-srg -d dead -c -l -e2 udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -grep ' !dead' output -grep ' dead' output && exit 1 -: diff --git a/iface/gspn/udcsfm.test b/iface/gspn/udcsfm.test deleted file mode 100755 index 8610e1062..000000000 --- a/iface/gspn/udcsfm.test +++ /dev/null @@ -1,39 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/udcs . -chmod +w udcs - -# F(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -f -m udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -# !F(ReP1 => F(gsP1)) is true -../ltlgspn-srg -c -f -m udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output - -# !G(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -f -m udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -: diff --git a/iface/gspn/udcsltl.test b/iface/gspn/udcsltl.test deleted file mode 100755 index 886d2349d..000000000 --- a/iface/gspn/udcsltl.test +++ /dev/null @@ -1,39 +0,0 @@ -#! /bin/sh -# Copyright (C) 2003 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 . - -. ./defs || exit 1 - -set -e - -cp -R $srcdir/examples/udcs . -chmod +w udcs - -# F(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -l -m udcs/udcs \ - 'F(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -# !F(ReP1 => F(gsP1)) is true -../ltlgspn-srg -c -l -m udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 >output - -# !G(ReP1 => F(gsP1)) is false -../ltlgspn-srg -c -l -m udcs/udcs \ - '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - -: diff --git a/m4/gspnlib.m4 b/m4/gspnlib.m4 deleted file mode 100644 index b9440454c..000000000 --- a/m4/gspnlib.m4 +++ /dev/null @@ -1,44 +0,0 @@ -AC_DEFUN([AX_CHECK_GSPNLIB], [ - AC_ARG_WITH([gspn], - [AC_HELP_STRING([--with-gspn=/root/of/greatspn], - [build interface with GreadSPN])]) - if test "x${with_gspn-no}" != xno; then - ax_tmp_LDFLAGS=$LDFLAGS - ax_tmp_LIBS=$LIBS - LIBGSPN_LDFLAGS= - if test "x${with_gspn-yes}" != xyes; then - # Try to locate the headers and libraries. - gspn_version_sh=$with_gspn/SOURCES/contrib/version.sh; - AC_CHECK_FILE($gspn_version_sh,, - [AC_MSG_ERROR( - [Cannot find $gspn_version_sh. Check --with-gspn's argument.])]) - gspn_version=`$gspn_version_sh` - LIBGSPN_LDFLAGS="-L$with_gspn/$gspn_version/2bin/lib" - LIBGSPN_CPPFLAGS="-I$with_gspn/SOURCES/WN/INCLUDE" - fi - LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" - AC_CHECK_LIB([gspnRG], [initialize], [], - [AC_MSG_ERROR([Cannot find libgspnRG. Check --with-gspn's argument.])], [-lm -lfl]) - LIBGSPNRG_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnRG -lm -lfl" - - LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" - AC_CHECK_LIB([gspnSRG], [initialize], [], - [AC_MSG_ERROR([Cannot find libgspnSRG. Check --with-gspn's argument.])], [-lm -lfl]) - LIBGSPNSRG_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnSRG -lm -lfl" - - LDFLAGS="$LDFLAGS $LIBGSPN_LDFLAGS" - # Soheib Baarir is working on this library, and it is not part - # of the GreatSPN repository yet. Use it only if it is here. - AC_CHECK_LIB([gspnSSP], [initialize], [have_ssp=yes], - [have_ssp=no], [-lm -lfl]) - LIBGSPNSSP_LDFLAGS="$LIBGSPN_LDFLAGS -lgspnSSP -lm -lfl" - LDFLAGS="$ax_tmp_LDFLAGS" - LIBS="$ax_tmp_LIBS" - fi - AM_CONDITIONAL([WITH_GSPN], [test "x${with_gspn-no}" != xno]) - AM_CONDITIONAL([WITH_GSPN_SSP], [test "x${have_ssp-no}" != xno]) - AC_SUBST([LIBGSPN_CPPFLAGS]) - AC_SUBST([LIBGSPNRG_LDFLAGS]) - AC_SUBST([LIBGSPNSRG_LDFLAGS]) - AC_SUBST([LIBGSPNSSP_LDFLAGS]) -]) diff --git a/src/sanity/Makefile.am b/src/sanity/Makefile.am index fdcfae8e3..d69364e77 100644 --- a/src/sanity/Makefile.am +++ b/src/sanity/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -53,7 +53,7 @@ check-local: check-80columns check-style check-readme check-includes # Ensure we have not forgotten to include an header. check-installed-includes: CXX='$(CXX)' \ - CPPFLAGS='-I $(includedir) -I$(pkgincludedir) $(LIBGSPN_CPPFLAGS) $(CPPFLAGS)' \ + CPPFLAGS='-I $(includedir) -I$(pkgincludedir) $(CPPFLAGS)' \ CXXFLAGS='$(AM_CXXFLAGS) $(CXXFLAGS)' \ INCDIR='$(pkgincludedir)' \ $(SHELL) $(srcdir)/includes.test $(TESTHEADER)