|
| 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 2006 "Edinburgh" released on December 12, 2006. See The CADP Newsletter Nr. 6 for details.
So far, CADP 2006 "Edinburgh" has been found to be fairly mature and reliable except a few minor problems described below, for which we try to provide workarounds.
On July 26, 2007, an updated version named CADP 2006-a "Edinburgh" was released, which is almost the same as CADP 2006 "Edinburgh", but integrates the changes required to solve problems 2006-b, 2006-c, 2006-e, and 2006-f below. These changes are mostly intended to Ubuntu Linux users.
There also exist more recent beta-versions of CADP that solve all the issues listed in this page and bring many enhancements, including support for 64-bit machines. Please contact [email protected] to get access to the latest beta-version of CADP.
If your Cygwin software has been installed or updated since 19th December 2006, you may encounter strange behaviours with some CADP tools such as SVL:
-- svl 2.1 -- Frederic Lang, Hubert Garavel -- (c) INRIA Rhone-Alpes --
: command not found
: No such file or directoryvl/standard
svl: intermediate files are kept for diagnostics
svl: run ``svl -sweep "demo"'' to erase
This problem is due to the fact that Cygwin now contains version 3.2.9-10 of Bash, which breaks compatibility with previous versions. SOLUTION:
To solve this problem, the recommended solution is to set a new Windows system variable SHELLOPTS in the Cygwin startup script, which usually located in C:\\cygwin.bat. After the update, the contents of this script should look as follows:
@echo off
set SHELLOPTS=igncr
C:
chdir C:\\bin
bash --login -i
The cadp_cygwin.com shell-script (version 2.21 and above) was updated so as to set SHELLOPTS automatically in the cygwin.bat file.
Note: In an interactive bash shell (or in the the .profile or .bashrc files), it is not possible to assign variable SHELLOPTS as usual, e.g.:
SHELLOPTS="$SHELLOPTS":igncr
This triggers an error message stating that this variable is read-only after the bash shell is launched. However, it is still possible to assign it using a different syntax:
set -o igncr
export SHELLOPTS
However, we recommand to set SHELLOPTS directly in the cygwin.bat file. This will work is most cases (except when you are logging onto your Windows machine using the ssh server provided by Cywgin; in such case, you must add manually the "set -o" and "export" commands above in your ".bash_profile" startup file).
If the value of the $PATH environment variable does not contain "." (meaning, the current directory), EUCALYPTUS 2.6 produce an error message of the form:
/bin/sh: cannot execute...after clicking on a file and selecting "Execute" from the contextual menu. SOLUTION:
Edit file "$CADP/src/eucalyptus/eucalyptus.tcl" using a text editor and change line 4791 as follows:
4791c4791
< {Execute "[File_Name Execute]"}
---
> {Execute "./[File_Name Execute]"}
Due to the fact that Linux distribution Ubuntu 6.10 uses "/bin/dash" instead of "/bin/bash" for "sh" shells, there are some problems caused by difference of behaviour between "bash" and "dash".
Variable ``$CADP_CC'' is not set (default value is '-p: not found /usr/bin/gcc is /usr/bin/gcc') *** Can't find command ``-p: not found /usr/bin/gcc is /usr/bin/gcc'' ==> Add directory containing ``-p: not found /usr/bin/gcc is /usr/bin/gcc'' to your ``$PATH'' variable ==> or set variable ``$CADP_CC'' to use another C compiler (e.g., ``gcc'') Variable ``$CADP_PS_VIEWER'' is set to ``ggv'' *** Can't find command ``-p: not found ggv: not found'' ==> Add directory containing ``-p: not found ggv: not found'' to your ``$PATH'' variable ==> (otherwise you will not be able to use ``bcg_draw'') ...
In SVL, renaming does not work properly in some cases. For instance, demos number 25 and 37 do not run as expected.
These problems can be solved by applying some patches manually to a few script files contained in CADP 2006 "Edinburgh":
< WHICH=`type -p "$1"` --- > WHICH=`/bin/bash -c "type -p '$1'"`
Edit file "$CADP/src/com/cadp_echo" and change the last line as follows:
< echo "$@" --- > /bin/echo "$@"This will work in most cases (i.e., unless your $CADP directory is shared between Linux and Solaris machines; in such case contact us to get the latest version of file "cadp_echo").
Two changes have to be done in file "$CADP/src/svl/standard":
1256c1256
< echo "${SVL_SPACES}\""$2"\"""$4" >> "$1"
---
> "$CADP"/src/com/cadp_echo "${SVL_SPACES}\""$2"\"""$4" >> "$1"
1258c1258
< echo "${SVL_SPACES}""$2""$4" >> "$1"
---
> "$CADP"/src/com/cadp_echo "${SVL_SPACES}""$2""$4" >> "$1"
In CAESAR 7.0, the "-gradual" option does not work properly. It might increase the size (number of states and/or number of transitions) of the graph generated by CAESAR, whereas it should normally preserve or decrease this size.
Avoid invoking CAESAR 7.0 with the "-gradual" option. This problem will be solved in the next version of CADP.
Due to a change in behaviour of the "bash" shell present in the recent versions of Cygwin, the following error message is emitted when "cadp_web" or "tst" are run on Windows equipped with the latest versions of Cygwin:
$CADP/src/com/cadp_web: line 53: !/Microsoft: event not foundThis warning is annoying, but harmless. SOLUTION:
This problem can be solved by applying the following patch manually. Edit file "$CADP/src/com/cadp_web" using a text editor and remove lines 52-53:
# Pour Windows 95 avec IE 5.0 et Windows NT4 avec IE 2.0
PATH="$PATH:/Program Files/Plus!/Microsoft Internet"
On some recent versions of Cygwin, running Executor causes the following error message:
/cadp/src/com/cadp_cc -I. -I/cadp/incl -I/cadp/src/open_caesar -c /cadp/src/open_caesar/executor.c -o executor.o /cadp/src/com/cadp_cc executor.o bitalt_protocol.o -o executor -L/cadp/bin.win32 -lcaesar executor.o:executor.c:(.text+0x392): undefined reference to `_sleep' collect2: ld returned 1 exit statusSOLUTION:
Edit file "$CADP/incl/caesar_system.h" and change line 29:
#if defined (ARCHITECTURE_PC_WIN32)into:
#if defined (ARCHITECTURE_PC_WIN32) || defined (WIN32)This will solve the problem until the next stable release of CADP.
On recent versions of Ubuntu Linux (Feisty 7.04), CAESAR emits a torrent of error messages:
caesar -more '/bin/cat' -english -gc -monitor any.lotos -- caesar 7.0 -- Hubert Garavel (INRIA Rhone-Alpes) -- caesar: syntax analysis of ``any'' caesar: semantic analysis of ``any'' caesar: - processes binding caesar: - gates binding caesar: - types binding caesar: - signature analysis caesar: - sorts binding caesar: - variables binding caesar: - operations binding caesar: - functionality analysis caesar: restriction of ``any'' caesar: expansion of ``any'' caesar: type survey of ``any'' /tmp/caesar_11164.c:2:19: error: stdio.h: No such file or directory /tmp/caesar_11164.c:3:20: error: stdlib.h: No such file or directory /tmp/caesar_11164.c:4:20: error: unistd.h: No such file or directory /tmp/caesar_11164.c:5:20: error: memory.h: No such file or directory In file included from /usr/lib/gcc/i486-linux-gnu/4.1.2/include/syslimits.h:7, from /usr/lib/gcc/i486-linux-gnu/4.1.2/include/limits.h:11, from /tmp/caesar_11164.c:6: /usr/lib/gcc/i486-linux-gnu/4.1.2/include/limits.h:122:61: error: limits.h: No such file or directory /tmp/caesar_11164.c:7:23: error: sys/types.h: No such file or directory /tmp/caesar_11164.c:9:24: error: netinet/in.h: No such file or directory In file included from /tmp/caesar_11164.c:13: ../any.h:6:20: error: signal.h: No such file or directory ../any.h:7:20: error: string.h: No such file or directory /tmp/caesar_11164.c: In function `main': /tmp/caesar_11164.c:16: error: expected `=', `,', `;', `asm' or `__attribute__' before `*' token /tmp/caesar_11164.c:16: error: `CAESAR_RESULT' undeclared (first use in this function) /tmp/caesar_11164.c:16: error: (Each undeclared identifier is reported only once /tmp/caesar_11164.c:16: error: for each function it appears in.) /tmp/caesar_11164.c:31: warning: incompatible implicit declaration of built-in function `printf' /tmp/caesar_11164.c:61: error: `NULL' undeclared (first use in this function) /tmp/caesar_11164.c:64: warning: incompatible implicit declaration of built-in function `printf' /tmp/caesar_11164.c:66: warning: incompatible implicit declaration of built-in function `exit' /tmp/caesar_11164.c:69: warning: incompatible implicit declaration of built-in function `fprintf' /tmp/caesar_11164.c:111: warning: incompatible implicit declaration of built-in function `exit' #130 error in file ``.h'' during type survey: survey program is rejected by the C compiler quitThis problem is also detected by the "$CADP/com/tst" command:
This is ``tst'' version 1.203 (06/11/30 13:07:23) Current host is ``...'' Variable ``$CADP'' is set to ``...'' Current architecture is ``iX86'' Current operating system is ``Linux 2.6.20-16-generic'' Debian version is 4.0 Current gcc version is ``4.1.2 (Ubuntu 4.1.2-0ubuntu4)'' Current glibc version is ``2.5'' [...] Variable ``$CADP_CC'' is not set (default value is '/usr/bin/gcc') Command ``/usr/bin/gcc'' is ok *** ``/usr/bin/gcc'' failed to compile a minimal C program ==> Check that your C compiler is installed properly [...]SOLUTION:
The problem comes from the fact that the "build-essential" package containing C header files (such as "stdio.h" for instance) is not installed by default. You must install it manually using the following command:
sudo apt-get install build-essential
(contributed by Gwen Salaün, University of Malaga, Spain)
Back to the CADP Home Page