diff --git a/ChangeLog b/ChangeLog
index 87b8669e5..a5bf79606 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
 2003-10-01  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test: New files
+	* iface/gspn/Makefile.am (TESTS): Add them.
+	(XFAIL_TESTS): Add udcseltl.test.
+	* iface/gspn/example/udcs/udcs.net, iface/gspn/example/udcs/udcs.def
+	iface/gspn/example/udcs/udcs.tobs: New files.
+	* iface/gspn/Makefile.am (EXTRA_DIST): Add them.
+
 	* iface/gspn/Makefile.am (check_PROGRAMS): Add eltlgspn-srg.
 	(eltlgspn_srg_SOURCES, eltlgspn_srg_LDADD, eltlgspn_srg_CPPFLAGS):
 	New variables.
diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am
index ae4848a28..28ac28fc6 100644
--- a/iface/gspn/Makefile.am
+++ b/iface/gspn/Makefile.am
@@ -51,6 +51,9 @@ EXTRA_DIST = \
   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 = \
@@ -58,7 +61,10 @@ TESTS = \
   dcswave.test \
   dcswaveltl.test \
   dcswavefm.test \
-  dcswaveeltl.test
+  dcswaveeltl.test \
+  udcsltl.test \
+  udcseltl.test
+XFAIL_TESTS = udcseltl.test
 
 # Each test case depends on defs.
 check_SCRIPTS = defs
diff --git a/iface/gspn/examples/udcs/udcs.def b/iface/gspn/examples/udcs/udcs.def
new file mode 100644
index 000000000..5bf74dd90
--- /dev/null
+++ b/iface/gspn/examples/udcs/udcs.def
@@ -0,0 +1,78 @@
+|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>
+))
diff --git a/iface/gspn/examples/udcs/udcs.net b/iface/gspn/examples/udcs/udcs.net
new file mode 100644
index 000000000..90922624e
--- /dev/null
+++ b/iface/gspn/examples/udcs/udcs.net
@@ -0,0 +1,46 @@
+|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
diff --git a/iface/gspn/examples/udcs/udcs.tobs b/iface/gspn/examples/udcs/udcs.tobs
new file mode 100644
index 000000000..666e34ee3
--- /dev/null
+++ b/iface/gspn/examples/udcs/udcs.tobs
@@ -0,0 +1,9 @@
+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
diff --git a/iface/gspn/udcseltl.test b/iface/gspn/udcseltl.test
new file mode 100755
index 000000000..eb7a84169
--- /dev/null
+++ b/iface/gspn/udcseltl.test
@@ -0,0 +1,12 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/udcs .
+chmod +w udcs
+
+# F(ReP1 => F(gsP1)) is false
+../eltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output \
+  || test $? = 1
diff --git a/iface/gspn/udcsltl.test b/iface/gspn/udcsltl.test
new file mode 100755
index 000000000..56148940c
--- /dev/null
+++ b/iface/gspn/udcsltl.test
@@ -0,0 +1,12 @@
+#! /bin/sh
+
+. ./defs || exit 1
+
+set -e
+
+cp -R $srcdir/examples/udcs .
+chmod +w udcs
+
+# F(ReP1 => F(gsP1)) is false
+../ltlgspn-srg udcs/udcs 'F(ReP1 => F(gsP1))' ReP1 gsP1 > output \
+  || test $? = 1