|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
The current stable version of CADP is version 2001 "Ottawa" released on July 13, 2001. See The CADP Newsletter Nr. 5 for details.
So far, CADP 2001 "Ottawa" has been found to be fairly mature and reliable except a few minor problems described below, for which we try to provide workarounds.
If you have not faced specific problems using CADP 2001 "Ottawa", we recommend that you continue using it until the next version is available.
There also exist more recent beta-versions of CADP that solve all the issues listed in this Page. If the proposed workarounds are not appropriate for you, please contact [email protected] to get access to the latest beta-version of CADP.
When upgrading to RedHat 7.2 a machine that was running an older version of Linux, it seems that the LICENSE file for CADP becomes invalid. Some CADP tools mail fail with an error message such as:
*007 protection violation
illicit attempt at using ``bcg_io 1.4'' on machine ``xxxxx''
no appropriate license
quit
SOLUTION:
The recommended solution is to regenerate a license file by invoking the following command:
rfl -f $CADP/LICENSE | mail [email protected]
We will return to you a new, valid license file. For more information, please consult the file $CADP/INSTALLATION_3.
On certain old versions of Linux (e.g., Linux RedHat 6.1 and 6.2), when using bcg_io to convert a graph from an ASCII format (e.g., ".seq", ".aut") to the BCG format, some labels are not parsed correctly. For instance, if a label contains an offer of the form "!0x00", this offer will be parsed as a floating-point number(!).
This problem comes from a bug in the "strtod()" function of the C library (glibc version 2.1.3) included in RedHat 6.1 and 6.2. Upgrading to glibc version 2.2.2 (included in Linux RedHat 7.1 or higher) will solve the problem.
Some minor problems have been reported about SVL 2.0:
SVL 2.0 could generate ".exp" files containing an "hide all but" operator, which is not available for this format. This was not accepted by the tools reading the EXP format (ALDEBARAN, EXP.OPEN, etc.).
Option -sh of SVL was not working properly (shell options passed to SVL were ignored).
When processing an instruction of the form:
"file.bcg" = rename A -> B in "file.aut"SVL would generate "file.bcg" and remove it afterwards. SVL was designed under the assumption that two files with the same prefix would necessarily represent LTSs with the same behavior. Hence, if "file.aut" had to be converted to the BCG format, then the converted graph was stored in "file.bcg", but considering that "file.bcg" was a temporary file that should be removed when SVL terminates.
Although documented in the SVL manual, this assumption proved to be over-constraining, as users may ignore SVL conventions or forget about them. To avoid user files from being removed or modified accidentally, this assumption has been abandoned in the new version of SVL, in which every temporary file is given a unique name.
A new version SVL 2.1 is available that processes the "all but" feature correctly using the BCG_LABELS tool. If you face this problem, a patch of SVL for CADP 2001 "Ottawa" can be obtained upon request to [email protected].
This problem is also solved in SVL 2.1.
This problem can be avoided by using a different name than "file.bcg":
"other_file.bcg" = rename A -> B in "file.aut"or by breaking the SVL instruction in two steps:
"tmp.bcg" = "file.aut"; "file.bcg" = rename A -> B in "tmp.bcg";
The "tst" command may emit a warning of the form
License file ``$CADP/LICENSE'' exists
*** No license exists for host ``xxx''
==> Read the INSTALLATION file to apply the RFL procedure
even if a valid license exists for the given host ``xxx''. This occurs when
the host name and/or the domain name contain upper case letters.
SOLUTION:
Ignore this spurious warning if you have a valid license. The problem will be solved in future versions of CADP.
Since the release of CADP 2001 "Ottawa" (July 2001), the Cygwin software has evolved; this is also the case for the GhostScript/GSView software. Therefore, some of the installation directives given for CADP 2001 "Ottawa" are no longer valid.
We have updated the installation directives. The most recent version (valid for Cygwin 1.3.10, GhostScript 7.04, and GSView 4.3) is available on-line from here.
Also, with the latest versions of Cygwin, you should use "$HOME/.profile" instead of "$HOME/.bashrc" as a startup file. In particular, we recommend to set the environment variables $CADP and $PATH in the ""$HOME/.profile" because this file is executed every time a Bash window is open by clicking on the Cygwin icon (the "$HOME/.bashrc" is no longer executed when a Bash window is started). Migrating to the new conventions can be done by typing the following command:
cd ; mv -i .bashrc .profile
When running CAESAR with the "-gc" option on RedHat 7.3 Linux, a segmentation fault occurs. If CAESAR is launched within the EUCALYPTUS graphical user interface, the following error message is likely to occur:
/bin/sh: line 33: 3921 Segmentation fault caesar -more '/bin/cat' -english -map -gc -monitor bitalt_protocol.lotosThis problem does not occur on RedHat 7.2 and earlier versions. SOLUTION:
This problem is located in the Boehm-Demers garbage collection library. CADP 2001 "Ottawa" uses version 5.3 of this library, which does not support on RedHat 7.3. Upgrading to the version 6.0 of the library solves the problem.
To avoid the problem, you can either:
seek must be permitted for a bcg_file in BCG_OPEN_BINARYDESCRIPTION-2:
Current operating system is ``CYGWIN_NT-5.1 1.3.18(0.69/3/2)''
:1:1: warning: "__STDC__" redefined
:9:1: warning: this is the location of the previous definition
:1:1: warning: "__STDC__" redefined
:1:1: warning: this is the location of the previous definition
:1:9: warning: "cpu" re-asserted
:1:13: warning: "machine" re-asserted
/lib/mingw/crt1.o(.text+0x111):crt1.c: undefined reference to `__p__fmode'
...
SOLUTION:
This problem is related to a recent decision of Cygwin developers to migrate the C compiler from GCC 2.95 to GCC 3.2.
The CADP libraries contained in CADP 2001 "Ottawa" have been produced using GCC 2.95 and have problems when linked against the new GCC 3.2 libraries.
To solve the problem, you can either:
DESCRIPTION:
On recent versions of Cygwin, Installator fails to send by e-mail the prototype license files. The problem is caused by the fact that the "blat.exe" binary (which is used by Installator to send e-mail) does not have the "x" (executable) bit set in its permission mode.
On older versions of Cygwin, this was not a problem since the ".exe" extension would automatically make "blat.exe" an executable binary, even if the "x" bit was missing. It seems that it is no longer the case for recent versions of Cygwin.
chmod a+x $CADP/src/installator/bin.win32/blat.exeand rerun Installator,
DESCRIPTION:
The Linux binaries included in CADP 2001 "Ottawa" cause a segmentation fault when launched on recent versions of Linux such as RedHat 9.0 and Mandrake 9.1 (although these binaries have been working properly for earlier versions of Linux, e.g., up to RedHat 8.0 and Mandrake 9.0 included).
To be sure about the problem, you can launch the following command and observe if a segmentation fault occurs:
$CADP/bin.iX86/hostinfo
$CADP/bin.iX86/cadp_hostinfo
This problem can be solved by upgrading to a recent version of CADP (precisely, CADP beta-version 2002-k or higher).
DESCRIPTION:
On recent Linux distributions, the "compress" and "uncompress" commands are no longer available by default. This causes a problem since Installator (i.e., the shell-script "installator.shar", a.k.a. "installator.com") --- as well as a few other tools of CADP 2001 "Ottawa" --- relies on the presence of "uncompress":
Extracting files from archive CADP_iX86_01_5f14b8f3.tar.Z Error while decompressing .../cadp/src/com/install_uncompress: line 31: uncompress: command not foundSOLUTION:
The "uncompress" command must be installed separately, as it is no longer bundled by default.
For distributions of Linux based on RPMs (e.g., RedHat, Mandrake), the package containing the compress and uncompress tools is called "ncompress" and can be found by asking rpmfind.net.
For other distributions of Linux (e.g., Debian), try asking Google with keywords such as "ncompress" and "debian".
The future versions of CADP will be modified so as to use "gzip -d" instead of "uncompress".
Back to the CADP Home Page