* configure.ac: Output iface/gspn/defs.

* iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS).
(TESTS, check_SCRIPTS, distclean-local): New.
* iface/gspn/dcswave.test, iface/gspn/simple.test,
iface/gspn/defs.in: New files.
* iface/gspn/dottygspn.cc (main): Take the list of properties
of interest in argument.

ChangeLog

@@ -1,3 +1,13 @@
+2003-07-24  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* configure.ac: Output iface/gspn/defs.
+	* iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS).
+	(TESTS, check_SCRIPTS, distclean-local): New.
+	* iface/gspn/dcswave.test, iface/gspn/simple.test, 
+	iface/gspn/defs.in: New files.
+	* iface/gspn/dottygspn.cc (main): Take the list of properties
+	of interest in argument.
+
 2003-07-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* iface/gspn/examples/DCSwave/DCSWave.def,

configure.ac

@@ -28,6 +28,7 @@ AC_CONFIG_FILES([
   doc/Doxyfile
   iface/Makefile
   iface/gspn/Makefile
+  iface/gspn/defs
   src/Makefile
   src/ltlenv/Makefile
   src/ltlast/Makefile

iface/gspn/Makefile.am

@@ -22,4 +22,15 @@ EXTRA_DIST = \
   examples/DCSwave/DCSWave.tobs \
   examples/simple/simple.def \
   examples/simple/simple.net \
-  examples/simple/simple.tobs
+  examples/simple/simple.tobs \
+  $(TESTS)
+
+TESTS = \
+  simple.test \
+  dcswave.test
+
+# Each test case depends on defs.
+check_SCRIPTS = defs
+
+distclean-local:
+	-rm -rf testSubDir

iface/gspn/dcswave.test

@@ -0,0 +1,10 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/DCSwave .
+
+# ../dottygspn-rg DCSwave/DCSWave ATTiIDLj SCi SCj >output
+../dottygspn-srg DCSwave/DCSWave ATTiIDLj SCi SCj >output

iface/gspn/defs.in

@@ -0,0 +1,54 @@
+# -*- 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', be verbose.
+if test -z "$srcdir"; then
+   test -z "$VERBOSE" && VERBOSE=x
+   # 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

iface/gspn/dottygspn.cc

@@ -5,10 +5,21 @@ int
 main(int argc, char **argv)
   try
     {
-      spot::gspn_interface gspn(argc, argv);
-
       spot::gspn_environment env;
-      env.declare("obs");
+
+      if (argc <= 2)
+	{
+	  std::cerr << "usage: " << argv[0] << " model props..." << std::endl;
+	  exit(1);
+	}
+
+      while (argc > 2)
+	{
+	  env.declare(argv[argc - 1]);
+	  --argc;
+	}
+
+      spot::gspn_interface gspn(2, argv);
 
       spot::bdd_dict* dict = new spot::bdd_dict();
 

iface/gspn/simple.test

@@ -0,0 +1,23 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/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
+: