* iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg.

(eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS):
New variables.
(TESTS): Add dcswaveeltl.test.
* iface/gspn/dcswaveeltl.test: New file.
* iface/gspn/ltlgspn.cc [CEC]: Use emptiness_check.

ChangeLog

 2003-10-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg.
+	(eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS):
+	New variables.
+	(TESTS): Add dcswaveeltl.test.
+	* iface/gspn/dcswaveeltl.test: New file.
+	* iface/gspn/ltlgspn.cc [CEC]: Use emptiness_check.
+
 	* m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New files.
 	* Makefile.am (EXTRA_DIST): Add them.
 	* configure.ac: Call adl_ENABLE_DEVEL, adl_ENABLE_DEBUG, ad_GCC_OPTIM,

iface/gspn/Makefile.am

@@ -16,6 +16,7 @@ check_PROGRAMS = \
   dottygspn-srg \
   ltlgspn-rg \
   ltlgspn-srg \
+  eltlgspn-srg \
   fmgspn-rg \
   fmgspn-srg
 
@@ -31,6 +32,10 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
 ltlgspn_srg_SOURCES = ltlgspn.cc
 ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
 
+eltlgspn_srg_SOURCES = ltlgspn.cc
+eltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
+eltlgspn_srg_CPPFLAGS = -DCEC $(AM_CPPFLAGS)
+
 fmgspn_rg_SOURCES = ltlgspn.cc
 fmgspn_rg_CPPFLAGS = -DFM $(AM_CPPFLAGS)
 fmgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
@@ -52,7 +57,8 @@ TESTS = \
   simple.test \
   dcswave.test \
   dcswaveltl.test \
-  dcswavefm.test
+  dcswavefm.test \
+  dcswaveeltl.test
 
 # Each test case depends on defs.
 check_SCRIPTS = defs

iface/gspn/dcswaveeltl.test

+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/DCSwave .
+chmod +w DCSwave
+
+# G(ATTiIDLj => F(!SCj U SCi)) is true
+../eltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output
+
+# G(F(!SCj U SCi)) is false
+../eltlgspn-srg DCSwave/DCSWave '!G(F(!SCj U SCi))' ATTiIDLj SCi SCj > output \
+  || test $? = 1

iface/gspn/ltlgspn.cc

@@ -6,6 +6,7 @@
 #include "tgbaalgos/ltl2tgba_lacim.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/emptinesscheck.hh"
 
 int
 main(int argc, char **argv)
@@ -44,8 +45,22 @@ main(int argc, char **argv)
 
       spot::tgba* model        = new spot::tgba_gspn(dict, env);
       spot::tgba_product* prod = new spot::tgba_product(model, a_f);
+#if CEC
+      {
+	spot::emptiness_check empty_check;
+	bool res = empty_check.tgba_emptiness_check(prod);
+	if (!res)
+	  {
+	    empty_check.counter_example(prod);
+	    exit(1);
+	  }
+	else
+	  {
+	    std::cout << "not found";
+	  }
+      }
+#else
       spot::tgba_tba_proxy* d  = new spot::tgba_tba_proxy(prod);
-
       {
 	spot::magic_search ms(d);
 
@@ -59,8 +74,8 @@ main(int argc, char **argv)
 	    std::cout << "not found";
 	  }
       }
-
       delete d;
+#endif
       delete prod;
       delete model;
       delete a_f;