diff --git a/alliance/src/ctl/Makefile.am b/alliance/src/ctl/Makefile.am
index af437a64..d78b6217 100644
--- a/alliance/src/ctl/Makefile.am
+++ b/alliance/src/ctl/Makefile.am
@@ -1 +1 @@
-SUBDIRS = src
+SUBDIRS = src man5
diff --git a/alliance/src/ctl/configure.in b/alliance/src/ctl/configure.in
index 2b0da2d1..d18e9194 100644
--- a/alliance/src/ctl/configure.in
+++ b/alliance/src/ctl/configure.in
@@ -26,7 +26,7 @@ dnl           Almost ten years since I wrote this stuff, I just can't
 dnl           believe it
 dnl Date    : 01/02/2002
 dnl Author  : Frederic Petrot <Frederic.Petrot@lip6.fr>
-dnl $Id: configure.in,v 1.1 2002/04/18 15:24:28 ludo Exp $
+dnl $Id: configure.in,v 1.2 2002/08/05 13:35:35 ludo Exp $
 dnl
 dnl
 AC_INIT(src/ctl.h)
@@ -41,5 +41,6 @@ AM_ALLIANCE
 
 AC_OUTPUT([
 Makefile
+man5/Makefile
 src/Makefile
 ])
diff --git a/alliance/src/ctl/man5/Makefile.am b/alliance/src/ctl/man5/Makefile.am
new file mode 100644
index 00000000..ec8b7934
--- /dev/null
+++ b/alliance/src/ctl/man5/Makefile.am
@@ -0,0 +1,2 @@
+man_MANS  = ctl.5
+EXTRA_DIST = $(man_MANS)
diff --git a/alliance/src/ctl/man5/ctl.5 b/alliance/src/ctl/man5/ctl.5
new file mode 100644
index 00000000..f4e71ec2
--- /dev/null
+++ b/alliance/src/ctl/man5/ctl.5
@@ -0,0 +1,86 @@
+.TH CTL 5 "August 5, 2002" "ASIM/LIP6" "CTL file format of ASIM/LIP6/CAO-VLSI lab."
+
+.SH NAME
+.PP
+\fBctl\fP - Control Temporal Logic file format.
+
+.so man1/alc_origin.1
+.SH DESCRIPTION
+.PP
+This document describes the CTL file format used by \fBmoka\fP(1) for model checking
+of finite states machine description.
+
+.br
+This CTL file format subset is defined to enable classical CTL formulae description.
+.br
+A CTL file is made of two parts: a declaration part and a formulae statement part.
+
+.br
+The declaration part described types, constants, macros and all variables used in CTL formulae.
+It also describes assumption conditions and initial conditions that have to be applied
+by \fBmoka\fP(1) during the model checking.
+
+.br
+The formulae statement part described all the CTL formulae that have to be verified.
+
+.br
+All boolean VHDL operators are supported (see vbe(5)) and also the 8 CTL operators
+AF, AG, AX, AU, EF, EG, EX and EU. The CTL file format support also the imply
+boolean operator '->' and the equivalence operator '<=>'.
+.br
+.SH EXAMPLE
+.PP
+.nf
+
+
+--  user type definition
+
+   TYPE A_ETAT_TYPE IS (A_E0, A_E1);
+   TYPE B_ETAT_TYPE IS (B_E0, B_E1);
+
+--  variables definition
+
+   VARIABLE A_NS, A_CS : A_ETAT_TYPE;
+   VARIABLE B_NS, B_CS : B_ETAT_TYPE;
+
+   VARIABLE    ck       : BIT;
+   VARIABLE    data_in  : BIT;
+   VARIABLE    data_out : BIT;
+   VARIABLE    reset    : BIT;
+   VARIABLE    ack      : BIT;
+   VARIABLE    req      : BIT;
+
+-- example of a macros definition
+
+   DEFINE      def1     : BOOLEAN := ack='1';
+
+-- the assigned value can be a constant
+
+   DEFINE      c1       : BIT  := '1';
+
+-- the assumption condition
+
+   ASSUME   ass1  := (reset='0');
+
+-- the initial reset condition
+-- be careful, the assumption condition is not applied 
+-- to the initial conditions.
+
+   INITIAL  init1 := (reset='1');
+
+-- formulae description statement part
+
+begin
+
+   prop1 : EX( ack='1' );
+   prop2 : AG( req -> AF( ack ) );
+   prop4 : AU( req='1', ack='1');
+
+end;
+
+.SH SEE ALSO
+.PP
+\fBmoka\fP(1)
+
+.so man1/alc_bug_report.1
+