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.
This commit is contained in:
Alexandre Duret-Lutz
parent
83ed4f8c90
commit
46e4408a85
38 changed files with 5 additions and 3534 deletions
12
README
12
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
|
||||
--------------------
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
SUBDIRS = dve2
|
||||
|
||||
if WITH_GSPN
|
||||
SUBDIRS += gspn
|
||||
endif
|
||||
|
|
|
|||
|
|
@ -1,8 +0,0 @@
|
|||
Makefile.in
|
||||
Makefile
|
||||
*.lo
|
||||
*.o
|
||||
*.la
|
||||
.deps
|
||||
.libs
|
||||
defs
|
||||
15
iface/gspn/.gitignore
vendored
15
iface/gspn/.gitignore
vendored
|
|
@ -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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "common.hh"
|
||||
#include <ostream>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
std::ostream&
|
||||
operator<<(std::ostream& os, const gspn_exception& e)
|
||||
{
|
||||
os << e.get_where() << " exited with " << e.get_err();
|
||||
return os;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_IFACE_GSPN_COMMON_HH
|
||||
# define SPOT_IFACE_GSPN_COMMON_HH
|
||||
|
||||
# include <string>
|
||||
# include <iosfwd>
|
||||
|
||||
// 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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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
|
||||
<S proc_0> + <S proc_1> + <S proc_2>
|
||||
))
|
||||
(F5 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F6 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F7 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F8 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F9 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F10 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F11 f 1.0 1.0 (@f
|
||||
<S proc_0>+<S proc_1>+<S proc_2>
|
||||
))
|
||||
(F12 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F13 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F14 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F15 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F16 f 1.0 1.0 (@f
|
||||
<S proc_0>+<S proc_1>+<S proc_2>
|
||||
))
|
||||
(F17 f 1.0 1.0 (@f
|
||||
<S proc_1>
|
||||
))
|
||||
(F18 f 1.0 1.0 (@f
|
||||
<S proc_0>
|
||||
))
|
||||
(F19 f 1.0 1.0 (@f
|
||||
<S proc_1>
|
||||
))
|
||||
(F20 f 1.0 1.0 (@f
|
||||
<S proc_0>
|
||||
))
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <S proc_1>
|
||||
1 5 0 0 1.0 1.0 <S proc_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 <S proc_1>
|
||||
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 <S proc_0>
|
||||
0
|
||||
0
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
simple.cap
|
||||
simple.cc
|
||||
simple.mark
|
||||
simple.minval
|
||||
simple.outtype
|
||||
simple.parse
|
||||
simple.sc
|
||||
simple.string
|
||||
simple.val
|
||||
9
iface/gspn/examples/simple/.gitignore
vendored
9
iface/gspn/examples/simple/.gitignore
vendored
|
|
@ -1,9 +0,0 @@
|
|||
simple.cap
|
||||
simple.cc
|
||||
simple.mark
|
||||
simple.minval
|
||||
simple.outtype
|
||||
simple.parse
|
||||
simple.sc
|
||||
simple.string
|
||||
simple.val
|
||||
|
|
@ -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
|
||||
<S C_0>
|
||||
))
|
||||
(F3 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
(F4 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
(F5 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
(F6 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
(F7 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
(F8 f 1.0 1.0 (@f
|
||||
<x>
|
||||
))
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <x>
|
||||
0
|
||||
0
|
||||
|
|
@ -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
|
||||
<S proc_0> + <S proc_1>
|
||||
))
|
||||
(F4 f 1.0o 1.0 (@f
|
||||
<S proc_0>
|
||||
))
|
||||
(F5 f 1.0 1.0 (@f
|
||||
<S proc_0>
|
||||
))
|
||||
(F6 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F7 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F8 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F9 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F10 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F11 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F12 f 1.0 1.0 (@f
|
||||
<S proc_0>+<S proc_1>-<p>
|
||||
))
|
||||
(F13 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F14 f 1.0 1.0 (@f
|
||||
<p>+<q>
|
||||
))
|
||||
(F15 f 1.0 1.0 (@f
|
||||
<q>
|
||||
))
|
||||
(F16 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F17 f 1.0 1.0 (@f
|
||||
<q>
|
||||
))
|
||||
(F18 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F19 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F20 f 1.0 1.0 (@f
|
||||
<S proc_0>+<S proc_1>
|
||||
))
|
||||
(F21 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
(F22 f 1.0 1.0 (@f
|
||||
<q>
|
||||
))
|
||||
(F23 f 1.0 1.0 (@f
|
||||
<q>
|
||||
))
|
||||
(F24 f 1.0 1.0 (@f
|
||||
<p>
|
||||
))
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <S proc_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 <S proc_0>
|
||||
0
|
||||
0
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <map>
|
||||
#include <cassert>
|
||||
#include <cstring>
|
||||
#include "gspn.hh"
|
||||
#include <gspnlib.h>
|
||||
|
||||
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<const state_gspn*>(other);
|
||||
assert(o);
|
||||
return reinterpret_cast<char*>(o->get_state())
|
||||
- reinterpret_cast<char*>(get_state());
|
||||
}
|
||||
|
||||
virtual size_t
|
||||
hash() const
|
||||
{
|
||||
return reinterpret_cast<char*>(get_state()) - static_cast<char*>(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<AtomicPropKind, bdd> ab_pair;
|
||||
typedef std::map<AtomicProp, ab_pair> 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<const state_gspn*>(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<const state_gspn*>(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<const state_gspn*>(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_);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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 <string>
|
||||
# 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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
:
|
||||
1358
iface/gspn/ssp.cc
1358
iface/gspn/ssp.cc
File diff suppressed because it is too large
Load diff
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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 <string>
|
||||
# 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
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
:
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
:
|
||||
|
|
@ -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])
|
||||
])
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue