* iface/gspn/dcswavefm.test: New file.

* iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and
fmgspn-srg.
(fmgspn_rg_SOURCES, fmgspn_rg_CPPFLAGS, fmgspn_rg_LDADD,
fmgspn_srg_SOURCES, fmgspn_srg_CPPFLAGS, fmgspn_srg_LDADD):
New variables.
(TESTS): Add dcswavefm.test.

ChangeLog

+2003-08-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* iface/gspn/dcswavefm.test: New file.
+	* iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and
+	fmgspn-srg.
+	(fmgspn_rg_SOURCES, fmgspn_rg_CPPFLAGS, fmgspn_rg_LDADD,
+	fmgspn_srg_SOURCES, fmgspn_srg_CPPFLAGS, fmgspn_srg_LDADD):
+	New variables.
+	(TESTS): Add dcswavefm.test.
+
 2003-08-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/ltlast/formula.hh: Make it clear that ref() and unref()

iface/gspn/Makefile.am

@@ -15,7 +15,9 @@ check_PROGRAMS = \
   dottygspn-rg \
   dottygspn-srg \
   ltlgspn-rg \
-  ltlgspn-srg
+  ltlgspn-srg \
+  fmgspn-rg \
+  fmgspn-srg
 
 dottygspn_rg_SOURCES = dottygspn.cc
 dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
@@ -29,6 +31,14 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
 ltlgspn_srg_SOURCES = ltlgspn.cc
 ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
 
+fmgspn_rg_SOURCES = ltlgspn.cc
+fmgspn_rg_CPPFLAGS = -DFM $(AM_CPPFLAGS)
+fmgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
+
+fmgspn_srg_SOURCES = ltlgspn.cc
+fmgspn_srg_CPPFLAGS = -DFM $(AM_CPPFLAGS)
+fmgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
+
 EXTRA_DIST = \
   examples/DCSwave/DCSWave.def \
   examples/DCSwave/DCSWave.net \
@@ -41,7 +51,8 @@ EXTRA_DIST = \
 TESTS = \
   simple.test \
   dcswave.test \
-  dcswaveltl.test
+  dcswaveltl.test \
+  dcswavefm.test
 
 # Each test case depends on defs.
 check_SCRIPTS = defs

iface/gspn/dcswavefm.test

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

iface/gspn/ltlgspn.cc

@@ -4,6 +4,7 @@
 #include "tgba/tgbatba.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/ltl2tgba.hh"
+#include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/magic.hh"
 
 int
@@ -34,7 +35,11 @@ main(int argc, char **argv)
       spot::gspn_interface gspn(2, argv);
       spot::bdd_dict* dict = new spot::bdd_dict();
 
+#if FM
+      spot::tgba* a_f = spot::ltl_to_tgba_fm(f, dict);
+#else
       spot::tgba* a_f = spot::ltl_to_tgba(f, dict);
+#endif
       spot::ltl::destroy(f);
 
       spot::tgba* model        = new spot::tgba_gspn(dict, env);