* iface/gspn/udcsfm.test, iface/gspn/udcsefm.test: New files.

* iface/gspn/Makefile.am (TESTS) Add them.
(check_PROGRAMS): Add emgspn-srg.
(efmgspn_srg_SOURCES, efmgspn_srg_LDADD, efmgspn_srg_CPPFLAGS): New
variables.
* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: Complete.

iface/gspn/Makefile.am

@@ -17,6 +17,7 @@ check_PROGRAMS = \
   ltlgspn-rg \
   ltlgspn-srg \
   eltlgspn-srg \
+  efmgspn-srg \
   fmgspn-rg \
   fmgspn-srg
 
@@ -36,6 +37,10 @@ eltlgspn_srg_SOURCES = ltlgspn.cc
 eltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
 eltlgspn_srg_CPPFLAGS = -DCEC $(AM_CPPFLAGS)
 
+efmgspn_srg_SOURCES = ltlgspn.cc
+efmgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS)
+efmgspn_srg_CPPFLAGS = -DCEC -DFM $(AM_CPPFLAGS)
+
 fmgspn_rg_SOURCES = ltlgspn.cc
 fmgspn_rg_CPPFLAGS = -DFM $(AM_CPPFLAGS)
 fmgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS)
@@ -63,8 +68,10 @@ TESTS = \
   dcswavefm.test \
   dcswaveeltl.test \
   udcsltl.test \
-  udcseltl.test
-XFAIL_TESTS = udcseltl.test
+  udcseltl.test \
+  udcsfm.test \
+  udcsefm.test
+XFAIL_TESTS = udcseltl.test udcsefm.test
 
 # Each test case depends on defs.
 check_SCRIPTS = defs

iface/gspn/udcsefm.test

@@ -0,0 +1,17 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+cp -R $srcdir/examples/udcs .
+chmod +w udcs
+
+# F(ReP1 => F(gsP1)) is false
+../efmgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1
+
+# !F(ReP1 => F(gsP1)) is true
+../efmgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1
+
+# !G(ReP1 => F(gsP1)) is false
+../efmgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1

iface/gspn/udcseltl.test

@@ -8,3 +8,10 @@ chmod +w udcs
 # F(ReP1 => F(gsP1)) is false
 ../eltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output
 test $? = 1 || exit 1
+
+# !F(ReP1 => F(gsP1)) is true
+../eltlgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1
+
+# !G(ReP1 => F(gsP1)) is false
+../eltlgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1

iface/gspn/udcsfm.test

@@ -0,0 +1,17 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+cp -R $srcdir/examples/udcs .
+chmod +w udcs
+
+# F(ReP1 => F(gsP1)) is false
+../fmgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1
+
+# !F(ReP1 => F(gsP1)) is true
+../fmgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1
+
+# !G(ReP1 => F(gsP1)) is false
+../fmgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1

iface/gspn/udcsltl.test

@@ -8,3 +8,10 @@ chmod +w udcs
 # F(ReP1 => F(gsP1)) is false
 ../ltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output
 test $? = 1 || exit 1
+
+# !F(ReP1 => F(gsP1)) is true
+../ltlgspn-srg udcs/udcs '!F(ReP1 => F(gsP1))' ReP1 gsP1 > output || exit 1
+
+# !G(ReP1 => F(gsP1)) is false
+../ltlgspn-srg udcs/udcs '!G(ReP1 => F(gsP1))' ReP1 gsP1 > output
+test $? = 1 || exit 1