From 46e4408a859a244852e11328ef4f872907105c98 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 29 Jan 2014 22:01:21 +0100 Subject: [PATCH] gspn: remove the interface with GreatSPN It hasn't been tested for several year, may not even compile, has to be linked with source code that isn't even publicly available, and its presence was the only reason to keep some inefficient code in gtec.cc and friends. * iface/gspn/: Delete this directory. * iface/Makefile.am, configure.ac, README: Adjust. * m4/gspnlib.m4: Delete. * src/sanity/Makefile.am: Do not use LIBGSPN_CPPFLAGS. --- README | 12 - configure.ac | 3 - iface/Makefile.am | 10 +- iface/gspn/.cvsignore | 8 - iface/gspn/.gitignore | 15 - iface/gspn/Makefile.am | 103 -- iface/gspn/common.cc | 33 - iface/gspn/common.hh | 61 - iface/gspn/dcswave.test | 32 - iface/gspn/dcswaveeltl.test | 40 - iface/gspn/dcswavefm.test | 36 - iface/gspn/dcswaveltl.test | 36 - iface/gspn/defs.in | 53 - iface/gspn/dottygspn.cc | 54 - iface/gspn/dottyssp.cc | 61 - iface/gspn/examples/DCSwave/DCSWave.def | 66 -- iface/gspn/examples/DCSwave/DCSWave.net | 38 - iface/gspn/examples/DCSwave/DCSWave.tobs | 14 - iface/gspn/examples/simple/.cvsignore | 9 - iface/gspn/examples/simple/.gitignore | 9 - iface/gspn/examples/simple/simple.def | 30 - iface/gspn/examples/simple/simple.net | 15 - iface/gspn/examples/simple/simple.tobs | 5 - iface/gspn/examples/udcs/udcs.def | 78 -- iface/gspn/examples/udcs/udcs.net | 46 - iface/gspn/examples/udcs/udcs.tobs | 9 - iface/gspn/gspn.cc | 493 -------- iface/gspn/gspn.hh | 49 - iface/gspn/ltlgspn.cc | 430 ------- iface/gspn/simple.test | 42 - iface/gspn/ssp.cc | 1358 ---------------------- iface/gspn/ssp.hh | 74 -- iface/gspn/udcsefm.test | 44 - iface/gspn/udcseltl.test | 45 - iface/gspn/udcsfm.test | 39 - iface/gspn/udcsltl.test | 39 - m4/gspnlib.m4 | 44 - src/sanity/Makefile.am | 6 +- 38 files changed, 5 insertions(+), 3534 deletions(-) delete mode 100644 iface/gspn/.cvsignore delete mode 100644 iface/gspn/.gitignore delete mode 100644 iface/gspn/Makefile.am delete mode 100644 iface/gspn/common.cc delete mode 100644 iface/gspn/common.hh delete mode 100755 iface/gspn/dcswave.test delete mode 100755 iface/gspn/dcswaveeltl.test delete mode 100755 iface/gspn/dcswavefm.test delete mode 100755 iface/gspn/dcswaveltl.test delete mode 100644 iface/gspn/defs.in delete mode 100644 iface/gspn/dottygspn.cc delete mode 100644 iface/gspn/dottyssp.cc delete mode 100644 iface/gspn/examples/DCSwave/DCSWave.def delete mode 100644 iface/gspn/examples/DCSwave/DCSWave.net delete mode 100644 iface/gspn/examples/DCSwave/DCSWave.tobs delete mode 100644 iface/gspn/examples/simple/.cvsignore delete mode 100644 iface/gspn/examples/simple/.gitignore delete mode 100644 iface/gspn/examples/simple/simple.def delete mode 100644 iface/gspn/examples/simple/simple.net delete mode 100644 iface/gspn/examples/simple/simple.tobs delete mode 100644 iface/gspn/examples/udcs/udcs.def delete mode 100644 iface/gspn/examples/udcs/udcs.net delete mode 100644 iface/gspn/examples/udcs/udcs.tobs delete mode 100644 iface/gspn/gspn.cc delete mode 100644 iface/gspn/gspn.hh delete mode 100644 iface/gspn/ltlgspn.cc delete mode 100755 iface/gspn/simple.test delete mode 100644 iface/gspn/ssp.cc delete mode 100644 iface/gspn/ssp.hh delete mode 100755 iface/gspn/udcsefm.test delete mode 100755 iface/gspn/udcseltl.test delete mode 100755 iface/gspn/udcsfm.test delete mode 100755 iface/gspn/udcsltl.test delete mode 100644 m4/gspnlib.m4 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)