|
| 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 |
What is the EXP language of CADP? Is the EXP language compositional? What is the difference between LOTOS NT and LNT? What are the differences between LNT2LOTOS and TRAIAN? Where is the reference manual for LNT? Does LNT support type aliasing (like "type ID is Nat")? How to debug a LNT specification that makes a segmentation fault? How to compile and execute an LNT specification? What is the largest graph minimized by BCG_MIN? A hidden transition between non observationally equivalent states disappears after observational minimization! Why does CAESAR a segmentation fault during the "simulation" phase?
| A. General questions |
| A.1. Installation and troubleshooting |
A.1.1. On which kind of machines/operating systems can I use CADP?
[Mon Mar 4 19:15:14 MET 2002]
Please, consult the "System requirements" Section in the CADP Home Page.
A.1.2. What is CADP's size?
[Mon Mar 4 13:50:25 CET 2002]
The entire CADP 2001 "Ottawa" distribution requires 81 Mbytes of disk space.
A.1.3. Where can I find the installation directives?
[Tue Oct 21 18:58:30 MEST 2003]
If your organization does not already have a CADP license, please fill in the Web form located at https://cadp.inria.fr/registration.
Otherwise, the appropriate information should already have been sent to you by the CADP authors. If you have lost it, please contact [email protected].
The installation is usually simple. You just have to run Installator, fill the required forms and click on OK buttons. Upon completion, Installator will send automatically a request-for-license (RFL) file to INRIA, and you will receive a reply with your "LICENSE" file that you will store as "$CADP/LICENSE".
A.1.4. How can I upgrade my version of CADP?
[Fri May 5 15:51:10 CEST 2023]
The easiest way is to run "installator" and click "Next" on each page. If your license has expired, you probably received a reminder with the download password. If not, just send an e-mail to [email protected] mentioning that you would like to upgrade.
A.1.5. How can I obtain a license number for CADP?
My administrator tried to intall the CADP tools but it still has the problem to enter the license number.
The license system of CADP is slightly different from the PC licensing scheme. You do not have to enter a license number yourself, but you have to run a command named "rfl" and we will mail you a license file. This is explained in the $CADP/INSTALLATION file, section II-B.
A.1.6. Who should be able to access the LICENSE file?
[Fri Jun 6 16:14:14 MET DST 1997]
The license file is set to be read for owner, group, whole and write for only owner. Does it have to set to be read, write and execute for owner, group and whole?
NO, -rw-r--r-- is OK
A.1.7. Is the software restricted to use in a subnet or on single hosts?
[Tue Jun 17 18:40:58 MET DST 1997]
Single hosts, but you can have many hosts in a unique license file.
A.1.8. What information do you need to create a licence file for us?
[Fri Nov 7 14:06:37 MET 1997]
The license file is automatically built using the "RFL" command shipped with CADP. This command will be invoked automatically when you launch the installator program.
A.1.9. How long is the license valid for?
[Fri Nov 7 14:06:37 MET 1997]
Licenses are granted for a whole year. This may seem short, but the CADP toolbox is constantly improved, so license files are granted for a year so that users upgrade every year.
This decision was taken in 1992, when we noticed an article contained benchmarks of aldebaran dating from 1989 !
A.1.10. How do I know when my licence will expire?
[Fri Nov 7 14:06:37 MET 1997]
Just take a look at the $CADP/LICENSE file. On every tool's line there are two dates: the first one is the date that the license was activated, the second one is the date on which it expires.
A.1.11. I get the following error: "License Error: The license for this product(SPARC ompiler C) has expired"?
[Fri Nov 7 14:06:37 MET 1997]
The problem does not come from the license for CAESAR, but from the license for your C compiler. You can either buy a license extension for your C compiler from Sun, or use the free compiler "gcc" instead (to do so, you have to do "setenv CADP_CC gcc" in your .login file). Make sure first, that gcc is installed on your machine.You should ask your system administrator. GCC is available by FTP on many sites.
A.1.12. The directory containing CADP on your FTP site is empty!
[Fri Jun 6 16:14:14 MET DST 1997]
I tried to download the toolset from your WWW page, but the directories were empty . It is intentional. The directories are not empty, their contents are hidden. Only registered users know the names of the files to download.
A.1.13. The CADP tools do not find the "cpp" command?
Run 'tst' and update your $PATH as explained
A.1.14. My license has expired. What should I do?
Licenses are usually granted for one year. If your version of CADP is one-year old, it is very likely to be obsolete and no longer supported. We do not store copies of obsolete versions and, therefore, cannot make or extend licenses for old versions. In such case, we recommend that you download the latest stable version of CADP. The numerous bug fixes and improvements are probably worth the effort of an FTP transfer! (See question A.1.4 on upgrades).
A.1.15. Error Message: "wrong global checksum"?
[updated Wed Aug 22 16:31:25 CEST 2012]
I tried to run caesar but it gave an error message which my administrator couldn't solve:
% caesar -english -analysis switch
-- caesar 5.1 -- Hubert Garavel (INRIA & IMAG) --
*016 protection violation:
falsified license
wrong global checksum
quit
The problem you have comes from the fact that the license file for CADP (you can consult this file in $CADP/LICENSE) has been somehow altered.
Please apply the following steps:
-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr/ -- This software is subject to copyright restrictions defined in -- the document "Contrat de mise a disposition de logiciels".
# end-of-file
A.1.16. Error Message: "wrong binary checksum"?
[Thu Sep 25 18:57:31 MEST 2003]
A.1.17. I am using CADP on several hosts. What is the easiest way to install it?
[Thu Sep 25 18:57:31 MEST 2003]
The best solution is to install CADP on a server that is accessible by all the clients (i.e., a volume shared by NFS or Samba), so that you do not need to install a different copy on each client.
This ensures that all the clients will use the same version of CADP, and simplifies the administrator's work.
When you run "rfl" on the server, you have to list all the clients that will be able to run CADP. For example:
rfl client1 client2 .... | mail [email protected]
A.1.18. The server and the clients have heterogeneous architectures. Does CADP supports it?
[Thu Sep 25 18:57:31 MEST 2003]
Yes. For example, you can have a Linux server, and Solaris and Linux clients that use the same installed version of CADP.
A.1.19. The clients are used as X terminals. Should I mention them in the "rfl" command?
[Thu Sep 25 18:57:31 MEST 2003]
No. In the "rfl" command, you must only mention clients that will run CADP on their own processor.
A.1.20. Error Message: "no appropriate license"?
[Thu Sep 25 18:57:31 MEST 2003]
It means that the machine on which you are running a CADP tool is not listed in the $CADP/LICENSE file. It might be the case that the name or the IP address of your machine has changed. In such case, it is necessary to obtain a new license for this host. This can be done by typing
rfl -f $CADP/LICENSE my_host | mail [email protected]
A.1.21. Can I install CADP on my home PC?
[Thu Sep 25 18:57:31 MEST 2003]
If your institution has already signed the license agreement, you can install CADP on your home PC and be granted a license for it. If you are a student, please ask your professor to provide us with a list of all students authorized to install CADP on their home PCs.
A.1.22. Would it be possible to use scp instead of rcp in rfl?
[Tue Sep 23 17:44:51 MEST 2003]
Versions of CADP after February 2003 provide support for rcp/rsh, scp/ssh and Kerberos' kcp/krsh.
A.1.23. My license expired. What should I do?
[Mon Nov 8 10:06:38 MET 2004]
Your can run Installator ($CADP/com/installator) ant then choose "keep the existing version". Then, follow the instructions given by Installator: it will allow you to update the different fields needed to get a new license, and also to require licenses for new machines.
You may also directly use rfl after having read the instructions given in $CADP/INSTALLATION_3; however, using Installator is easier and safer.
A.1.24. What's the procedure to get a localhost based CADP license for a laptop?
[Mon Nov 8 10:06:38 MET 2004]
Normally, you prepare a license for the laptop with one network address and it will continue working when the laptop is disconnected (i.e., when the laptop IP address becomes equal to 127.0.0.1).
A.1.25. What should I do when I encounter problems with CADP?
A.1.26. Where should I send bug reports?
Send them by E-mail to [email protected]
A.1.27. My administrator says that this CADP tool requires many environments that he might not have?
[Fri Jun 6 16:14:14 MET DST 1997]
Humm... CADP only relies on a few, standard external items (C compiler, X11, ghostview, etc.) All the less standard ones are shipped within the package. So far, CADP is really self-contained.
A.1.28. Which version of the CADP environment did I download?
[Fri Jun 6 16:14:14 MET DST 1997]
You can know this by looking at the end of the $CADP/VERSION file (or also the $CADP/HISTORY file).
You can also start the Eucalyptus graphical User Interface by typing "xeuca" and then click on the "Help" button, and then on the "Tool Versions" button.
A.1.29. Error Message: "Too many heap sections"?
[Mon Apr 21 15:48:56 MET DST 1997]
Under Solaris 2.5, I once got the following error message:
Too many heap sections: Increase MAXHINCR or MAX_HEAP_SECTS #187 system error during simulation: termination on ABORT signal (files completed) quit
Your system seems to be limited. Type the command 'limit', you may get something like this:
cputime unlimited filesize unlimited datasize 2097148 kbytes stacksize 8192 kbytes coredumpsize 0 kbytes vmemoryuse unlimited descriptors 64
To suppress these limitations, type the 'unlimit' command, which gives each ressource its maximum (physical) limit.
A.1.30. Error Message "libgc.a: warning: table of contents for archive is out of date; rerun ranlib(1)"?
[...]
The full error message was:
ld: /usr/local/caesar/gc/bin.sun4/libgc.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
ld: /usr/local/caesar/bin.sun4/libBCG_IO.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
ld: /usr/local/caesar/bin.sun4/libBCG.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
caesar : generation de ``bitalt_protocol''
caesar : - compilation du simulateur
ld: /usr/local/caesar/gc/bin.sun4/libgc.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
ld: /usr/local/caesar/bin.sun4/libBCG_IO.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
ld: /usr/local/caesar/bin.sun4/libBCG.a: warning: table of contents for
archive is out of date; rerun ranlib(1)
ld: Undefined symbol
_BCG_CREATE_EDGE_INDEX_2
_GC_dont_gc
_BCG_ET1_NEXT
_GC_scratch_alloc
_BCG_ET2_NEXT
etc.
The problem comes from a problem in your installation. You probably forgot the -p option when using the tar command, as explained in the INSTALLATION file. To correct this problem, type :
cd $CADP (cd bin.sun4 ; ranlib *.a) (cd bin.sun4.gcc ; ranlib *.a) (cd gc/bin.sun4 ; ranlib *.a) (cd tcl-tk/bin.sun4 ; ranlib *.a)
These commands must be executed under SunOS 4.*
A.1.31. I can't find lotos.open, Maybe my installation is not correct?
[Fri Nov 7 14:48:44 MET 1997 - updated Wed Feb 12 11:51:43 CET 2020]
lotos.open is in the 'com' directory, and not in the 'bin.sun*' directory. Please read the INSTALLATION file to be sure that your $path is correctly set.
A.1.32. On Windows, Installator displays "error reading "sockXXX": connection reset by peer"
[Wed Feb 27 19:47:59 CET 2008]
It is likely that a firewall is blocking FTP transfers. This is explained in the Windows installation page at http://cadp.inria.fr/windows.html
A.1.33. On Windows, I get errors messages "$'\r': command not found"
[Wed Feb 27 19:57:20 CET 2008]
When running a shell-script on Windows, if you obtain error messages such as:
/bin/sh $CADP/com/tst
/CADP2006-a/com/tst: line 2: $'\r': command not found
/CADP2006-a/com/tst: line 7: $'\r': command not found
/CADP2006-a/com/tst: line 9: $'\r': command not found
/CADP2006-a/com/tst: line 11: $'\r': command not found
/CADP2006-a/com/tst: line 13: $'\r': command not found
/CADP2006-a/com/tst: line 26: $'\r': command not found
/CADP2006-a/com/tst: line 37: syntax error near unexpected token `$'{\r''
'CADP2006-a/com/tst: line 37: `TAIL_LINE () {
etc.
then it is likely that you did not apply the "cadp_cygwin.com" shell-script after installing Cygwin. This is explained in the Windows installation page at http://cadp.inria.fr/windows.html
A.1.34. Why does CAESAR and/or CAESAR.ADT complain that "library file ``XXX.lib'' is unreadable"?
[Mon Nov 8 10:06:38 MET 2004]
This error occurs when the LOTOS code contains a directive of the form "library XXX endlib" and when there is no corresponding file named "XXX.lib", neither in the current directory, nor in the standard library "$CADP/lib". Check the following points to solve this problem:
A.1.35. The BCG tools do not find the "what" command !
Run 'tst' and update your $path as explained.
A.1.36. Error message: "bcg_file_area: include area does not exist ....."?
[Tue May 20 19:30:26 CEST 2008]
bcg_file_area: include area does not exist in the file in BCG_BEGIN_READ_AREA bcg_file_area: type area does not exist in the file in BCG_BEGIN_READ_AREA
These messages indicate that the BCG file is corrupted, and some parts of it are missing. This is usually a sign that the generation of the BCG failed was brutally interrupted (i.e., with a kill signal or a segmentation fault) or due to some other reason, e.g., because the memory is lacking or the disk space is exhausted. Remove the BCG file and generate it again.
A.1.37. Are there any restrictions on who can use CADP?
CADP is available to academic and research institutions and to commercial organisations for research purposes. If you are a university researcher working on a project with a commercial organisation, both the university and the company will probably need licenses. Contact us to discuss this.
We cannot grant licenses to individuals. For students who wish to use CADP on their personal PCs, this is permitted under the license granted to the institution, but the professor should contact us with a list of the students who require licenses for home use.
If you intend to use CADP for commercial products and your company is ready to purchase CADP, we can dicuss the necessary amendments to the contract, depending on your specific needs.
A.1.38. How do I get a license for a machine that is not connected to the Internet or cannot send mail?
If your machine is not connected to the Internet, you still need to run the rfl tool and send us the result. Run the tool as follows:
$CADP/com/rfl machine_name > rfl_output_file
Then send us rfl_output_file by some other means.
A.1.39. RFL fails because it cannot establish an RSH connection
Normally, rfl is programmed in such a way that it uses cp/sh instead of rcp/rsh on the localhost.
If your network security policy blocks use of rsh and rcp, you cannot use a single rfl command to generate the license request for all you machines. Instead, you must log in to each machine separately and run rfl. Then send all the license request files to us. We will concatentate the information and send you back a single license file.
If rsh permitted in your nework but rfl still fails indicating an rsh problem, it might be that you have given the fully qualified name of the machine (for example "mymachine.inria.fr") instead of just "mymachine". Type hostname and give to rfl the name given by hostname:
rfl `hostname`
A.1.40. How to get a CADP license for an additional machine?
There are two ways of doing this:
(1) If the new machine can access the binary files of your current CADP installation, you can run the following command:
$CADP/com/rfl current_machine_name other_machine | mail [email protected]
This will produce a new prototype license file containing the name
of your current machine and the new machine (if your current
CADP license is granted for several machines, you must put all their
names as arguments to the rfl command) and will send it to me.
I will reply with the license file asap.
(2) If not, you must install again CADP on your new machine using the graphical 'installator' tool (as you did for your current machine(s)).
A.1.41. How can I extend the license?
To extend your license please type the following command
$CADP/com/rfl mach1 ...possibly_other_machines_that_you_have... | mail [email protected]
A.1.42. How can I tell whether RFL worked? Running tst after it fails.
When RFL has finished, it displays the following message:
$COMMAND is done: your LICENSE file will be soon sent back to you by e-mail
You will not be able to use CADP until you have the licemse. If you try
to run the TST tool before the license is installed, you will see this
message:
*** File ``$CADP/LICENSE'' does not exist
==> Read the INSTALLATION file to apply the RFL procedure
A.1.43. RFL fails with "`tty` Ambiguous" message
This message indicates a problem with your shell initialization files (.login or .cshrc, for example). Check that you can do 'rsh' and 'rcp' from async1 to the other machines, and change your shell initialization files as necessary. Once rsh and rcp work, you should no longer have a problem with rfl.
A.1.44. RFL blocks at "RFL (phase 1): testing machine_name"
You are probably running RFL as root.There are often special rules for root, to prevent root from logging via rlogin/rsh. Try running RFL as an ordinary user.
A.1.45. RFL fails with scp usage message
If you have a symbolic link rcp -> scp, this can cause RFL to fail with a message such as the following:
* RFL (phase 2): asking machine1
* usage: scp [-pqrvBC46] [-F config] [-S ssh] [-P port] [-c cipher] [-i identity]
* [-o option] f1 f2
* or: scp [options] f1 ... fn directory
To avoid this problem remove the symbolic link.
A.1.46. I'm about to upgrade to a newer CADP. Can I run RFL from the old version so that I already have the license file when the installation is complete?
No, RFL reports some information about the version of CADP that you have installed, so you must run the RFL that is provided in the new distribution.
A.1.47. How can I get licenses for more machines?
You can run RFL once to generate the prototype license file for all the machines, as follows:
$CADP/com/rfl machine_1 machine_2 ... | mail [email protected]
We will reply with the final license file covering all your machines.
A.1.48. Error message; "No appropriate license"
This error message typically indicates that there is a mismatch between the host identity information and the CADP license was issued. Check that the license is installed on you machine was generated for that machine. Check that the hostname, hostid, domain name and IP address are exactly the same as they were when you ran the RFL license request tool (including the same case). If necessary, rerun RFL to request a new license.
A.1.49. Why has my CADP license expired?
The license of CADP are granted at most for one year and users should upgrade their CADP version once a year (some prefer upgrading more frequently). We do not have sufficient resources to handle bug reports coming from obsolete versions.
The good news is that you do not have to sign the paper contract each time you as to renew a license, but just once, for the first license.
A.1.50. Error message: "Wrong domain name"
Our network has changed to use NIS+ instead of NIS and the license file seems to be no longer valid. What's the easiest way to fix this?
You will need a new license file. Run RFL as usual.
A.1.51. Can I get a copy of CADP on CD-ROM?
No, CADP is only distributed through our FTP server, as described in https://cadp.inria.fr/registration.
A.1.52. Do diskless clients need licenses?
My CADP server is used by many students working on diskless clients and X terminals. Do these client systems need CADP licenses too? No, you only need licenses for client machines that have a processor and an IP address.
A.1.53. Server with two IP addresses
My CADP server has a second network card so that is can serve as license server for some other software, so it is configured with two IP addresses, one for each network it sits on. This causes problems when the CADP tools sometimes take the wrong IP address. I've modified the DNS configuration which improved things a bit, but there are still some problems. Is there a way of tweaking the license to say that it applies to the server and is valid with the two IP addresses?
There's no automatic way to do this, but we can generate you a special license that works for any IP address. Mention this when you next request a license.
A.1.54. Can I use CADP on a laptop with no fixed IP address?
Mobility is still quite new for CADP and we do not support it well. The tool indeed checks for IP number. So far we only support fixed IP addresses, but the tool accepts the special address 127.0.0.1 which means that the laptop is disconnected. So, a way to make it work is to disconnect the network cable.
If this is unpleasant, we can make a special license for you with "any_address".
A.1.55. Is it really necessary to run RFL remotely?
As a workaround, you can log in to each machine separately and run RFL locally and send is the separate license prototype files to concatenate and create the license file. However, this is time consuming both for you and for us, so if at all possible, run RFL once to generate a single prototype file for all you machines.
A.1.56. My laptop doesn't have FTP. How can I install CADP?
If you cannot temporarily use FTP (there are several versions available with free evaluation periods), the only solution is to install CADP elsewhere on a machine with FTP access, and then copy the content of the $CADP directory to your laptop by whatever method you usually use to transfer files. Then run rfl `hostname` on the laptop and send us the resulting file so we can generate the license for CADP on the laptop.
A.1.57. How can I check that installation and licensing was successful?
I'm new to CADP. It's all installed, including the license files, but how can I test that everything is working? (1) Read $CADP/INSTALLATION carefully.
(2) Run $CADP/com/tst and check the output, correcting anything it reports.
(3) Run $CADP/com/xeuca, which starts Eucalyptus, the graphical interface to CADP.
A.1.58. How can I check that I'm runnng the latest version of CADP?
Check the $CADP/LICENSE and $CADP/VERSION files to find out what version you are running. Then check the CADP web site at http://cadp.inria.fr for the date and number of the latest version (look in the "Latest News" box).
A.1.59. Can I rename the installation directory after installation and licensing?
Yes. You will have to change the value of $CADP for all users to reflect the new name.
A.1.60. Is it possible to install a new version of CADP while keeping the existing version?
We would prefer that you did not. We only support the most recent version. Although it is possible to have two copies of CADP installed on a system into two different locations, users must carefully set their $CADP environment variable, and we see many problems. Note that if you install a newer version using INSTALLATOR, it will remove the old version as part of the upgrade process.
A.1.61. Are there any special considerations when generating licenses for a demo system?
Make sure before you run rfl that the demo system is configured as it will be for the demo (IP address, host and domain names).
A.1.62. My laptop is dual-booted under Linux and NT. Can I install CADP just once and see it from both environments? How many CADP licenses do I need?
If you have a common partition that is visible in both environments, a single installation will work. Assuming you install CADP under Linux, to generate the license request, log in under Linux, check that the $CADP environment variable is defined correctly, and enter the command: rfl `hostname` > toto Then send us the toto file so we can create you a license. For further details, see $CADP/INSTALLATION_4.
A.1.63. Error "can't find a usable init.tcl" when installing on Windows
This usually indicates that Cygwin is not installed directly in "C:\", but is in a subdirectory of "C:\". The instructions given in http://cadp.inria.fr/windows.html explain how to install Cygwin as required by CADP, and how to remove old or unwanted versions of it.
A.1.64. No files visible in FTP directory
This is normal. This directory is not world readable, but if you have the download password and follow the directives for manual installation, you can download the files (unless you have a firewall restriction blocking FTP on your side).
A.1.65. Do I need to run RFL after INSTALLATOR?
No, if you use INSTALLATOR to install CADP the license request is done for you automatically. you only need to run RFL if you install CAP manually.
A.1.66. Errors running cadp_cygwin.com
After downloading cygwin, cadp_cygwin.com, as explained in the instructions for manual installation on Windows, I see various errors including the following:
> /cadp_cygwin.com: line 14: export: `PATH': not a valid identifier
> /cadp_cygwin.com: line 31: cd: /bin: No such file or directory
> /cadp_cygwin.com: line 41: syntax error near unexpected token `$'{\r''
> /cadp_cygwin.com: line 41: `UPDATE_CYWGIN_BAT () {'
Response: Make sure that the cadp_cygwin.com script was run correctly,
i.e., from a Cygwin window (and not a Windows command terminal), by
typing "/bin/sh cadp_cygwin.com" (and not simply "cadp_cygwin.com").
A.1.67. Can I run CADP on a virtual machine?
CADP can be installed in a virtual machine created using VMware Player on a Windows machine. Install Linux in the VM, then install CADP iX86 or x64 as normal for a Linux system. This type of installation is a useful alternative to the Cygwin/Windows configuration and can provide better performance.
A.1.68. Error message says license file is unreadable
Make sure that the license file is in $CADP/LICENSE and that it is readable (chmod a+r $CADP/LICENSE).
If it does not work, run the command
$CADP/com/tstand check the result.
A.1.69. Can I run CADP on my laptop when it is disconnected and connected?
Yes. Install CADP as normal while the system is connected. If you are using the INSTALATOR, this will generate a license request for the laptop with its current IP address. However, the tools also work with the "special" IP address 127.0.0.1. Edit /etc/hosts and include the line:
127.0.0.1 localhost.localdomain localhostThen edit /etc/rc.local and append the following line (replacing mydomain with your real domaim name):
domainname mydomain
A.1.70. On Windows, must CADP be in C:?
Ideally, yes, both Cygwin and CADP should be installed directly in C:. However, if you are short of space in the C: drive, you can move the man and doc folders of CADP, which are large, to another drive and create Cygwin symbolic links to them. Relocating other folders has not be tested so is not recommended. You can also save spece in C: by moving or removing some parts of Cygwin such as the documentation or /usr/share.
A.1.71. If I change my Linux installation, will my CAPD license still be valid?
I'm running CADP on a Linux system using Fedora Core 2. If I change to SUSE or some other Linux distribution, will my CADP still work? Will I need a new license. This is not something we have tested, but it's possible that CADP will continue to work, provided that the installation of the new OS does not change the partition where it is installed. The license will possibly continue to work but it is not certain. You will have to try and see!
A.1.72. Questions about installator.shar
(1) The file installator.shar does not appear to be an RMP package. Why not? This is because RPM only works for Linux systems and CADP is supported for other architectures so we need a format that works everywhere. (2) Is it necessary to uncompress installator.shar in Linux while .shar file is a kind of a shell file ? The .shar file is self-extractible, and it will download files from our FTP server. These files are compressed to save transfer bandwidth.
A.1.73. Error "couldn't set locale correctly" during manual installation on Unix
This is an operating system problem, not really linked to the CADP installation. The most likely cause is that you have replaced some standard Unix commands with GNU commands. Try running the TST shell scripts and correcting any problems it reports.
A.1.74. How can I tell what version of CADP I'm running?
Type the following command:
grep VERSION $CADP/VERSION | tail -1
A.1.75. Error "uncompress: corrupt input"
This error is displayed when the CADP distribution has been downloaded by FTP without setting the "binary" option. It is typically a problem when downloading from the INRIA FTP site to a Windows system, or between any Windows and Unix systems.
A.1.76. Will CADP run on my Linux system?
There are a lot of dependencies between CADP and Linux (or any operating system), including the version of the kernel and of glibc. The easiest way to tell whether your OS is compatible with CADP is to try it, as follows: (1) Copy the directory containing CADP from a system running CADP to the system running the OS you want to test. (2) Define $CADP and update your $PATH. (3) Run "$CADP/com/tst" and review the output, which will list any problems.
A.1.77. Why do I need to run the cadp_cygwin.com script? I don't want to change the environment or replace /bin/sh by bash
CADP requires that you use bash because /bin/sh contains a bug that causes problems for CADP (see http://sources.redhat.com/ml/cygwin/2000-09/msg01019.html and http://sources.redhat.com/ml/cygwin/2000-09/msg01022.html.
A.1.78. On Windows, CADP does not understand symbolic links
The CADP binaries are pure Win32 binaries, not linked against the Cygwin library, and therefore they do not understand Unix-like symbolic links. This can indeed cause problems if specifications or other input files are stored in a home directory mounted on a Unix file server. For example, you will need to start xeuca from the Windows drive that is the root of the Cygwin file system, and your working files will need to be accessible to xeuca without symbolic links.
A.1.79. Error message "ld terminated with signal 11 [Segmentation fault], core dumped"
This error is displayed when an object file (".o") generated by CADP on one system to copied to a system with a different architecture and linked. Object files are not portable between architectures.
A.1.80. CADP errors on Mac when name changes
In the default configuration of portable systems running Mac OS X, the name of the machine changes depending on whether or not it is connected to the network. In other words, the hostname is assigned dynamically. This can lead to error messages such as the following:
*011 violation de protection : utilisation illicite de ``caesar.adt 5.3'' sur la machine ``macbook.lri.fr'' nom de machine incorrect (``macbook.lri.fr'' au lieu de ``MacBook.local'') abandonThe solution is to run the $CADP/com/tst command, which will detect the problem and display instructions for defining a static hostname.
A.1.81. Error message "*015 protection violation: ... wrong Internet address 192.168.56.1"
This error was seen when running CADP on a laptop that was also running a virtual machine (in this case, Oracle Virtual Box). The solution is to deactivate the network device of the virtual machine.
A.1.82. Error message "*033 protection violation" on certain versions of Ubuntu
If you see this error message, the solution is described in the CADP forum. The URL is http://cadp.forumotion.com/t279-license-problem-on-ubuntu-1010-033-protection-violation
| A.2. The INSTALLATOR tool |
A.2.1. Can I install through a proxy server?
No, the FTP client in the current version of Installator does not know about proxies. You will have to use the manual installation procedure described in http://cadp.inria.fr/installator/noinstallator.txt.
A.2.2. How do I launch "installator.com" on a Win32 system?
This file is a Unix compressed archive, not an MS-DOS application, so it cannot be launched by double-clicking. To run it, open a Cygwin bash window and type the command:
/bin/sh installator.comor
/bin/sh installator.com -beta
A.2.3. Can I use Installator on a machine with no FTP?
The installation program has its built-in FTP client (written in Tcl). If this doesn't work for some reason, typically because your machine is behind a firewall, you can use the manual installation procedure.
A.2.4. What's the interface to the manual installation procedure?
If you use the manual installation procedure, which is described in there is no graphical interface. Instead you use shell commands.
A.2.5. Why does installation fail on Solaris with the message "stty: : Invalid argument"?
Check your .login file for any instruction concerning stty. Remove this instruction and restart the Installator and it will work.
A.2.6. Where should I store the installator.com file?
Anywhere except $CADP. The file installator.com, which does not belong to CADP but is downloaded by the user who wants to (re)install CADP, should not be stored in the $CADP directory, because if the user requests to uninstall CADP before reinstall it, then this will remove this file and the reinstall will become impossible.
A.2.7. Installator error message: "can't unset "state(data)": no such element in array"
We have not come across this error message: it looks like an FTP connection failure but it seems that the download has succeeded. Run the $CADP/com/tst command to check that the installation completed successfully.
| A.3. The TST tool |
| A.4. Questions about model checking |
A.4.1. Is there a way to generate automatically all paths in a LTS that lead to a deadlock?
[Tue Nov 4 17:53:47 MET 1997]
This is possible with the exhibitor tool, which can be used through the EUCALYPTUS graphical interface. Just click on the file in which you want search for deadlocks (this can be a LOTOS file, or a file containing an LTS, or a network of LTSs) and select "Find Deadlocks..." in the popup menu. In the window that opens, Select the exhibitor tool, and set the "Selected Execution Sequence" option to All.
A.4.2. How do you find out whether an action is reachable or not?
[Tue Nov 4 17:53:47 MET 1997]
Lets suppose in this case that we want to see if the action called "ERROR_ACTION" is reachable. There are several ways of getting this result.
<until> "ERROR_ACTION"
The command to type will then be:
lotos.open file.lotos exhibitor < toto.seq
bcg_io file.bcg -aldebaran - | grep ERROR_ACTION
But in this case, no diagnostic sequence leading to "ERROR_ACTION" is computed.
pot (<"ERROR_ACTION"> true)
Like exhibitor, evaluator can be used on the fly with lotos.open or on constructed graphs with bcg_open.
lotos.open file.lotos evaluator -l -d 8 -v toto.mcl
A.4.3. What is the maximum size of the graphs CADP tools can handle?
[Tue Sep 23 16:26:57 MEST 2003]
The size of the graphs or labelled transition systems (LTSs) that the tools can handle depends on the memory size of the machine. Usually, we manage to handle systems with millions of states and transitions.
| A.5. Questions about equivalence checking |
A.5.1. How can I check refinement with the CADP tools?
[Fri Mar 1 12:12 MET 2002]
QUESTION [Andreas Kerschbaumer, Graz University of Technology (Austria)]
How can I check refinement with the CADP tools? There are some simulation preorders available, however it seems that these are not appropriate for refinement checks. If A is simulated by B then B may be more non-deterministic; thus B may not be exchanged for A (simulation is not horizontally compositional?) and A is not refined by B. In CSP refinement is based on the failure model. Is there any tool for checking a failure refinement in CADP? If not, what kind of simulation checks are appropriate? Is there any work on comparison of the CADP checks and failure refinement?
ANSWER [Laurent Mounier, Verimag (France)]
You are right, the preorder relations available within CADP differ from the CSP notion of refinement. The CADP preorders are a strong ("bord") and a weak ("iord", "sord") version of Milner's simulation relation, which takes into account the branching structure of the processes. These preorders express that if S1<=S2 then S2 implements "at least" the behaviour of S1. CSP refinement is based on trace comparisons (including a notion of failure and/or divergence). It does not take into account the branching structure of the processes.
In general, these two notion are not comparable. But the simulation preorders available within CADP are congruences w.r.t. to parallel composition: if S1<=S2 then (S1||S) <= (S2||S).
I don't think that you can "simulate" CSP refinement using CADP options. You can approximate it by:
You will obtain an "observable trace containment" check, but without exactly taking into account the notion of failures (I guess?).
| A.6. Questions about performance evaluation |
| A.7. Documentation - Publications - Tutorial |
A.7.1. Where can I find documentation on CADP?
A.7.2. How to get an overview of the CADP toolset?
Invoke the Graphical User Interface (xeuca). Clicking on a file icon displays a menu that proposes all operations available for this file. Selecting an operation in the menu launches the corresponding tool(s). You can thus get an overview of the toolset, by clicking on different types of files.
A.7.3. Is there more documentation than in the man pages and in the $CADP/doc directory available?
[Fri Nov 7 14:06:37 MET 1997]
There are several Web pages, including this FAQ, which may help you:
There is a "Guided tour of CADP" Web page coming up soon, which explains how to use CADP through the EUCALYPTUS interface for newbies.
Another way of getting to know the toolbox, is by running through the demos that are shipped with the toolset: $CADP/demos .
A recent paper, Garavel-96 gives an overview of CADP. It is available
on-line at:
http://cadp.inria.fr/publications/Garavel-96.html
A.7.4. Demo 19 doesn't work: "Travelling crane - stop on upper end reached" .
[Wed Nov 12 16:17:28 MET 1997]
First of all, check your installation by running the 'tst' command. If no errors are signaled, then check that you do not optimize your compilations by using "gcc -O" or likewise. Your CADP_CC variable could be set to:
CADP_CC="/usr/local/bin/gcc -O"
Change the value of this variable to:
CADP_CC="/usr/local/bin/gcc"
A.7.5. I'm new to CADP: what's the best way to get started?
[Mon 4 Sep 11:32:31 MET 2000]
The best way to learn CADP is to use the graphical interface (type $CADP/com/xeuca). It also provides access to the manual pages for all the tools.
You can also try to run the demo examples (present in $CADP/demos).
There are also many papers (in $CADP/doc) describing the algorithms,
the tools and their applications.
| B. Questions about languages |
| B.1. The LOTOS language |
B.1.1. Where can I find ISO standards written in LOTOS?
You may find ISO standards written in LOTOS at the ISO's WWW site:
http://www.iso.ch .
Once you're at this site, click on <<ISO catalogue>>, then
click on <<International Standards>> and then use the
keyword search with the keyword "LOTOS" .
B.1.2. How can I split my LOTOS description into several files?
Two solutions:
B.1.3. How can I replace recursions on the left-hand side of disable?
[Fri Jun 6 16:14:14 MET DST 1997]
process P [...] (...) : noexit := G1 ... ; ... ; P [...] (...) [> B endproc
This program is not accepted because of the recursion on the left of the disable. You can solve this problem, in the case when B does not exit, by this code:
process P [...] (...) : noexit := (G1 ... ; ... ; exit [> B) >> P [...] (...) endproc
B.1.4. Visibility problem with values received on gates?
[Fri Jun 6 16:14:14 MET DST 1997]
In the following code, I get the error message "X not declared":
G ?X:NAT; P [...] (...) >> G !X ; stop
The solution to this problem is to write:
G ?X:NAT; ( P [...] (...) >> G !X; stop )
B.1.5. Is there an if-then-else instruction in LOTOS?
[Tue Nov 4 16:08:14 MET 1997]
There are several ways of writing "if V then B1 else B2 endif" in LOTOS, even though there is no explicit "if-then-else" instruction:
([V] -> B1) [] ([not (V)] -> B2)
You can replace V by a boolean variable:
let OK:BOOL = V in (([OK] -> B1) [] [not (OK)] -> B2)
#define if (let OK:BOOL = ( #define then ) in ([OK] -> ( #define else ) [] [not (OK)] -> ( #define endif )))
You can then write directly your conditional statement "if V then B1 else B2 endif"
B.1.6. Do you have tools that make LOTOS programming easier?
[Wed Mar 06 10:14:16 CET 2002]
The APERO tool, which is supported by the EUCALYPTUS graphical user interface, is a preprocessor that enables the use of compact notations that will later be expanded to standard LOTOS. The pre-processor is currently configured to enable to define simple data types, in a Pascal-like manner ("enum", "record", etc.). To obtain APERO, just send an E-mail to [email protected], asking him for it. APERO is free of charge.
COMPLEMENT [Solofo Ramangalahy, Bull (France)]
There also exist tools for application domains, e.g. DILL (Digital Logic in LOTOS), which uses the m4 macro processor.
Users can also develop specific pre-processing techniques to suit their own needs. But these solutions are adhoc. One can expect that the situation will improve with E-LOTOS, as the LOTOS commitee seems to address for remarks on "user-friendliness", e.g., regarding the data-types part of LOTOS.
B.1.7. What is LOTOS?
[Mon Nov 8 10:06:38 MET 2004]
LOTOS is an acronym for "Language Of Temporal Ordering Specification". The language finds its origin within the standardisation effort related to the Open Systems Interconnection (OSI) standard, initiated by the International Standards Organisation (ISO). The standards organisation recognized in the early 1980's that there was a clear need for an unambiguous statement of requirements for the OSI model that is free from implementation bias. Therefore, a special group was formed to produce a standard for a formal specification approach, to be used within the definition of the OSI standard. This effort led to two international standards for formal description techniques:
B.1.8. What is Basic LOTOS?
[Mon Nov 8 10:06:38 MET 2004]
Basic LOTOS is a simplified version of LOTOS that only describes processes without data, while "Full LOTOS" describes processes together with data (Full LOTOS is a value-passing process algebra).
B.1.9. Does LOTOS allow to hide actions based on both gate names and values?
[Mon Nov 8 10:06:38 MET 2004]
In LOTOS, you can only hide actions based on the name of gates. Indeed, the "hide" operator only accepts gates (in fact, hiding a gate has the effect of declaring the gate).
This is different from the hiding and renaming operators provided by the "caesar_hide_1" and "caesar_rename_1" libraries, and used in various tools such as Bcg_Labels, Generator, Reductor, SVL, etc: using these operators, you can hide and/or rename entire labels.
Note that E-LOTOS has a renaming operator that allows deep transformation on the entire label.
B.1.10. What is the semantics of LOTOS?
[Mon Nov 8 10:06:38 MET 2004]
LOTOS is based on the well-established mathematical process algebras:
and the algebraic specification language for abstract data types, ACT ONE, [Ehrig-et-al-85].
The process algebras provide a basis for the formal specification of the behaviour of a system, that allows unambiguous definition of:
Both synchronous and asynchronous communication can be specified in LOTOS. The abstract data type part of LOTOS allows implementation independent specification of data exchanged between processes. The mathematical foundations of LOTOS provide a solid basis for the formal analysis of specifications written in LOTOS and also for the development of reliable tool support, which is essential for critical applications.
B.1.11. Does LOTOS support object-orientation?
[Mon Nov 8 10:06:38 MET 2004]
The LOTOS language itself does not provide object-oriented features such as inheritance. However, since the language is used to specify processes (and (de) composition of processes), and focuses on the modelling of behaviour expressions and the interfaces to its environment (so-called gates),the language is quite close to object-oriented way of thinking (using objects and methods). A LOTOS process appears as a black box to its environment, where the environment has no information about its internal structure and mechanisms. LOTOS processes can only interact with other processes through its gates, effectively implementing a notion of data hiding.
However, current state-of-the-art object-oriented methods still lack the power to (formally) reason about the temporal properties of the models created (aka the order of events in the system). LOTOS provides a means to denote exactly which orderings of interactions (so-called events)are permitted.
Several attempts have been made to combine the ideas from both worlds, e.g. combining the hierarchical object-oriented design (HOOD) method with LOTOS. On one hand, the graphical notation provided by HOOD can be used as a means of communication by visualisation of the design, while the underlying LOTOS specification provides the necessary mathematical rigour to verify temperal properties of the same design. Similar combinations of HOOD and PetriNets and HOOD and Z exist as well.
B.1.12. Can LOTOS handle concurrency?
[Mon Nov 8 10:06:38 MET 2004]
LOTOS is extremely well-suited to denote concurrency between communicating processes. The CCS and CSP calculi form the core of the LOTOS language, which is also referred to as "Basic LOTOS".
This subset provides all necessary means to decompose the system into (communicating) processes and to define the observable behaviour of the process (e.g. with the environment or with other processes). This design can be refined, where processes are broken up into smaller processes, observable behaviour is defined and so on. As soon as the architecture of the design is laid down, the data types, of which instances are communicated between processes when an event occurs, can be defined using the abstract data type definition facilities provided by the "Full LOTOS" language (the ACT-ONE part).
B.1.13. Is LOTOS executable?
[Mon Dec 19 18:56:17 MET 2005]
By nature, LOTOS descriptions are executable. Several approaches exist to validate LOTOS descriptions by execution:
The CAESAR and CAESAR.ADT compilers translate LOTOS descriptions into executable code. In particular, the C code generated for EXEC/CAESAR ("-exec" option of CAESAR) can be used to connect a LOTOS specification to a real environment. See the paper by Garavel-Viho-Zendri-00.
B.1.14. What sorts of systems can be described in LOTOS?
[Mon Nov 8 10:06:38 MET 2004]
Obviously, any kind of reactive system that involves asynchronous concurrency. Typical application areas are:
B.1.15. Where can I find a LOTOS-mode for emacs?
[Tue Sep 23 11:03:14 MEST 2003]
A LOTOS-mode is included in CADP, you will find it in "$CADP/emacs". A READ_ME file explains how to install it.
B.1.16. Which subset of LOTOS is accepted by CAESAR and CAESAR.ADT?
[Tue Sep 23 11:10:14 MEST 2003]
The restrictions for CAESAR are described in the paper "$CADP/doc/*/Garavel-90-a.*". The restrictions for CAESAR.ADT are described in the paper "$CADP/doc/*/Garavel-89-c.*".
B.1.17. How should I handle probabilistic or timed transitions in a LOTOS specification?
To handle real numbers (time, probabilities, rates), there are two techniques:
| B.2. The EXP language |
B.2.1. What is the EXP language of CADP?
[Thu Nov 22 14:24:19 CET 2012 - H. Garavel]
The ".exp" files specify concurrent automata, which are synchronized using the operators belonging to different languages (for instance, synchronization vectors or parallel composition operators of the CCS, CSP, LOTOS, or LNT process calculi). The definition of the EXP format is given in the EXP.OPEN manual page.
B.2.2. Is the EXP language compositional?
[Thu Nov 22 14:35:45 CET 2012 - H. Garavel]
Yes. The EXP operators enable to combine LTSs (or Interactive Markov Chains) corresponding to individual system components that have been generated separately and then minimized. This is usually done transparently using SVL.
| B.3. The MCL (Mu-calculus) language |
| B.4. The SVL language |
B.4.1. Why does ALDEBARAN fail on some .exp files?
SVL automatically generates .exp files satisfying the general EXP format syntax described in the ALDEBARAN manual page. However, ALDEBARAN itself does not support the whole EXP format. In particular, ALDEBARAN does not accept .exp files containing "hide" operators in the scope of parallel operators (we call these hide operators "inner hides"). The ideal solution to this problem would be for ALDEBARAN to be modified. For now, it is up to the user to provide composition expressions that will not be generated as .exp files with inner hides when they are to be used as inputs of ALDEBARAN. Either use "generation" operations to generate sub-parts of the composition expression containing inner hide nodes, or move hide nodes towards the top of the composition expression.
B.4.2. Why using the parallel FC2 format may fail?
The program FC2OPEN is used to generate sequential FC2 from parallel FC2. FC2OPEN calls FC2OPEN2C that is not yet implemented. Moreover, the FC2TOOLS are not supported on some architectures.
| B.5. The XTL language |
[Fri Nov 7 14:58:40 MET 1997]
XTL is model-checking tool that takes a LTS n the .bcg format as input as well as a .xtl file containing temporal formulas. Using EUCALYPTUS, just click on a LTS file and select "Verify Temporal Formulas" in the menu. Then select the XTL tool.
B.5.2. Is it possible to have some additional documentation about XTL?
[Fri Nov 7 14:58:40 MET 1997]
The essential reference is the Unix manual page (man xtl), together with the examples ($CADP/demos/demo_{16,21,22,23}) and the predefined libraries ($CADP/src/xtl/*.xtl) of temporal logic operators.
The Unix manual is intended to be self-contained, and to provide the minimum amount of information necessary to understand the examples and the operators defined in the libraries. Some constructs of the language may seem quite unusual (e.g., the iterators "for..end_for"), but from my experience they provide a compact way to write graph traversals and thus to define various temporal operators.
For the moment, I suggest that you use the predefined temporal logic libraries (there is one implementing ACTL) until you will become more familiar with XTL; then, you may attempt to write your own temporal operators/notations (the macro processor, xtl_expand, may be very helpful).
B.5.3. How can I handle the data values contained in transition labels?
[Thu Sep 25 09:55:57 MEST 2003]
Theoretically, BCG and XTL can handle all user-defined sorts and functions of an original LOTOS specification. Yet, the labels of the BCG files produced by CAESAR only use simple sorts (i.e., booleans, integers...). Values belonging to user-defined types (such as enumerated types, structures...) are represented as character strings. In XTL formulas it is possible to handle boolean, integers and string values of transition labels. For instance, the label "SEND !0 !true !cons (0, nil)" is parsed as a gate "SEND" followed by three offers: a first with "0", a second with "true" and a third with the string "cons (0, nil)".
B.5.4. Is XTL able to give an error-trail when a property is not true?
[Tue Sep 23 16:57:29 MEST 2003]
There is an ACTL library (written in XTL by Charles Pecheur) which is able to exhibit diagnostic sequences witnessing the truth values of the formulas. You can find it in the "$CADP/src/xtl/walk*.xtl" files, and an example of use is given in "$CADP/demos/demo_25". Unfortunately, there is no detailed documentation about this library, except for the comments in the "walk*.xtl" files. There are also some informal explanations in the technical report "$CADP/doc/*/Pecheur-98.*".
B.5.5. Error: aucune possibilite de liaison pour la variable
The following request is not working:
<| fby on T:edge |> <| fby on T2:edge |>
if (T -> [ CREATE ?I:string !K ?V:integer _ where (X < V) and (V <
Y) ] and T2 -> [ DELETE ?I:string !K ?V:integer _ where (X < V) and (V
< Y) ]) then
print (I) fby print ("\n")
else
nop
end_if
The error message is:
#036 erreur pendant la premiere phase de typage des expressions : aucune possibilite de liaison pour la variable (ou fonction nullaire) BCG ``I'' [r1_expanded.xtl : 4] abandonWhat is causing the problem? It seems that the problem is caused by an ambiguity in the bindings of I and V in the program. In an instruction "if C then B1 else B2", if condition C is an action predicate, like "T -> [ PORTE ?x:T ]", the variables bound by C ("x" in this case) are only visible in branch B1.
Therefore, to export these variables, the action predicate must appear at a higher level than the condition C, that is to say, C must not contain Boolean operators on these action predicates (if it does, no variable will be exported by C). This is documented in the XTL XTL man page, section EXPRESSIONS, expression if-then-else.
In this specific case, the problem can be resolved by rewriting the code as follows:
<| fby on T:edge |> <| fby on T2:edge |>
if (T -> [ CREATE ?I:string !K ?V:integer _ where (X < V) and (V < Y) ]) then
if (T2 -> [ DELETE !I !K !V ]) (* same I, K, and V as T *) then
print (I) fby print ("\n")
else
nop
end_if
else
nop
end_if
| B.6. The LNT language |
B.6.1. What is the difference between LOTOS NT and LNT?
[Tue Jun 3 10:22:03 CEST 2014 - H. Garavel]
In the 90s, the LOTOS NT language (where "NT" stands for "New Technology") was implemented in the TRAIAN compiler. In 2005, the development of the LNT2LOTOS translator was undertaken. This translator used a slightly different version of LOTOS NT, also called LNT, as a shortcut for "LOTOS New Technology". As timed passed, the TRAIAN compiler remained stable, while the LNT2LOTOS translator and its input language was quickly evolving. Therefore, in 2014, the decision was taken to reserve the name "LOTOS NT" for the language accepted by TRAIAN, and to use "LNT" for the language accepted by LNT2LOTOS.
The CADP documentation and Web site have been updated to use LNT in place of LOTOS NT, taking into account that only LNT is supported by CADP. Be warned, however, that all papers published before Spring 2014 do not make such a distintinction, and use LOTOS NT and LNT as synonyms.
B.6.2. What are the differences between LNT2LOTOS and TRAIAN?
[Tue Jun 3 10:29:11 CEST 2014 - H. Garavel]
TRAIAN (Traian) is an early compiler for LOTOS NT. TRAIAN only implements the datatype part of LOTOS NT. Moreover, the LOTOS NT language accepted by TRAIAN is different from the LNT language supported by LNT2LOTOS. TRAIAN is not part of CADP, and most CADP users do not really need to use TRAIAN directly. However, they use it indirectly, as TRAIAN is used to develop many compilers present in CADP.
B.6.3. Where is the reference manual for LNT?
[Thu Nov 22 15:01:56 CET 2012 - HG]
You can find it here. Do not confuse it with the TRAIAN reference manual, which is based on the LOTOS NT language.
B.6.4. Does LNT support type aliasing (like "type ID is Nat")?
[Thu Nov 22 14:44:13 CET 2012 - H. Garavel]
Using LNT, you can create derived types (i.e., a type having the same structure as Nat but different from Nat) but you can not create alias types (in the sense that ID would just be a synonym for Nat and values of type ID and values of type Nat could be mixed without any explicit conversion).
Notice first that simply defining
type ID is Nat end typedefines an enumerated type ID with a single enumerated value Nat, which is probably not what is expected. Instead, one should write a subtype definition:
type ID is X:Nat where true end typeYou can also define a range type
type ID is range 0 .. 100 of Nat end type
B.6.5. How to debug a LNT specification that makes a segmentation fault?
[Sun Nov 25 13:49:19 CET 2012 - H. Garavel]
LNT being a strongly-typed language, a segmentation fault is likely to be caused either (1) by incorrect external C written manually and invoked within the LNT specification, or (2) by a non-terminating LNT function that enter into infinite recursive calls, or (3) a stack overflow done by a correct program using deep recursion.
Issue (3) can be diagnosed easily by enlarging the stacksize to a larger value (possibly, unlimited) using the shell "limit" or "ulimit" command and seeing if the problem still occurs. Unfortunately, this is not possible using Windows/Cygwin.
Issues (1) and (2) can be diagnosed using the C debugger. The main problem is to force the LNT tools to keep the intermediate files. To do so, set the environment variable $CADP_TMP to a know directory, and the $CADP_CC variable to a C compiler with debugging options, e.g.,
setenv CADP_TMP $HOME/debug setenv CADP_CC "gcc -g" mkdir $CADP_TMPor
CADP_TMP=$HOME/debug ; export CADP_TMP CADP_CC="gcc -g" ; export CADP_CC mkdir $CADP_TMP(see $CADP/INSTALLATION_2 file for details)
Then, consider the command that led to the segmentation fault. If you are using SVL, add the "-debug" option on the command line after svl. Then go into the directory $CADP_TMP, which should contain a subdirectory named, e.g., lnt.28293. Go into this subdirectory.
To reproduce the problem, type the command causing the segmentation fault, e.g.,
lnt.open MY_PROGRAM.lnt generator OUT.bcgor, if you have a particular main progress to specify:
lnt.open -root My_PROCESS MY_PROGRAM.lnt generator OUT.bcgThis should end with an error message of the form
lotos.open: running ``generator OUT.bcg'' for ``MY_PROGRAM.lotos'' Segmentation faultLaunch then the debugger on the "generator" program, e.g.:
gdb generatorand type the two commands to run the program and inspect the stack:
run OUT.bcg where
B.6.6. How to compile and execute an LNT specification?
[Tue Jun 3 10:31:11 CEST 2014 - H. Garavel]
CADP users should invoke LNT.OPEN to process their LNT specifications. LNT.OPEN is the recommended entry point and will invoke other tools (such as LPP and LNT2LOTOS) automatically.
| B.7. Other languages |
B.7.1. What is the current status of E-LOTOS?
[Mon Mar 4 15:13:15 CET 2002]
E-LOTOS has been adopted as an ISO/IEC International Standard (under the reference 15437:2001) in september 2001. See http://vasy.inria.fr/elotos
B.7.2. Do you plan to adapt CADP to E-LOTOS?
[Thu Nov 22 14:16:06 CET 2012 - H. Garavel]
CADP implements LNT, a pragmatic version of E-LOTOS. As far as we know, there was no implementation of E-LOTOS as such.
B.7.3. Are you aware of any model checking work in the context of Erlang?
Thomas Arts and other people from Ericsson have experimented with a translation of Erlang into Promela and with verifying the Promela code using the SPIN model checker. This is reported upon in a MSc thesis (http://www.ericsson.com/cslab/~thomas/Xjobb/christian.ps). The main outcome of the experiment was that Promela (and hence SPIN) is too far away from Erlang to really use them together. It is a little like using C to specify an Erlang program in.
Searching for a better specification language, they found mCRL, provided by CWI in Amsterdam (http://www.cwi.nl/~mcrl). A first use of mCRL was to manually specify Erlang programs and then use the EVALUATOR model checker of CADP to verify properties (http://www.ericsson.com/cslab/~thomas/papers/ifl2000.pdf and http://www.ericsson.com/cslab/~thomas/Reports/sen9910.ps).
Using a specification language is always a little drawback, because it takes you lots of extra work. The work may pay off in the end, but often it is just tedious, since the Erlang program can be seen as a specification as well. An automated translator from Erlang to mCRL was developed, which was able to handle a significant subset of Erlang: http://www.ericsson.com/cslab/~thomas/papers/fmics2001.pdf.
You can also take a look at some case studies mentioned on the CADP web site that use Erlang:
In the latest versions of CADP, LOTOS is still there, but other easier
languages are supported (such as FSP by Magee and Kramer, and also
LNT which is our next generation formal method).
[Fri Sep 26 18:19:47 MEST 2003]
True. If you are looking for the shortest execution path from the
initial state to a given state numbered S, the command
might not give you the shortest path. You should use:
[Fri Sep 26 18:19:47 MEST 2003]
This can be done by typing
[Fri Aug 1 10:52 MES 2003]
This is allowed in the definition of the .aut format (consult the
Aldebaran man page):
double quotes are not mandatory for labels that do not contain spaces
nor commas. Indeed, some tools (such as ALDEBARAN and BCG_IO) may omit
doubles quotes when not needed. You can check this by running a command
like:
[Mon Nov 8 10:06:38 MET 2004]
Use the bcg_io tool. You can consult the
bcg_io documentation.
For instance, to convert a .aut file to a BCG file, use:
This error message is caused by a memory overflow and indicates that
the memory available on your machine is not sufficient for the
aldebaran tool to perform the reduction. Consider using BCG_MIN instead,
which is likely to consume less memory. You will first need to convert
your input file to BCG format (see 15.4).
Yes, using the -ocla, -bcla, -pcla, etc. options, which display the
class equivalences after refinement. However, for certain cases there
can be initial phases of saturation that create or eliminate
transitions and can result in the classes not being entirely correct.
A better approach is to use BCG_MIN with the -class option, which
accurately records the class equivalences.
No, if you compare two LTSes using branching equivalence, and they are
not equivalent, there is no message besides FALSE.
One option would be to first minimize for branching bisimulation (using
either Aldebaran or Bcg_Min), then compare for strong equivalence, which
will produce a message indicating where the problem is.
As stated in the aldebaran
man page, the gate name must be enclosed in double quotes:
"
The -path option of ALDEBARAN produces a file in the SEQUENCE (.seq)
format, which can be converted to the BCG (.bcg) or AUT (.aut) format
using BCG_IO. For example:
[Mon Nov 8 10:06:38 MET 2004]
This occurs because BCG_DRAW does not handle optimally the case
when there are two arrows s1-a->s2 and s2-b->s1 relating two states.
Currently, both arrows are drawn as straight lines, which makes them
appear as a double-tipped arrow.
To separate the arrows, you can use the BCG_EDIT drawing tool (called
from the button "Visualize->Edit" of the XEUCA graphical interface).
Clicking with the middle mouse button on the arrow makes its "control
points" to appear; by dragging these points one of the arrows is
changed into a curve, and thus the two arrows can be separated.
No, there is currently no conversion from BCG format to xfig. BCG_DRAW
stores files in a special BCG PostScript format, which contains special
coded comments containing the list of states, arcs, etc. The format is
described in Tock-95.
With this information, it should be relatively easy to create an xfig
file from the BCG PostScript, however, you should be aware that the xfig
format often changes.
BCG (Binary Coded Graphs) is the binary format for LTSs that is
used in CADP (see "man bcg"). It is much more compact than a
textual format such as ".aut".
The BCG format allows one to store the values of state variables. However,
in the case of LOTOS, the variables present in the LOTOS description are
not observable in the corresponding graph: from a semantic point of view,
in the Labelled Transition System (LTS) model all useful information is
contained in transition labels and is not attached to states.
There are plenty of good semantic reasons for this choice, among which the
abstraction from a particular implementation (two LOTOS programs with
equivalent behaviours may have different variables) and the compositional
reasoning (a parallel component can be replaced by a simpler one, but with
an equivalent behaviour).
If you want to display information in the LTS, it is sufficient to modify
the LOTOS specification by adding a DEBUG gate on which you can send the
desired information (e.g., the values of certain variables in the current
state).
No, you cannot edit a BCG file with a text editor because it is a highly
compressed binary format designed to store graphs with billions of states
and transitions. You should use the BCG_DRAW, BCG_EDIT, BCG_IO tools or,
at a lower level (C code programming), the BCG_READ and BCG_WRITE APIs.
[Fri Jun 6 16:14:14 MET DST 1997]
Yes. Type:
[Mon Apr 21 13:52:32 MET DST 1997]
This happens in version Z. It has been solved in version 97a.
In version Z, the format of the ".aut" files generated by
ALDEBARAN had been modified unilaterally. Before version Z,
the edges in ".aut" files generated by ALDEBARAN were always
sorted by increasing number of the "from-states". Since
version Z, some options of ALDEBARAN produce ".aut" files
that are not sorted, e.g.:
This situation causes problems in various places. In particular
BCG_IO could not deal with non-sorted ".aut" files, which led
to the following error message:
The new version of BCG has been modified to tackle non-sorted
".aut" files. However, the BCG files now produced from ".aut"
files are now less compact than before (technically, their edge
area is encoded with format 1 instead of format 2).
Therefore, the recommended policy is to use BCG files rather
than ".aut" files. In particular, it is better to generate
directly a BCG file from CAESAR, rather than generating a
".aut" file first and convert it later to a BCG file.
Note: An unsorted ".aut" file can be sorted using the following
command: bcg_io unsorted.aut sorted.aut
The BCG_LABELS tool provides these features and operates on BCG files.
For instance,
You can also have renaming patterns, including regular expressions.
For instance,
Note that these renamings can also be performed using SVL scripts.
The first example above can be rewritten in SVL as follows:
[Mon Nov 8 10:06:38 MET 2004]
You first have to convert the .aut file into a .bcg file
Then, run bcg_min:
For further details, please consult the
bcg_min page.
[Thu May 19 17:13:16 CEST 2016]
So far, BCG_MIN 2.0 was able to minimize a huge BCG graph with 841
million states and 3.5 billion transitions. Minimization modulo strong
bisimulation took less than 8 hours and 83 GB of memory. Minimization
modulo branching bisimulation took less than 8 hours and 132 GB
memory.
[Mon Feb 28 16:05:16 MET 2005]
Reducing two strongly bisimilar BCG graphs modulo branching stochastic
bisimulation using BCG_MIN, precisely,
Indeed, due to maximal progress of hidden transitions in stochastic
systems, bcg_min may cut some stochastic transitions, thus making some
states (and even some parts of the graph) become unreachable from the
initial state. To remove those unreachable states, one can use
bcg_open and generator as follows:
[Thu May 19 16:14:25 CEST 2016]
A user was expecting that if there exists a tau-transition s1 -i-> s2
in the input graph and if states s1 and s2 are not observationally
equivalent, then there should exist a tau-transition from the
equivalence class of state s1 to the equivalence class of state s2
in the minimized graph.
This affirmation is not correct.
Recall that observational minimization is done in three steps:
(1) tau-expansion, which consists in computing the transitive
closure of the tau-transition relation; basically, a transition
s1 -i-> s2 is added for each sequence of transitions s1 -i+-> s2
(2) branching minimization of the tau-expanded state graph
(3) elimination of redundant tau-transitions, which is somehow the
inverse of tau-expansion: a tau-transition s1 -i-> s2 is redundant
if there exists a sequence of at least two tau-transitions
s1 -i+-> s2
Therefore, redundant tau-transitions of the input graph will not
map to tau-transitions in the minimized graph. This can be illustrated
concretely on the following graph (in AUT format):
Observational minimization thus produces the following graph:
This also illustrates why branching bisimulation should be preferred
to observational equivalence:
The price to pay is that graphs minimized modulo branching bisimulation
may have few more states and transitions than graphs minimized modulo
observational equivalence, because the latter relation is weaker than
the former. In practice, however, the graph size difference (if any)
is generally small.
Running BCG_OPEN in two different windows caused the following problem:
Running a single instance works fine.
If both instances are running in the same directory, it is possible that
there are conflicts between generated files. It is advisable to run only
one command at a time in a given directory.
[Wed Nov 12 16:17:28 MET 1997]
You man find relevant documentation in the "bcg_write" man page. This
will show how to write BCG files. At compile-time, you must use the
following flags:
See file $CADP/src/open_caesar/generator.c for an example of BCG
output.
The BCG format is not documented. This is a deliberate decision on the
part of the team, because it is a research topic for us and we reserve
the right to change and evolve the format to handle new problems without
being disturbed by other implementations. For example, recently we modified
the format to move to 64-bit, while preserving backward compatibility with
version 1.0 dating from 1993.
A BCG should be seen as an abstract object (as is the case for a PDF or
GIF file, for example) that can be manipluated with APIs. The key APIs,
both documented in a man page, are bcg_read and bcg_write.
Yes. When you create a BCG file using BCG_WRITE, you can add a comment
that is a text zone, or concatenate text with an existing zone. For
details of how to do this, look at the information on the
BCG_IO_WRITE_BCG_BEGIN() function in the
bcg_write man page.
The comments can subsequently be displayed using BCG_INFO.
It is very likely that your filesystem is full, so that the ".c"
file generated by CAESAR has been truncated. Check your console
window for "file system full" error messages. Then, remove some
files to gain space on your disk, or move to another directory
with more space (e.g., /tmp). An other approach would be to convert the
.aut files to .bcg by using the bcg_io tool (this divides the size by
10 to 20).
[Fri Mar 14 15:21:14 MET 1997]
Your LOTOS description is too large. CAESAR has not enough memory to
build the corresponding Petri net. You can try to use CAESAR with
the "-gradual" option. If it does not succeed, try to reduce the number
of parallel processes in your description.
[Mon Apr 21 13:52:32 MET DST 1997]
1. A lot of work has been done lately to improve CAESAR's speed. In the
97a version, CAESAR 5.2 is much much much faster than CAESAR 5.1 in
version Z (* up to 30 times faster !!!! *).
2. Under Solaris you may change CAESAR's compilation options, to
include compilation optimisations. We recommend you use the '-xO4'
option (caesar -cc 'cc -xO4') under Solaris 2. The compilation is slower
(15 minutes sometimes) and requires a lot of swap space. If you can't
compile with -xO4 try -xO3 or -xO2.
3. You may also accelerate the code by changing the sizes of the HASH
Tables (CAESAR_STATE_HASH_SIZE and CAESAR_POSITION_HASH_SIZE), to do so
you must change CAESAR's compilation options:
caesar -cc 'cc -CAESAR_STATE_HASH_SIZE=xxxxxx ' where xxxxxx is the new
size of the HASH table. We recommend you use the closest prime number to
the expected number of states. Another way of doing this is to type
setenv CADP_CC "/opt/SUNWspro/cc -DCAESAR_STATE_HASH_SIZE=xxxxxx" before
running CAESAR.
By default, the HASH size is 131,071.
[Fri Dec 5 10:13:33 CET 2008]
CAESAR doesn't always produce the minimal graph (this problem is a
difficult one, and it is even undecidable in the case of arbitrary
graphs). You can reduce the graph produced by CAESAR or CAESAR.OLD
by using BCG_MIN or REDUCTOR.
[Mon Apr 21 13:52:32 MET DST 1997]
This problem occurs under Solaris 2.* when the swap size is too small.
To know the swap size type "$CADP/com/swapsize". The swap size should
be 2-3 times larger than your RAM.
This problem also happens when the /tmp directory is also the swap
device and there is not enough room left in this directory.
First, try to clean /tmp in order to have more disk space
If this does not succeed, try to set the CADP_TMP environment variable
to another directory (e.g., setenv CADP_TMP .)
[Mon Dec 19 19:21:18 MET 2005]
When you generate a BCG file, you can use the -monitor option of
CAESAR, GENERATOR, REDUCTOR. This opens a monitor window, with info
on the progression of the graph construction.
After the BCG graph is generated, you can know about its size by
typing
[Tue Nov 4 17:33:45 MET 1997]
This problem occured with the following LOTOS code:
Process P is recursively instantiated through a parallel composition
operator. This is rejected by CAESAR because it gives raise to an
infinite number of parallel processes. The solution is to use only a
fixed number of parallel instances, as in:
or
[Tue Nov 4 17:33:45 MET 1997]
if the "process recursion is not allowed on the left and right hand
part of |[...]|, nor on the left hand part of >> and [>" then will the
following specification work properly?
This is perfectly allowed: ManagementApplications and
ManagementPlatform can be recursive themselves. If the restriction
phase of CAESAR does not complain, it is OK.
What would not be allowed is the following:
[Tue Sep 23 17:53:36 MEST 2003]
The "-root" option of CAESAR expects a process without
value-parameters (see the man-page for CAESAR). An instantiation to
process P' with value-parameters should be encapsulated in the
definition of another process P without value parameters, to which the
"-root" is applicable.
[Tue Sep 23 16:29:38 MEST 2003]
The size of the labelled transition systems (LTSs) that the tools can
handle depends on the memory size of the machine and on the size of
the states of the LOTOS specification. Usually, we manage to handle
systems with millions of states and transitions.
If you cannot manage to generate the LTSs in a reasonable time and/or
memory, you can try to perform compositional generation using the
caesar (with option -root), bcg_min, and exp.open tools of CADP.
For more details about compositional generation, you may consult the
sections about OPEN/CAESAR in the CADP FAQ
as well as the examples in "$CADP/demos/demo_{10,11,20}".
[Wed Apr 27 09:32:33 MEST 2005]
The EXEC/CAESAR environment is described in section 4 of the paper
"$CADP/doc/*/Garavel-Viho-Zendri-00.*".
More technical information can be found in the
CAESAR manual page and the file
"$CADP/incl/caesar_kernel.h".
Finally, demonstration $CADP/demos/demo_19 (production cell) demo 19
illustrates the use of the EXEC/CAESAR environment.
There is no simple answer to this question. One can guess an upper bound
on the number of states using different techniques (either from the
structure of the algebraic terms, or from the structure of the Petri
net generated: the PREDICTOR tool uses the latter approach).
The number of states strongly depends on the compiler, which is free
to generate large or small graphs, provided that they are strongly
bisimilar. The CAESAR compiler is regularly optimized in order to
reduce the number of states generated from LOTOS descriptions.
[Wed Jul 18 13:40:26 CEST 2012 - Hubert Garavel and Wendelin Serwe]
There are several possible causes. One cause is that you have provided
a hand-written implementation in C of abstract data types or functions
and that this implementation is incorrect.
Another cause is that the system stack size overflows due to recursive
function calls. This may occur if your LOTOS specification is too
complex, either in the data types (namely, recursive functions invoked
on large data structures such as very long lists)
or in the behaviour part. In such case, increasing the maximal size
for the stack or removing existing size limitations
("unlimit stacksize" in csh/tcsh) may solve the problem. If not,
please contact [email protected]
Run 'tst' and update your $path as explained or invoke CAESAR.ADT
with option -indent
[Fri Mar 14 17:09:09 MET 1997]
The current version of CAESAR.ADT does not generate code for
parameterized and actualized types. You have to actualize them by hand,
by duplicating the code of the parameterized type and substituting the
formal sorts by the actual ones and the formal operations by the actual
ones. Sorry for the inconvenience.
Yes, the 'renamedby' construct is handled properly.
[Fri Mar 14 15:21:14 MET 1997]
The LOTOS code is in the directory $CADP/lib.
For the LOTOS types that are declared as "external" (in files
"$CADP/lib/X_*.lib") , the corresponding implementation in C is in
directory $CADP/incl (in files "$CADP/incl/X_*.h").
For the X_*.lib files, do not forget to include the corresponding X_*.h files in
your .t or .f file.
[Wed Oct 22 11:45:32 MET DST 1997]
This error message appeared for old versions of CAESAR.ADT prior to
version 2.5 released in April 2004 (see entry #903 in the $CADP/HISTORY
file for details). It no longer appears after CAESAR.ADT 2.5, since
recent versions of CAESAR.ADT can now generate iterators for any
finite sort (unless the user declared this sort as "external" or
provided a hand-written iterator for it in the ".t" file).
However, the new version of CAESAR.ADT will still generate no iterator
for LOTOS sorts with an infinite domain. The remainder of this
paragraph explains how to address this problem. Note that it uses
old-style iterators, whereas new-style operators should now be
preferred.
If CAESAR complains about the impossibility to enumerate the values
of some sort S, the causes of this problem are:
There are several solutions to this problem.
We will study them here on the following example:
the sort `Queue': a FIFO queue of natural numbers.
The first thing to do, as our sort is not finite, is to restrain it
to a finite subset, otherwise it would be impossible to generate the
finite state machine.
We will thus limit the size of the queue to 2 elements, so it may take
any of the following values:
1. The first solution is a LOTOS-based one: you modify your LOTOS
description to add a process in parallel which feeds your LOTOS
description with elements of the desired sort (in this example, Queues).
When the description does "G ?Q:Queue" it should be synchronized with
a feeder process that sends !NIL, CONS (X, NIL), etc etc etc . This
is relatively easy to do in LOTOS:
We recommend you modify the Natural iterator to reduce it from 0..255
to 0..5, in order to avoid state space explosion with this feeder.
2. The second solution is to write the iterator in C yourself. This
is more complex than the first solution. The C iterator is a loop
instruction over the desired sort:
This is easy to do on simple sorts (booleans, integers, etc ...).
With other complicated sorts, you must find a way of iterating the
different elements of the sort. In this case, an easy way of iterating
over them, is to first to build an array containing all the elements of
the sort, and then to enumerate the elements of the array.
This is the approach we will take here.
To use a C iterator, do the following:
3. The last solution is to use CAESAR's -exec option which calls a
C procedure instead of an iterator to obtain a value for X. Here,
there is no iteration, just one value of X is given by the C function.
Wherever there are External Gates in the LOTOS description, a C function
named "name-of-the-external-gate" is called. In this C function,
you may interact with the outside world (useful for prototyping),
for instance, you may prompt the user for a value, or you can just
compute the value and return it.
For more details on EXEC/CAESAR see the paper Garavel-Viho-Zendri,
Caesar's man page, as well as $CADP/demos/demo_19 (production cell).
[Tue Nov 4 17:13:01 MET 1997]
These annotations are explained in "$CADP/doc/Garavel-90-a.ps". They
follow sort declarations and allow the correspondence between abstract
LOTOS sorts and concrete C types. With this special comment, the user
provides the names of the C functions implementing the abstract LOTOS
sorts. Since version X (see improvement #206 in $CADP/HISTORY) these
comments are optional and can be safely ommitted.
This does not apply to the (*! constructor *) annotation, which is
mandatory. If you forget all (*! constructor *) annotations for a
given sort, CAESAR.ADT will assume that this sort is external and
CAESAR will ask you for a hand-written implementation in C.
[Tue Oct 21 13:04:31 CEST 2008]
Let's suppose that the name of your LOTOS file is foo.lotos.
To restrict the enumeration of integers, you must create a file
called foo.t containing the following lines:
With previous versions of CADP (before 2004), you should have
used the following lines:
[Sat Sep 27 11:51:15 CEST 2008]
The Y_* files are not directly compilable. They are rather "pattern"
files which serve as a model. You have to edit them slightly. For
Y_QUEUE and Y_SET, you have to replace the LOTOS type (i.e., module)
Element and the LOTOS sort (i.e., type) Elem, respectively, by the
type and sort of elements you want to have in the queue or the set
(e.g., type NaturalNumber and sort Nat, respectively).
[Wed Nov 12 15:45:20 MET 1997]
The best way to do this is to create a symbolic link from the current
directory to the library file you wish to use.
[Wed Nov 12 15:45:20 MET 1997]
In a short-circuit "and", the left expression is only evaluated if the
right expression is true (like the "and then" operator in ADA).
In a short-circuit "or", the left expression is only evaluated if the
right expression is false (like the "or else" operator in ADA).
This is not very standard in LOTOS, but you can do it easily using
CADP. All you have to do is to use the X_BOOLEAN library instead of the
BOOLEAN library. Just replace the following line of your LOTOS
description:
with:
and create .t file containing the following lines:
and a .f file containg the line:
In the X_BOOLEAN library, the "and" and "or" operators are always
short-circuit.
[Thu Nov 28 09:35:49 MET 2002]
CAESAR catches the SIGTERM signal (15), and then tries to close all files (e.g., the BCG file containing the automaton being generated) properly.
[Thu Nov 28 10:31:25 MET 2002]
You add special comments "implementedby" to the constructors.
[Thu Nov 28 10:31:25 MET 2002]
In the ``.t'' file, you cannot use all the C types generated from your LOTOS code, because some of these types could depend themselves of the external types defined in the ``.t'' file. Yet, there are two important families of types that Caesar.adt defines before including the ``.t'' file and that you can use in the ``.t'' file itself:
However, more complex types cannot be used in your external types.
[Thu Nov 28 10:31:25 MET 2002]
Yes. If you are using the predefined NATURALNUMBER library of the LOTOS
standard (located in $CADP/lib/NATURALNUMBER.lib), you get no
support for number notations. You are supposed to write succ (0),
succ (succ (0)), succ (succ (succ (0))), etc. rather than 1, 2, 3,
etc. If you are using number notations, CAESAR.ADT will complain
about "variable or constant operation 1 was not declared".
To address the problem, we provide a richer library named NATURAL.lib
(located in $CADP/lib/NATURAL.lib), which defines constants notations
from 0 to 9.
You can declare additional numbers as follows:
If you have larger numbers (or even floating-point numbers), you may
implement them externally (i.e., directly in C).
See $CADP/demos/demo_19/cell for such an example with real numbers.
[Thu Nov 28 10:31:25 MET 2002]
By default, Caesar.adt implements natural numbers on a single byte in order to reduce memory costs for model-checking. In fact, natural numbers range from 0 to 254 (as 255 poses an overflow problem with the iterator).
If you need larger numbers, you can use the prodefined library X_NATURAL in which the NATURAL sort are implemented externally in C, as an unsigned int (32 bits). To do so, your ".lotos" file should include
instead of
You should also create in your current directory a
".t" file containing the following lines
and a ".f" file containing
(this ".f" file is meant to store the definitions of external functions, but is almost empty as these functions are already included in the ".t" file). The files themselves are in
$CADP/lib/X_NATURAL.lib
and
$CADP/incl/X_NATURAL.h
Of course, you can define your own natural number types (e.g., 16-bit numbers).
[Thu Nov 28 13:40:15 MET 2002]
You have implemented some functions as "external" (or you forgot to give equations for some functions, in which case CAESAR.ADT assumes that they are external), but you did not provide the corresponding ".f" file containing the implementation of these functions in C.
[Tue Sep 2 09:46:45 MEST 2003]
Yes. If your LOTOS specification is named foo.lotos, you can write code
for external types in foo.t, and external functions in foo.f.
Your files foo.t and foo.f must be in the same directory as
foo.lotos when you call the caesar.adt compiler.
You can have a look at the library examples and follow their models.
For each type FOO, the source code is in $CADP/lib/X_FOO.lib
and the corresponding C implementation in $CADP/incl/X_FOO.h
You should edit the ".h" file and look at the comments before the
"#include" directive (if any). There is a list of all things that need
to be defined in the ".t" and ".f" files.
[Tue Sep 2 09:46:45 MEST 2003]
With the LOTOS-like algebraic semantics, you would have to write n*n equations
for an enumerated type that has n values.
CAESAR.ADT uses priorities between equations, so that you have only to write
2 equations:
The equations for 'ne' would be:
[Tue Sep 2 09:46:45 MEST 2003]
Yes. Use the X_NATURAL library instead of NATURAL. X stands for eXternal.
You can have a look at the following files:
[Tue Sep 2 09:46:45 MEST 2003]
At the beginning of your .t file (if you write one), you have to write:
The values of CAESAR_ADT_EXPERT_T and CAESAR_ADT_EXPERT_F should be the
version number of the CAESAR.ADT compiler you are using.
They will allow to keep compability with future versions of the compiler.
[Tue Sep 2 09:46:45 MEST 2003]
Strictly speaking, you can't.
LOTOS was designed by to be 100%-pure abtract data type.
CAESAR.ADT is a bit more flexible and allows to handle external types and
functions defined in C. Therefore you can handle C strings in your
Lotos program by giving them operation names.
For example:
[Wed Sep 3 08:34:03 MEST 2003]
You can use the #include preprocessor directives in your .t and .f files.
See demo_16 for an example.
[Wed Sep 3 08:34:03 MEST 2003]
See the demo_19 (in $CADP/demos/demo_19) to see how this can be done.
[Wed Sep 3 08:34:03 MEST 2003]
Yes you can, but only some of them.
The external types you define in the .t file can use all the simple types that are
generated by caesar.adt: integer types and enumerated types only.
You can also use the types of the X_*.lib libraries. Do not forget to
include the corresponding X_*.h file at the beginning of your .t.
However, more complex types cannot be used in your external types.
[Wed Sep 3 08:34:03 MEST 2003]
You can use the "-debug" and "-trace" options.
You can have a look at the caesar.adt man page for more details.
[Mon Nov 8 10:06:38 MET 2004]
If you get a message that looks like this:
[Fri Mar 14 15:21:14 MET 1997]
Click on a ".lotos", ".aut", ".bcg" or ".exp" file, then select
`Evaluate mu-calculus formulas' then select "Evaluate mu-calculus
formulas" and then choose a file containing the formula to evaluate
(this file should have .mcl extension and its icon in EUCALYPTUS is
a big 'mu').
[Fri Mar 14 15:21:14 MET 1997]
This is a known bug of Version Z. The problem comes from evaluator,
who asks a question to the user interactively ("Do you want a
diagnostic?"). As Eucalyptus is not designed for accepting answers
on the standard input, every thing is blocked. The solution is to run
evaluator from the command line in a shell window.
[Tue Sep 23 16:11:55 MEST 2003]
On Evaluator's man page (type "man evaluator") there are examples
of formulas expressing different classes of interesting properties
(safety, liveness, fairness). Other formulas can be found in several
CADP demos (see demos 01, 02, 15, 20, 21, 22). Files with the .mcl
extension contain mu-calculus formulas.
[Tue Sep 23 16:14:40 MEST 2003]
The notion of alternation depth has been first introduced by
Emerson and Lei (see E. A. Emerson and C-L. Lei, Efficient Model
Checking in Fragments of the Propositional Mu-Calculus,
Proceedings of the 1st LICS, 1986, p. 267-278) as a measure of
the degree of mutual recursion between the minimal and maximal
fixed points contained in a mu-calculus formula.
For example, the formula mu X . nu Y . f (X, Y) has alternation
depth two, because the minimal fixed point variable X and the
maximal fixed point variable Y are mutually recursive.
Mu-calculus formulas can be grouped into different classes
according to their alternation depth. The simplest such class
(called alternation-free mu-calculus) is obtained for alternation
depth one, which means that no recursion between minimal and
maximal fixed points is allowed.
Alternation-free mu-calculus is sufficiently powerful to express
safety, liveness, and certain fairness properties, and also
benefits from efficient model-checking algorithms (linear in the
size of the formula and of the Labelled transition System).
For more details on the alternation-free mu-calculus, see
H. R. Andersen, Model checking and boolean graphs, Theoretical
Computer Science 126 (1994), p. 3-30.
The syntax of ".mcl" files given in the EVALUATOR manual page
(see "man evaluator") only accepts alternation free formulas.
[Thu Sep 25 10:08:05 MEST 2003]
1. While it may seem that properties are more easily written in XTL
(since they can be "programmed" in a functional style), the contrary
holds for complex temporal properties containing regular expressions
on action sequences. For instance, it is difficult to specifiy in XTL
that a sequence contains a "SEND" followed after several "ERROR"
eventually by a "RECV", all this interlaced by sequences of internal
"tau" actions. In EVALUATOR, it is sufficient to put the correspond
regular expression inside a single modal operator "< >":
Furthermore, it is possible to use libraries and macros to facilitate
the expression of properties (see also the CADP demos containing
".mcl" files).
2. EVALUATOR can generate automatically diagnostics (i.e., subgraphs
of the LTS in ".bcg" format) explaining the truth-value of a formula
(according to the truth-value, a diagnostic has to be interpreted as
an example or counter-example). While it is certainly possible to
program diagnostics in XTL, it is both complicated and leads to
inefficient results (it amounts to program graph traversal in a
functional style).
3. In contrary to XTL, EVALUATOR operates "on-the-fly", and can thus
handle larger LTS.
4. EVALUATOR stops as soons as the truth-value of the property has
been decided, whereas XTL performs a global evaluation, i.e., the
property is evaluated for all states. Thus EVALUATOR is much more
efficient on already constructed LTS (in ".bcg" format).
To sum up, the initial effort necessary to learn the operators of
EVALUATOR (see the man page and the paper
$CADP/doc/Mateescu-Sighireanu-00.ps) will be rewarded by the richer
possibilities offered by EVALUATOR. Furthermore, experience shows
that usually only a small number of operators is necessary
(essentially the modalities "< >" and "[ ]" as well as the regular
operators ".", "|" and "*").
Also, the use of macro-libraries is strongly recommended (see the
demos of CADP containing ".mcl" files).
[Thu Sep 25 10:03:52 MEST 2003]
EVALUATOR handles transition labels as character strings. While this
does not allow to handle data as in XTL, use of regular expressions
enables precise predicates on labels. For instance, the predicate
"SEND.*![0-9].*" represents all labels with a gate "SEND" and an offer
"!0" or "!1" or ... "!9" anywhere in the list of offers.
There is a chapter by Bradfield and Stirling called "Modal Logics and
Mu-Calculi: An Introduction" in the Handbook of Process Algebra (eds.
Bergstra, Ponse and Smolka, Elsevier, 2001).
There is also an article by Ingolfsdottir and Steffen on "Characteristic
Formulae for Processes with Divergence", in Information and Computation,
volume 110 number 1, 1994.
Since LNT has as underlying models Labelled Transition Systems (LTSs),
which are action-based models, it is more appropriate to express
the properties using an action-based temporal logic, such as Action-based CTL
(ACTL) or the modal mu-calculus rather than a state-based one such as CTL.
This is because in the LTSs generated from LNT specifications there is no
information in the states (according to the process algebraic semantics)
but all useful information is present on transition labels.
The 1990 paper "Action versus State Based Logics for Transition Systems"
by De Nicola and Vaandrager (LNCS, volume 469, pub. Spriner Verlag),
gives the definition of ACTL and its relationship with CTL.
Regarding ACTL and action-based logics, you can find some pointers
in the $CADP/doc/Mateescu-Sighireanu-00.ps paper, and also in the
$CADP/src/xtl/actl* files).
For information about the property pattern mappings (proposed by Matt
Dwyer and al.) expressed using ACTL, see
this page.
Yes, you should use parentheses around every occurrence of a macro
parameter in the macro's body, because this avoids subtle errors caused
by the parsing of actual macro arguments according to the precedence
of operators in expressions. For example, an unclean macro definition
like
For example, it is easy to formulate "no starvation" for a process, but
formulating the property for a number of these processes in the system
is a different issue.
A possible approach could be to hide all the actions except those of
interest and to check the property on the abstracted graph. This can
be done directly on a BCG graph using the BCG_LABELS tool, or by means
of an SVL script. The abstracted graph can be minimized using BCG_MIN.
It may be the case that the minimized graph is so simple that it can
be verified visually using BCG_EDIT.
The diagnostic obtained after evaluating an MCL formula on an LTS
illustrates the truth value of the property on the LTS. The diagnostic
produced by EVALUATOR is included in the LTS modulo the preorder of
strong bisimulation. When the MCL formula is valid on the LTS and it
expresses an invariant (i.e., a formula that must be true on all states
of the LTS), the diagnostic may be larger than the LTS if the evaluation
of the formula requires an unfolding of the LTS.
Consider for example the LTS < { 0 }, { A }, { 0--A-->0 }, 0 >, which
consists of a single A-loop. The MCL formula < A { 5 } > true, which
states the existence of a A-sequence of length 5 in the LTS, evaluates
to true and its diagnostic is the A-sequence
0--A-->0--A-->0--A-->0--A-->0--A-->0, which is quantitatively larger
than the LTS but still included in the LTS modulo the preorder of
strong bisimulation.
No. If you want to say that from the current state there is no outgoing
transition satisfying an action formula 'A', you must use the following
modality:
The definition of the ACTL operators is in $CADP/src/xtl/actl.mcl.
To use them in a file prop.mcl, the module actl.mcl must first be included,
then the formula is written. For example, for the CADP demo on the alternating
bit protocol (demo_01), you can write an ACTL property as follows:
You can find details of the definition and use of macros in the
EVALUATOR manual page (see EVALUATOR 3 man page or type "man evaluator3").
This property is:
The property can also be expressed as
As a general rule, when checking safety properties, which intuitively
express that "something bad never happens", or that "some bad execution
sequence must be absent", you first try to characterize the bad sequences
as a regular language R, and then just use the modality "[ R ] false"
to express that these sequences are absent (most of the safety properties
of $CADP/src/xtl/mcl_pattern.mcl are of this form).
You can find such identities in the manual page of the tool (type
"man evaluator" or take a look in $CADP/man) and in the paper
https://cadp.inria.fr/publications/Mateescu-Sighireanu-00.html
The evaluator.bcg contains a diagnostic of the formula (i.e., a
subgraph of the LTS that illustrates the truth value of the formula
on the LTS). In the case of safety formulas [ R ] false which are true,
the result is a large part of the LTS (the part that the tool had to
explore in order to verify the formula). For safety properties [ R ] false
which are false, the diagnostic is usually much smaller (a sequence that
violates the formula, i.e., that matches R). This is documented in the
EVALUATOR manual page (see EVALUATOR man page or type "man evaluator").
I want to specify the property that the system will never reach a state
where action 'bad' is enabled, while both of actions 'good1' and 'good2'
are enabled.
That means it is right if both of 'good1' and 'good2' are enabled but
'bad' is disabled, and it is also right if 'bad' is enabled but not BOTH
'good1' and 'good2' are enabled at the same state.
I want to check the following
(state)-good1, good2, bad->
is not a part of the LTS.
The property you want to express could be written as follows:
EVALUATOR can provide diagnostics (subgraphs of the LTS being verified)
for a formula. If the formula is true, the tool provides a positive
diagnostic (example), while if the formula is false, the tool provides
a negative diagnostic (counterexample). If you are using EVALUATOR
through the EUCALYPTUS graphical user interface, the option
"Generation of Diagnostic Files" is selected by default and the default
name of the diagnostic file is "evaluator.bcg". Therefore you will
automatically obtain a diagnostic in this file when you evaluate a
formula. The diagnostic can be viewed as any normal BCG file, using the
options on the "Visualize" menu.
You can set the $CADP_TIME environment variable, which was introduced
in April 2008 (see entry #1276 in the $CADP/HISTORY file for details).
This will provide timing information on the executions of EVALUATOR (and,
more generally, of OPEN/CAESAR application programs used).
Yes. In MCL, you can specify the following formula:
Yes. For example, it is possible to write formulas like:
EVALUATOR accepts a subset of the standard UNIX regular expressions.
These are detailed in a special CADP regexp manpage:
$CADP/man/*/regexp, as indicated in the evaluator man page.
Detailed question: Using Evaluator 3, How can I verify a formula such as
the following:
Response: Instead of verifying the whole formula at once, which is likely
to exhaust the memory, we recommend that you split it in seperate files,
one for each conjunct, and verify each conjunct separately.
Concerning LTL, the encapsulation is indirect: with MCL one can now code
Buchi automates (with labelled transitions), which serve as an
intermediate language for model checking LTL formulas.
These Buchi automates are coded in MCL with the infinite iteration
operator, "< ... > @", which is then compiled into disjunctive BESs with
tagged variables (in a manner similar to tagged states in Buchi
automates).
These BESs, which are of a size proportional to the product of the
initial "< ... > @" formula and the LTS (i.e., |< ... > @|*(|S|+|T|)),
where |< ... > @| is the number of operators in the formula, can be
resolved in linear time with the BES resolution algorithm that was
proposed in $CADP/doc/Mateescu-Thivolle-08.* (FM'2008). Here, "linear"
is w.r.t. the size of the BES mentioned above.
Note, this is not to say that MCL and EVALUATOR 4.0 provide a model
checking procedure of linear complexity for LTLs, because the translation
of LTLs to Buchi automates has exponential complexity in the worst case.
In other words, the MCL "< ... > @" formulas resulting from the
translation of LTL formulas can have a size that is exponential compared
with that of the LTL formulas.
This manner of verifying properties that are linear in nature with MCL is
close to the first version of SPIN, which enables LTL formulas to be
expressed directly as Buchi automates (the "never claims" of Holzmann).
Currently, MCL and EVALUATOR 4.0 can serve as a verification engine for
LTL provided that there is a translation of the LTL formulas into Buchi
automates (e.g. with the LTL2Buchi translator) followed by conversion of
these automates into MCL formulas of the form "< ... > @".
This is normal as there is a conflict between A and B. Use the -conflict
option, or write
Please refer to the updated exhibitor manpage
[Fri Nov 7 15:07:04 MET 1997]
This problem occurs when your disk is full ! Check it out, and make
some room.
[Fri Nov 7 15:10:52 MET 1997]
See question A.4.2 (Verification).
If you are looking for an action called "ERROR !12", you must create
a .seq file containing the line:
or
It is best to do this type of search on-the-fly using lotos.open
[Mon Nov 8 10:06:38 MET 2004]
OCIS has some internal features, such as time handling
and MSC drawing that are not yet available to CADP users, since the
other tools of CADP do not give access to these features. The pictures
on the web site have been used on our internal prototypes, which we do not
distribute yet since they are not yet stable enough.
[Mon May 15 11:02:09 MEST 2006]
CADP offers three simulators allowing step-by-step execution:
OCIS, XSIMULATOR, and SIMULATOR.
OCIS (Open/Caesar Interactive Simulator) is a more recent
tool that supersedes XSIMULATOR. To launch OCIS from EUCALYPTUS,
you should select "Advanced Simulation" from the "Execute..." menus.
The XSIMULATOR tool is reaching the end of its software life; it has
several limitations that are impossible to overcome without a total
rewrite; this was exactly the inital purpose of OCIS. OCIS has also
many advanced features that are missing from XSIMULATOR.
The SIMULATOR command has the same functionnalities as XSIMULATOR,
but with command-line options. The same behaviour can be obtained
by invoking OCIS with the (undocumented) "-tty" option.
[Mon May 15 11:47:19 MEST 2006]
Internally, OCIS can display timing information (ie. information about
delays). At present, there is no tool exploiting this possibility by
passing timing information to OCIS. But this might change in the future.
[Mon May 15 11:47:51 MEST 2006]
When using OCIS on a LOTOS program (or an ".exp" specification)
containing several concurrent processes, one only gets one process
(named "Task 0") in the MSC view of the OCIS simulation window,
although there should be more than one. One cannot obtain the MSC
(message sequence charts) pictures shown on the
OCIS manual page
In fact, OCIS is indeed designed to support MSC views with more than one
process. However, this feature relies on the OPEN/CAESAR V2 API
(Application Programming Interface). So far, the existing
OPEN/CAESAR-compliant compilers (e.g., Caesar and Exp.Open) only implement
the Open/Caesar V1 interface, in which there is only one process (i.e., all
parallel processes are merged into a single, sequential automaton, which
corresponds to the classical view of a Labelled Transition System).
Since, at present, no compiler provides OCIS with information related to
multiple tasks, OCIS assumes that there is only a single task.
In the future however, we expect to implement OPEN/CAESAR V2.
There are two possible cases:
1) The sequence is explicit and is stored in a BCG (.bcg) file. To
display the sequence, click "Load scenario" in the OCIS interface.
2) The sequence is implicit in the form of a "pattern" in SEQUENCE
format (.seq) for EXHIBITOR or a temporal logic formula in the MCL
langauge (.mcl) for EVALUATOR. This is is typically the case when
searching for sequences of the form a.tau*.a.tau*.c. In this case, you
must find the corresponding explicit sequence in the LTS using EXHIBITOR
or EVALUATOR with
the -diag option. The resulting explicit sequence can then be displayed
as in case 1).
Use the "Save scenario" button to save the sequence in a BCG file.
Then you can use BCG_EDIT to make any changes you wish to the file and
to print it. See the bcg_edit man page
for details.
All the OPEN/CAESAR tools (exhibitor, terminator, xsimulator, etc.)
work on-the-fly: they do not require that the whole LTS is generated.
If you type:
you will be able to simulate your program without generating the whole
LTS. Same thing for exhibitor, etc.
Of course, you can also apply the OPEN/CAESAR tools to completely
generated graphs (using bcg_open) but this is not mandatory.
[Wed Sep 24 10:38:48 MEST 2003]
The interface descriptions are part of CADP and can be found in
various places, e.g., "$CADP/doc/*/Garavel-92-a.html" or
"$CADP/man/*/caesar_*".
The interfaces are in "$CADP/incl/caesar_*".
Examples of Open/Caesar tools (several in source code form) are given
in "$CADP/src/open_caesar/*".
So far, we have not decided to publish the Open/Caesar APIs on the
Internet. However, registered CADP users have full access to these APIs
after installation. The files are in directory $CADP/man. There are
subdirectories for NROFF, PostScript and HTML formats. The contents of
these directories are the same (as the PostScript and HTML is produced
automatically).
You can simply type "man caesar_hide_1" or "man caesar_rename_1" or find
the HTML files in $CADP/man/html/.
The full book of Open/Caesar APIs is in $CADP/doc/Garavel-92.ps
In terms of languages, the semantic is the following:
(B1 -|| B2) has for result the automaton B1 from which have been
eliminated the following:
The explanation extends to the case of a semi-composition operator
(B1 -|L| B2) involving a synchronisation list L. See the
projector man page
for details.
[Mon Nov 8 10:06:38 MET 2004]
Reductor uses a simple algorithm: from a given state, it first explores
the tau component (all states reachable by following tau transitions)
then fires all non-tau transitions from these states. The source code
of Reductor is given in $CADP/src/open_caesar.
There was a paper on tau*.a bisimulation by Fernandez and Mounier in 1990.
There is a related paper by Bouajjani et al. in 1992 on safety equivalence.
We also have published a paper at CAV 03 on
computing tau-confluence on the fly.
Use the REDUCTOR tool with the -trace and -total options. See the
reductor man page
for information about the tool and its options.
Yes. You can use the REDUCTOR tool with the -taustar option to minimize
the LTS modulo tau.* equivalence. See the
reductor man page for information about the tool and its options.
[Mon Apr 21 13:52:32 MET DST 1997]
Check your LD_LIBRARY_PATH.
You should have /usr/openwin/lib libraries before the X11 libraries
For instance, if you have
LD_LIBRARY_PATH = /usr/X11/lib:/usr/openwin/lib
permuting both of them is likely to solve the problem
[Mon Apr 21 13:52:32 MET DST 1997]
We have used fonts the most widespread fonts on X11 window systems.
The 75dpi and 100dpi fonts are generally found on all machines. Maybe
your X Terminal hasn't been configured properly, and some of the
standard fonts have been left out.
If you can't configure your X terminal, so it can display 75dpi fonts,
then, your may alter the source of xsimulator, especially the file:
$CADP/src/xsimulator/xsimulator.tcl at the line 39:
In this line, replace -*-times-bold-r-normal--24-*-*-*-*-*-*-* by a font
that your terminal can display (use the xfontsel command to find out
what your terminal can display).
[Mon Apr 21 13:52:32 MET DST 1997]
This problem has been solved in version 97a. If you still experience
problems with Xsimulator, you could use simulator instead, which is an
ASCII version of Xsimulator. Type:
[Wed Jun 18 17:26:32 MET DST 1997]
I have a xsimulator program generated from a LOTOS program.
I want to execute it on another machine, i.e. to send it to somebody
else, so that they can use the simulation. Can I execute the generated
xsimulator program on his machine?
You can, provided that the other machine is the same type (i.e.
architecture and operating system) than the machine on which xsimulator
was produced.
If the other machine has CADP installed, there is no problem, be sure
that the $CADP environment variable is correct.
If the other machine does not have CADP installed on it, you have to
copy xsimulator and some other files from the CADP release in order
to make xsimulator work. By executing the following commands, you
can create a directory containing a minimal subset of CADP necessary
to execute xsimulator:
The Xsim directory now contains all that xsimulator needs. You can now
copy this directory on a remote machine, where CADP is not installed.
To execute xsimulator, you must set the global environment variable,
CADP to the location of the Xsim directory.
if you are using csh, or
if you are using sh.
[Mon Dec 19 19:09:24 MET 2005]
Yes! you can generate a .aut file with CAESAR, then reduce it with
BCG_MIN, and then explore it using BCG_OPEN and OCIS, or draw it
using BCG_DRAW.
This is achieved really easily through EUCALYPTUS. Just click on the
reduced file and select Execute / Standard simulation
[Mon May 15 10:36:03 MEST 2006]
There is no version of XSIMULATOR for Windows, i.e., there are no such
files in CADP named
This is due to the fact that XSIMULATOR (and its companion tool
DUPLEX) use a Unix-specific mechanism ("fork()") for process creation,
which is absent from Windows. On Windows, you should use OCIS instead
of XSIMULATOR.
[Mon May 15 10:46:07 MEST 2006]
This problem occurs when a state has so many outgoing transitions
that the pipe buffer used for interprocess communication between
XSIMULATOR and DUPLEX becomes full. Unfortunately, it seems that this
problem will be solved easily, because the limitations come from
the operating system itself (size of the buffers). In such case,
you should use OCIS instead of XSIMULATOR.
[Wed Oct 20 16:58 MET 1999 - Mon Aug 21 18:13 MET 2000]
For monitors with a limited number of colors, it might be that
the colors of XSIMULATOR are unreadable (for instance, the
background is light grey and the font is displayed in white on top
of that, or the background is white and the text is displayed in
light yellow). Thus, the display text is not distinguishable from the
background.
You have two options. (1) You can switch to OCIS instead of XSIMULATOR,
which does not exhibit this problem. (2) If you want to stay with
XSIMULATOR, you could try to patch the TCL/TK files of XSIMULATOR
to force different colors. Look for the files:
and try to replace non-primitive colors (such as Thistle1, VioletRed1,
SlateBlue1, VioletRed1) with more primitive ones such as (blue, red,
yellow, green, white, and black).
[Mon Apr 21 13:52:32 MET DST 1997]
No. This is a known feature of partial verification (and particularly of
Holzmann's supertrace algorithm). There may exist deadlocks that
TERMINATOR can't detect. For an exhaustive deadlock detection, you
should use "aldebaran -dead" or use EXHIBITOR with the sequence
<any>* <deadlock>
The automaton below represents a set of execution traces and can be
used as a "stress test" for TGV because of its high complexity.
Yes, this can be done using an SVL script. Before invoking TGV, a
message can be displayed using standard functions of the UNIX shell,
which can be freely used in SVL scripts by preceding them by the '%'
character.
Yes ! It's called Eucalyptus an is invoked by typing xeuca .
First of all 2 european/canadian projects from 1994 to 1996. For
more information visit the WWW page:
EUCALYPTUS 2.* has two main changes, compared to versions 0.* and 1.*:
it is written in TCL/TK instead of XTPANEL, so the interface is much
better and faster; it will be integrated in CADP so you no longer need
to install two packages (CADP and EUCALYPTUS).
Consequently, EUCALYPTUS 1.2 (which is the most latest XTPANEL-based
version) will no longer evolve in the future.
Yes ! http://vasy.inria.fr/eucalyptus.html
[Tue Apr 22 10:57:03 MET DST 1997]
This happens when "/usr/openwin/lib" is not in your LD_LIBRARY_PATH, as
explained in the INSTALLATION directives. This error is detected by the
"tst" routine:
[Tue Apr 22 10:57:03 MET DST 1997]
The early versions 0.* and 1.* of EUCALYPTUS were preliminary drafts of
the GUI.
The current versions 2.1 (shipped within CADP version Z), 2.2 (Shipped
within CADP version 97a) of EUCALYPTUS are much better.
It has been entirely rewritten in Tcl/Tk.
So forget about EUCALYPTUS 1.* and upgrade to EUCALYPTUS 2.* which is
really better. It is used here everyday with satisfaction.
This error message indicates that Eucalyptus is unable to read these BCG
files. This is probably because they were generated by a version of the
mCRL tools that was compiled and linked against an old version of CADP.
The solution is to entirely recompile the mCRL2 tools, being sure
that variable $CADP points to the directory where the latest CADP tools
have been installed. Then regenerate the BCG files.
The fundamental question is whether to use bisimulation checking or model
checking. This is subject to vast debate.
The verification of ACTL (Action-based CTL) formulas has a linear time
complexity O (n.f) w.r.t. the number of states n and the formula size f.
The computation of bisimulation is a little bit more costly, with a
complexity O (n log n). These theoretical worst-case bounds become more
uncertain for on-the-fly verification.
In addition, a single verification by bisimulation checking may replace
the verification of several temporal logic formulas. See, for instance,
the article "$CADP/doc/*/Garavel-Mounier-96.html" for excellent examples
of bisimulation checking.
Finally, the debate does not concern only ALDEBARAN and XTL. Indeed, CADP
contains other verification tools: ALDEBARAN, BCG_MIN, and BISIMULATOR
for bisimulation checking; XTL, EVALUATOR 3.x and EVALUATOR 4.0 for model
checking.
You may find a list of Case-Studies on the WWW page:
Yes, CADP has been used in many case studies and projects. See the CADP web site and notably the Case
Studies page for an up-to-date list.
See the WWW page
Yes, registered users are individually informed on the availability of
new versions of CADP. The traffic on this mailing list is moderate (3 or
4 messages per year) which is intentional, as this mailing list is not
a newsgroup but just a means of keeping users informed. If you are on
this mailing list, then you probably received a message in december 1996
on the availability of version Z. To be added to this list, just send an
E-mail to [email protected].
[Fri Jun 6 16:14:14 MET DST 1997]
All registered users are automatically added to the mailing-list.
This list is used to announce new releases.
1. XESAR was a verification toolbox developed in the 80s for a dialect
of ESTELLE named ESTELLE/R. This toolbox contained a module for
evaluating temporal logic formulas on a labelled transition system.
This evaluation module, extended with diagnosis capabilities, is called
CLEOPATRE.
Unfortunately, the XESAR/CLEOPATRE tools are no longer distributed with
CADP because they are not maintained and because of a lack of
documentation and a lack of portability (a PASCAL compiler is necessary)
Also, due to a lab split, some people who developed XESAR are no longer
in our lab, so we can't distribute this software ourselves.
You might obtain a copy of XESAR/CLEOPATRE by sending a request to
[email protected]. He might send to you some (free of charge)
license agreement. In any case, there will be very little documentation
and no support at all.
2. In place of XESAR/CLEOPATRE, we suggest that you use the EVALUATOR
tool that is already in the official CADP Distribution. EVALUATOR is a
powerful on-the-fly model-checker for branching-time mu-calculus.
It is implemented on top of the OPEN/CAESAR interface.
There is a manual page for EVALUATOR (type "man evaluator"), and you can
also have the look at the corresponding demos.
3. Finally, we are currently developing another model checker, named
XTL, compatible with LOTOS, not yet integrated in the toolset.
[Fri Nov 7 14:29:42 MET 1997]
The simplest way is to let CAESAR generate BCG files. The latest
version of CAESAR generates BCG files by default (simply omit
the -aldebaran option). Then you can convert this BCG file to the format
supported by the Concurrency Workbench using the BCG_IO command.
or:
[Thu Nov 6 09:52:14 MET 1997]
You may obtain the Fc2tools directly from the following Web Page:
http://www.inria.fr/meije/verification/downloads.html
[Thu Nov 6 09:52:14 MET 1997]
[Thu Nov 6 09:52:14 MET 1997]
As in the question above, you can do
this operation from EUCALYTPUS or from the command line.
[Thu Nov 6 09:52:14 MET 1997]
As in the question above, you can do
this operation from EUCALYTPUS or from the command line.
[Thu Nov 6 09:52:14 MET 1997]
The Fc2Tools can't process directly .exp files. There exists a tool
in the toolset, called 'exp2fc2', that converts networks of
communicating LTSs expressed in the .exp format to networks of
communicating LTSs expressed in the .fc2 format.
This tool has been integrated into EUCALYPTUS, so that the user may
click on a .exp file and use the Fc2Tools without bothering about file
conversions, the interface does it itself.
A deadlock state has no successors. This can be checked with the bcg_user.h API.
The VLTS (Very Large Transition Systems) benchmark suite is a collection of Labelled Transition Systems obtained from various case studies about the modelling of communication protocols and concurrent systems. Many of these case studies correspond to real life, industrial systems. For more information, see the VLTS Benchmarks resource page at http://cadp.inria.fr/.
A state without successor is not necessarily a problem. This may also correspond to the normal termination of a system. The word "deadlock" evokes a concurrent program, where some synchronization failed; this may indeed indicate a design error.
These are LTSs generated from realistic case-studies, many of which are
industrial systems, or fragment of industrial systems. These LTSs were
selected among a larger set of examples, based on statistical criteria
(increasing sizes, branching factor, etc.). There is no documentation
attached; to the contrary, the labels of certain LTSs corresponding to real
industrial systems have been renamed.
There are a number of CADP tools you could use to analyze DTMCs and CTMCs:
BCG_STEADY for steady state numerical analysis, BCG_TRANSIENT for
transient numerical analysis, DETERMINATOR for on-the-fly model reduction
by removing stochastic nondeterminism, and CUNCTATOR for on-the-fly
steady-state simulation of CTMCs. See the relevant man pages for details.
B.7.4. Learning LOTOS is not as easy as reading a book and doing it... Are there other languages I can use with CADP that are easier to use than LOTOS?
C. Questions regarding CADP tools
C.1. The ALDEBARAN tool
C.1.1. The -path option of ALDEBARAN does not give me the shortest path!
aldebaran -path S FILE.bcg
bcg_info -path S FILE.bcg
C.1.2. How do I get the branching factor of a .bcg file?
bcg_info -branching FILE.bcg
C.1.3. Why does my .aut files contain some actions with quotes and some actions without quotes?
bcg_io $1.bcg $1.aut
on any BCG file.
C.1.4. How to convert a .aut file to another format?
bcg_io $1.bcg $1.aut
C.1.5. "No more memory" error when reducing a state space
C.1.6. Can Aldebaran produce a record of the renaming of states during propjection?
C.1.7. Using branching equivalence, can Aldebaran display information about where two LTSs are not equivalent?
C.1.8. What is the correct syntax for specifying the name of a gate in an AUT (.aut) file?
C.1.9. How can I manipulate a trace produced with the -path option of ALDEBARAN?
aldebaran -path 23 graphe.bcg > result.seq
bcg_io result.seq result.bcg
The resulting trace in BCG format can then be visualized and converted
to PostScript format using BCG_EDIT.
C.2. The BCG_DRAW and BCG_EDIT tools
C.2.1. Why does BCG_DRAW produce double-tipped arrows when drawing a BCG file?
C.2.2. Can BCG_DRAW produce output in xfig format?
C.2.3. What is BCG format?
C.2.4. How can I know the names of the BCG variables representing the variables of a LOTOS program?
C.2.5. Can I use a normal editor to edit a BCG file?
C.3. The BCG_GRAPH tool
C.4. The BCG_INFO tool
C.4.1. Is there a way to know the size of a bcg graph without calling ALDEBARAN?
bcg_info FILE.bcg
C.5. The BCG_IO tool
des (0, 6, 7)
(0, F, 6)
(4, E, 5)
(0, C, 3)
(1, B, 2)
(3, D, 4)
(0, A, 1)
bcg_edge: previous state are not increasing in BCG_WRITE_EDGE
C.6. The BCG_LABELS tool
C.6.1. How can I rename or hide transition labels in a BCG file?
bcg_labels -hide -partial foo.hid locker1.bcg locker2.bcg
where foo.hid is
hide
"pid(1)"
"pid(2)"
will hide all labels containing the substrings "pid(1)" or "pid(2)"
in locker1.bcg. The result is stored in locker2.bcg
bcg_labels -rename foo.ren locker.bcg
where foo.ren is
rename
"return({pid(\[0-9]*\)),tag},ok,pid(\([0-9]\)*))" -> "return \1 \2"
".*" -> "others"
will rename
"return({pid(1),tag},ok,pid(0))" into "return 1 0",
"return({pid(2),tag},ok,pid(0))" into "return 2 0",
"return({pid(3),tag},ok,pid(0))" into "return 3 0",
etc.
and everything else into "others".
"locker2.bcg" = partial hide "pid(1)", "pid(2)" in "locker1.bcg" ;
The second example above can be rewritten in SVL as follows:
"locker.bcg" =
total rename
"return({pid(\[0-9]*\)),tag},ok,pid(\([0-9]\)*))" -> "return \1 \2",
".*" -> "others"
in "locker.bcg" ;
C.7. The BCG_MERGE tool
C.8. The BCG_MIN tool
C.8.1. How can I minimize a .aut file using BCG_MIN?
bcg_io FILE.aut FILE.bcg
bcg_min -strong FILE.bcg
or
bcg_min -branching FILE.bcg
If you absolutely want oservational equivalence, instead of branching
equivalence, the first thing to do is a pre-minimisation using the
branching equivalence (using "bcg_min -branching"). Then run:
aldebaran -bmin FILE.bcg
C.8.2. What is the largest graph minimized by BCG_MIN?
C.8.3. Stochastic branching reduction of two strongly equivalent graphs yields graphs of different sizes!
bcg_min -branching -rate ...
may produce BCG graphs of different sizes, i.e., with different numbers
of states and/or transitions.
bcg_open input.bcg generator output.bcg
This produces a BCG graph named output.bcg, which is equal to
input.bcg deprived from its unreachable states.
C.8.4. A hidden transition between non observationally equivalent states disappears after observational minimization!
des (0, 5, 3)
(0, i, 1)
(0, i, 2)
(0, B, 2)
(1, i, 2)
(1, A, 2)
Steps (1) and (2) leave the graph unchanged (i.e., each state is the
only member of its own equivalence class) but step (3) eliminates
the tau-transition (0, i, 2), which is redundant due to the existence
of the sequence (0, i, 1) followed by (1, i, 2).
des (0, 4, 3)
(0, i, 1)
(0, B, 2)
(1, i, 2)
(1, A, 2)
Note that this graph has no tau-transition from (the equivalence class
of) state 0 to (the equivalence class of) state 2, although the
original graph has a tau-transition from state 0 to state 2.
C.9. The BCG_OPEN tool
bcg_open cons23NoWA.bcg evaluator -verbose -bfs -diag evaluator.bcg r1new.mcl
bcg_open: using ``/cadp/bin.win32/evaluator.a''
bcg_open: running ``evaluator -verbose -bfs -diag evaluator.bcg r1new2.mcl''
for
``./cons23NoWA.bcg''
-- evaluator 3.6 -- R. Mateescu and M. Sighireanu (INRIA Rhone-Alpes) --
evaluator: preprocessing of ``r1new2''
evaluator: syntax analysis of ``r1new2.xm''
evaluator: semantic analysis of ``r1new2.xm''
evaluator: - type binding
evaluator: - data variable binding
evaluator: - propositional variable binding
evaluator: - function binding
evaluator: - type checking
evaluator: - consistency checking
evaluator: conversion to PNF of ``r1new2.xm''
evaluator: simplification of ``r1new2.xm''
evaluator: translation to PDLR of ``r1new2.xm''
evaluator: translation to HMLR of ``r1new2.xm''
evaluator: optimisation of ``r1new2.xm''
evaluator: writing blk dump of ``r1new2.xm''
evaluator: resolution of ``r1new2''
evaluator: diagnostic of ``r1new2''
bcg_version: unknown version number 0.0 in bcg_compute_version
C.10. The BCG_READ and BCG_WRITE APIs
LDFLAGS = "-L${BCG:-$CADP}/bin.`$CADP/com/arch` -lBCG_IO -lBCG -lm";
C.10.2. Where can I find documentation on the definition of the BCG format?
C.10.3. Is there a way to write comments in a BCG file?
C.11. The BCG_STEADY and BCG_TRANSIENT tools
C.12. The BISIMULATOR tool
C.13. The CAESAR tool
C.13.1. Why does CAESAR give me the following message?
caesar: - simulator compilation
"SPEC.c", line 26625: CAESAR_ undefined
"SPEC.c", line 26625: syntax error
#167 error in file ``.h'' during simulation:
simulator program is rejected by the C compiler
quit
*** Error code 1
make: Fatal error: Command failed for target `SPEC.aut'
C.13.2. Why does CAESAR stop during the "generation" phase?
C.13.3. How can I accelerate the graph generation?
C.13.4. How can I produce the minimal graph?
C.13.5. Error Message: "ld: fatal: file /tmp/caesar_6888.x: cannot msync file; errno=12"?
ld: fatal: file /tmp/caesar_6888.x: cannot msync file; errno=12
#122 error in file ``.h'' during type survey:
survey program is rejected by the C compiler
quit
*** Error code 1
make: Fatal error: Command failed for target ..
C.13.6. How can I find out the number of states generated while CAESAR is running?
bcg_info FILE.bcg
C.13.7. Error Message: "theoretical limitation during restriction: process recursion through some forbidden operator"
process P [G] : noexit :=
G ? ... ; ...
|||
i; P [G]
endproc
P [G] ||| P [G] ||| ... ||| P [G]
i; P [G] ||| i; P [G] ||| ... ||| i; P [G]
C.13.8. Is it possible to mix recursion and parallel composition?
specification ManagementSystem[l,f,t,c,d,s,sop]:noexit
behaviour
ManagementApplications[l,f,t,c,d,s,sop]
|[l,f,t,c,d,s,sop]|
MangementPlatform[l,f,t,c,d,s,sop]
where
process ManagementApplications[l,f,t,c,d,s,sop]:noexit:=
(* is infinite, with several parallel applications
for performance, log, security ... *)
endproc
process MangementPlatform[l,f,t,c,d,s,sop]:noexit:=
(* has a infinite behaviour too, providing services to
the applications *)
endproc
endspec
process ManagementSystem[l,f,t,c,d,s,sop]:noexit :=
( ... )
|[l,f,t,c,d,s,sop]|
( ... ManagementSystem[l,f,t,c,d,s,sop] ... )
endproc
C.13.9. Error Message: "root process having value parameters"
C.13.10. What is the maximum size of LOTOS specifications CAESAR can handle?
C.13.11. Where can I find information about the EXEC/CAESAR environment?
C.13.12. What is the mathematical relationship between the number of LOTOS processes (and temporal operators) and the number of states of the associated BCG generated by CAESAR?
C.13.13. Why does CAESAR a segmentation fault during the "simulation" phase?
C.14. The CAESAR.ADT tool
C.14.1. CAESAR.ADT does not find the `indent' command?
C.14.2. Does CAESAR.ADT deal with parameterized types?
C.14.3. Does CAESAR.ADT deal with renamed types?
C.14.4. Where can I find the LOTOS standard library (containing predefined types such as booleans, bits, integers, etc)?
C.14.5. Error Message: "Theoretical limitation: domain of an infinite (or complex) sort cannot be enumerated"?
process FEEDER [G] : noexit
G !NIL;
FEEDER [G] ;
[]
choice X: NAT []
G !CONS (X, NIL);
FEEDER [G]
[]
choice X,Y: NAT []
G !CONS (Y, CONS (X, NIL));
FEEDER [G]
endproc
#define ITERATOR(X) for (X=element_of_sort; X < limit_itr_of_sort; X=next_element)
Example: File descr.lotos
type Queue is Natural
sorts
Queue (*! enumeratedby Enum_Queue *)
opns
...
endtype
#define CAESAR_ADT_EXPERT_T 4.3
/* This command restricts integers to range 0..4 */
#define INTEGER_LIMIT 5
#undef ADT_ENUM_NAT
#define ADT_ENUM_NAT(CAESAR_ADT_0) \
for ((CAESAR_ADT_0) = 0; (CAESAR_ADT_0) < INTEGER_LIMIT; ++(CAESAR_ADT_0))
/* Number of Queues */
#define LIMIT_ITR_QUEUE INTEGER_LIMIT + INTEGER_LIMIT * INTEGER_LIMIT + 1
/* Array of Queues */
CAESAR_ADT_TYPE_QUEUE ITR_QUEUE[LIMIT_ITR_QUEUE];
/* Here comes the iterator Enum_Queue */
#undef Enum_Queue
#define Enum_Queue(X) \
int CAESAR_I; \
MON_INIT (); /* Construction of the ITR_QUEUE array */ \
for (CAESAR_I = 0;
((CAESAR_I) < LIMIT_ITR_QUEUE) ? ((X) = ITR_QUEUE[CAESAR_I]) : 0;
++(CAESAR_I))
/* loop instruction */
/* Here, we build an array containing all the elements of Queue */
void MON_INIT ()
{
static ONCE = 0;
int I;
if (ONCE == 0) {
ONCE = 1;
{
CAESAR_ADT_NAT VAR_NAT_X;
CAESAR_ADT_NAT VAR_NAT_Y;
/* Queue = NIL */
ITR_QUEUE[I = 0] = Q_EMPTY ();
{
/* Queue = CONS (X , NIL) */
/* The following line is the iterator for the NAT sort */
/* It is thus a loop command */
CAESAR_ADT_ITR_NAT (VAR_NAT_X)
ITR_QUEUE[++I] = Q_CONS (VAR_NAT_X, Q_EMPTY ());
}
{
/* Queue = CONS (Y, CONS (X, NIL)) */
CAESAR_ADT_ITR_NAT (VAR_NAT_X)
{
CAESAR_ADT_ITR_NAT (VAR_NAT_Y)
ITR_QUEUE[++I] = Q_CONS (VAR_NAT_Y,
Q_CONS (VAR_NAT_X, Q_EMPTY ());
}
}
}
}
} /* end of function MON_INIT */
Lotos description:
G ?X:NAT;
driver.c file:
int G (INPUT, NAT, X, EOL)
CAESAR_KERNEL_OFFER INPUT;
char *NAT;
ADT_NAT X
CAESAR_KERNEL_OFFER EOL;
{
assert (INPUT1 == CAESAR_KERNEL_INPUT);
assert (strcmp (NAT, "ADT_NAT") == 0);
fprintf(stdout,"Enter a value for X:");
fscanf(stdin,"%d",&X);
return 1;
}
C.14.6. What is the meaning of the following annotations: "(*! implementedby X comparedby Y enumeratedby Z printedby T *)"?
C.14.7. How can I restrict iteration on integers from 0..255 to 0..n?
#define CAESAR_ADT_EXPERT_T 5.3
/* This file restricts the message numbers to the integer range 1..3 */
#undef ADT_ENUM_NEXT_NAT
#define ADT_ENUM_NEXT_NAT(CAESAR_ADT_0) ((X)++ < 3)
#define CAESAR_ADT_EXPERT_T 4.3
/* This file restricts the message numbers to the integer range 1..3 */
#undef ADT_ENUM_NAT
#define ADT_ENUM_NAT(CAESAR_ADT_0) \
for ((CAESAR_ADT_0) = 1; (CAESAR_ADT_0) <= 3; ++(CAESAR_ADT_0))
C.14.8. Where can I find the concrete C implementation for Y_QUEUE.lib and Y_SET.lib?
C.14.9. How do I use library files that are not in $CADP/lib nor in the current directory?
C.14.10. Are there short-circuit "and" and "or" expressions in LOTOS?
library BOOLEAN
library X_BOOLEAN
#define CAESAR_ADT_EXPERT_T 4.4
#include "X_BOOLEAN.h"
#define CAESAR_ADT_EXPERT_F 4.4
C.14.11. In the generated .h file, why do fatal errors call "kill(getpid(), 15)" rather than "exit(1)"?
C.14.12. How can I use the C code generated for enumerated types in my own C program?
The syntax to use the constructors on your C program is F() (for example
TRUE() or FALSE(), do not forget the parentheses).
C.14.13. In my ``.t'' file, I cannot use the C types generated from my LOTOS code.
You can also use the types of the X_*.lib libraries. Do not forget to
include the corresponding X_*.h file at the beginning of your .t.
C.14.14. The Natural library only contains natural number digits up to 9. Can I go beyond this?
type ExtendedNatural is Natural
opns
10, 11, 20 : -> Nat
eqns
ofsort Nat
10 = Succ (9);
11 = Succ (10);
20 = 10 + 10;
endtype
C.14.15. In LOTOS, can I define natural numbers with more than 256 values?
library X_NATURAL endlib
library NATURAL endlib
#define CAESAR_ADT_EXPERT_T 5.0
#include "X_NATURAL.h"
#define CAESAR_ADT_EXPERT_F 5.0
C.14.16. When I run caesar or lotos.open, it complains that I haven't got a ".f" file
C.14.17. Can I import C types and functions into my LOTOS description?
C.14.18. How can I define the 'eq' operator on enumerated types?
ofsort bool
x eq x = true;
x eq y = false;
x ne y = not (x eq y);
C.14.19. Is it possible to use naturals but to have them implemented using natural C integers?
$CADP/lib/X_NATURAL.lib -- LOTOS definitions
$CADP/incl/X_NATURAL.h -- corresponding C types/functions
$CADP/demos/demo_12 -- example of use
$CADP/demos/demo_16 -- example of use
You will have to include X_NATURAL.h in your .t file.
C.14.20. What do CAESAR_ADT_EXPERT_T and CAESAR_ADT_EXPERT_F mean? Which values should I give them?
#define CAESAR_ADT_EXPERT_T 5.1
and to add a similar line in your .f file, with CAESAR_ADT_EXPERT_F.
C.14.21. How do I use characters and strings in a LOTOS specification?
------------------------------- test.lotos ------------------------------------
specification STRING_EXAMPLE [PRINT] : noexit
library X_BOOLEAN, X_NATURAL, X_CHARACTER, X_STRING endlib
type MY_OWN_STRINGS is STRING
opns HELLO_WORLD (*! implementedby HelloWorld *) : -> STRING
THE_END (*! implementedby TheEnd *) : -> STRING
endtype
behaviour
PRINT !HELLO_WORLD;
PRINT !THE_END;
stop
endspec
------------------------------- test.t ------------------------------------
#define CAESAR_ADT_EXPERT_T 4.6
#include "X_BOOLEAN.h"
#include "X_NATURAL.h"
#include "X_CHARACTER.h"
#include "X_STRING.h"
------------------------------- test.f ------------------------------------
#define CAESAR_ADT_EXPERT_F 4.6
#define HelloWorld() "Hello World"
#define TheEnd() "The End"
----------------------------------------------------------------------------
To see the effect, you can type:
lotos.open test.lotos -I$CADP/incl xsimulator
and observe the result:
PRINT !"Hello World"
PRINT !"The End"
C.14.22. How can I split my .t and .f files into several files?
C.14.23. How can I use floating-point constants in my LOTOS specification?
C.14.24. Can I use LOTOS types in my .t file?
C.14.25. How can I debug the code produced by CAESAR.ADT for my LOTOS types?
C.14.26. Why does caesar.adt complain that "file ``.h'' is unwritable"?
caesar.adt: syntax analysis of ``top''
caesar.adt: semantic analysis of ``top''
caesar.adt: - gates binding
caesar.adt: - processes binding
caesar.adt: - types binding
caesar.adt: - signature analysis
caesar.adt: - sorts binding
caesar.adt: - variables binding
caesar.adt: - operations binding
caesar.adt: - functionality analysis
#230 system error:
file ``.h'' is unwritable
quit
It means that writing to file "top.h" is not allowed. Check that the
directory and the file itself have write permission. If not, use the
command "chmod u+w . top.h". This error can also be caused by a
full filesystem: make some cleanup and restart caesar.adt afterwards.
C.15. The CAESAR.BDD tool
C.16. The CAESAR.INDENT tool
C.17. The CAESAR.OPEN tool
C.18. The CONTRIBUTOR tool
C.19. The CUNCTATOR tool
C.20. The DECLARATOR tool
C.21. The DETERMINATOR tool
C.22. The DISTRIBUTOR tool
C.23. The EVALUATOR tool
C.23.1. How can I evaluate mu-calculus formulas in EUCALYPTUS?
C.23.2. xeuca hangs when I try to evaluate a mu calculus file. All I see is "running evaluator .."?
C.23.3. Where can I find a example of mu-calculus formula accepted by Evaluator?
C.23.4. What is _alternation-free_ modal mu calculus?
C.23.5. What are the advantages of EVALUATOR with respect to XTL?
< "SEND" . ("tau"* . "ERROR")* . "tau"* . "RECV" > true
C.23.6. How to handle the data values contained in transition labels?
C.23.7. Can you recommend a publication on the relation between the modal mu-calculus and weak/strong/branching bisimulation?
C.23.8. Can I use CTL to express properties on LNT specifications?
C.23.9. When writing MCL macros, is it necessary to use parentheses around arguments?
macro M (A, P) =
< not A > P
end_macro
may yield a wrong interpretation when it is invoked with the following
arguments:
M (a1 or a2, p1 and p2)
Indeed, this yields after macro expansion the following formula:
< not a1 or a2 > p1 and p2
which is parsed by the EVALUATOR 4.0 tool as follows according to the
precedence of boolean and modal operators:
(< ((not a1) or a2) > p1) and p2
instead of the original intended meaning
< not (a1 or a2) > (p1 and p2)
A clean definition of this macro would therefore be:
macro M (A, P) =
< not (A) > (P)
end_macro
C.23.10. Is there a general method to "promote" a property of a process to a property of a system?
C.23.11. When a MCL formula is evaluated to true on an LTS, why is the diagnostic so big?
C.23.12. I am working on your case study of the alternating bit protocol (demo_01). Here I want to modify the XTL formula contained in bitalt.xtl in a way that invisible actions are not ignored, meaning that after a GET a PUT must follow immediately. Is there a more general solution than 'Box (TAU, false)'?
[ not (A) ] false
which is written in the $CADP/src/xtl/hml.xtl library of XTL as
Box (TAU, false)
C.23.13. I would like to know how to use ACTL formulas with Evaluator 3.x.
(* File prop.mcl *)
(* Include the library *)
library actl.mcl end_library
(* Property : each "GET" will be inevitably followed by a "PUT" *)
AG_A (true, [ "GET" ] AU_A_A (true, true, "PUT", true))
C.23.14. How can I use RAFMC to express the property S||T precedes P?
((S,T) or (T,S)) precedes P
You may express this property using the formula below, which
forbids the undesirable execution sequences (when P occurs
before any S or T; when P occurs after an S but before a T; and
when P occurs after a T but before an S):
[ (not (S or T))* . P ] false
and
[ (not (S or T))* . S . (not T)* . P ] false
and
[ (not (S or T))* . T . (not S)* . P ] false
(Note: this assumes S and T are disjoint action predicates. If they
overlap, you would have to precise the meaning of an action
which simultaneously satisfies S and T).
[ (not (S or T))*] ([P]false and [S . (not T)* . P ] false and [T . (not S)* . P ] false)
The first formula above could be rewritten using a single
regular modality containing the union of the three languages that
you want to forbid in your labelled transition system:
[ ((not (S or T))* . P) |
((not (S or T))* . S . (not T)* . P) |
((not (S or T))* . T . (not S)* . P)
] false
which by factorizing common prefixes and common suffixes yields:
[ (not (S or T))* . (nil | (S . (not T)*) | (T . (not S)*)) . P ] false
This is in fact what was done when factorizing the modalities in
the second formula - but it could be translated into a single modality.
C.23.15. Is there a translation of RAFMC to MC? Or a list of identities like [a][b]false=[a.b]false that hold for the RAFMC formulae?
C.23.16. What is written to evaluator.bcg?
C.23.17. Expressing a property in regular alternation-free mu-calculus
not < true* > (
< 'bad' > true
and
< 'good1' > true
and
< 'good2' > true
)
This means that you cannot reach a state where the three actions are
simultaneously enabled.
C.23.18. When a property is false, how do I read or extract the counterexample?
C.23.19. How can I measure the time is takes to evaluate a temporal logic formula?
C.23.20. Is it possible, in a MCL formula, to capture a data value present on a transition label and reuse it for matching another transition label?
[ true* . {REQUEST ?r:Nat} ] < true* . {RESPONSE !r} > true
where the request 'r' (represented here as a natural number) is captured
by the first action predicate '{REQUEST ?r:Nat}' and used later in the
second action predicate '{RESPONSE !r}'.
C.23.21. Does MCL's parametrization on data mean that one can put variables in actions to quantify over them?
forall P,R:Nat. [ true* . {RELEASE !R !P} ] false
in order to forbid the occurrences of actions of the form
'RELEASE !R !P' in the LTS. The use of quantification over finite data
domains is explained in the EVALUATOR 4.0 manual page (see
EVALUATOR 4.0 man page or type "man evaluator4").
C.23.22. What regular expressions on strings can be used with EVALUATOR?
C.23.23. How can I verify long conjunctive formulas?
[true*. "decide(3, 2)". true*. "decide(2, 5)"] false
and
[true*. "decide(3, 5)". true*. "decide(2, 2)"] false
and
[true*. "decide(3, 2)". true*. "decide(2, 7)"] false
and
.
.
.
then 15 more such conjunctions:
For up to three conjunctions (having 2 "and"s), I can verify a formula but
for more than 3, bcg_open complains about memory.
C.23.24. EVALUATOR 4 and LTL formulas
C.24. The EXECUTOR tool
C.25. The EXHIBITOR tool
C.25.1. The graph B does not match the sequence:
(~ A)*
B
(~ A & ~ B)*
B
C.25.2. I get the following Error: "ld: fatal: file exhibitor: cannot write file; errno=28"?
C.25.3. How can I use EXHIBITOR to search for a given action?
<until> "ERROR !12"
<until> [ERROR.*]
C.26. The EXP.OPEN tool
C.27. The FSP2LOTOS and FSP.OPEN tools
C.28. The GENERATOR tool
C.29. The LNT.OPEN, LNT2LOTOS, and LPP tools
C.30. The OCIS tool
C.30.1. Why is there no time column in OCIS, as on the snapshots of the CADP web page?
C.30.2. What is the difference between OCIS and SIMULATOR/XSIMULATOR?
C.30.3. How can I see timing information in OCIS?
C.30.4. . How can I see message sequence charts in OCIS?
C.30.5. How can I display an execution sequence using OCIS?
C.30.6. How can I get a printout of an execution sequence using OCIS?
C.31. The OPEN/CAESAR library
lotos.open foo.lotos xsimulator
C.31.2. Where can I find the interface descriptions of the OPEN/CAESAR environment?
C.31.3. Where can I find information on how to write a hide or rename file?
C.32. The PREDICTOR tool
C.33. The PROJECTOR tool
C.33.1. What are the intuitive semantics of the semi-composition operator?
C.34. The REDUCTOR tool
C.34.1. What is the on-the-fly reduction algorithm used by Reductor?
C.34.2. How can I use CADP to determinize a finite state automaton?
C.34.3. Is it possible to free an LTS from invisible actions with CADP?
C.35. The SEQ.OPEN tool
C.36. The SIMULATOR/XSIMULATOR tools
C.36.1. I get a core dump as soon as I run XSIMULATOR, on Solaris 2?
lotos.open small.lotos xsimulator
lotos.open: using ``/..../bin.sun5/xsimulator.a''
lotos.open: using link mode
`xsimulator' is up to date.
lotos.open: running ``xsimulator''
Segmentation Fault
C.36.2. Xsimulator can't find the "Times 24" font .
xsimulator.tcl: {Label "OPEN/CAESAR XSIMULATOR" -*-times-bold-r-normal--24-*-*-*-*-*-*-* }
C.36.3. Xsimulator doesn't react when there are too many transitions .
lotos.open file.lotos simulator
C.36.4. How can I execute an xsimulator program on another machine?
mkdir Xsim
mkdir Xsim/com
cp xsimulator Xsim/.
cp -r $CADP/src/xsimulator Xsim
cp -r $CADP/tcl-tk/lib-tcl Xsim
cp -r $CADP/tcl-tk/bin.`$CADP/com/arch` Xsim
cp $CADP/com/arch Xsim/com/arch
setenv CADP /home/user1/Xsim
CADP=/home/user1/Xsim ; export CADP
C.36.5. Can I use the simulator on a reduced graph?
C.36.6. Where is the Windows version of XSIMULATOR?
$CADP/bin.win32/xsimulator.a
$CADP/bin.win32/duplex.exe
C.36.7. Why do I get the message "duplex buffer is full: skipping ... lines"?
C.36.8. Why does Xsimulator gives awful colors on my 256-color monitor?
$CADP/src/xsimulator/main.tcl
$CADP/src/xsimulator/windows.tcl
C.37. The SVL tool
C.38. The TERMINATOR tool
C.38.1. Can TERMINATOR detect all deadlocks?
C.39. The TGV tool
C.39.1. How can I "stress test" the TGV tool?
des (0, 11, 11)
(0, "[^i].*", 1)
(1, "[^i].*", 2)
(2, "[^i].*", 3)
(3, "[^i].*", 4)
(4, "[^i].*", 5)
(5, "[^i].*", 6)
(6, "[^i].*", 7)
(7, "[^i].*", 8)
(8, "[^i].*", 9)
(9, "[^i].*", 10)
(10, ACCEPT, 10)
C.39.2. Is there a way to display comments when generating tests from a test objective using TGV (in a way similar to checking properties in XTL specifications)?
C.40. The XEUCA (Eucalyptus) interface
C.40.1. Is there a a nice X interface for CADP and how can I invoke it?
C.40.2. What is Eucalyptus?
http://vasy.inria.fr/eucalyptus.html
In the framework of these projects, a Graphical User Interface
EUCALYPTUS has been built on top of CADP and other LOTOS tools.
Version 0.* and 1.* of this IHM were distributed separately from CADP
Versions 2.* are integrated in CADP.
C.40.3. What differences are there between versions (0.*-1.*) and Versions 2.*?
C.40.4. I was looking for an Eucalyptus home page, is there any?
C.40.5. Error Message: "ld.so.1: /.../tcl-tk/bin.sun5/wish: fatal: libX11.so.4: can't open file: errno=2"?
*** Variable ``$LD_LIBRARY_PATH'' should be properly set so as
to give access to X11 or OpenWindows dynamic libraries
C.40.6. I have problems in using EUCALYPTUS 1.0 (or 1.1).
C.40.7. Error message using BCG files from mCRL2: "unknown version number 144.22 in bcg_compute_version"
C.41. The XTL tool
D. Suggested enhancements
D.1. Wish list for the next versions of CADP
D.2. Processors/systems to be supported
E. Miscellaneous
E.1. Case-studies and research tools made with CADP
E.1.1. Where can I find a list of practical applications of CADP?
http://cadp.inria.fr/
By clicking on the name of a Case-Study you access a page that describes
the study in further detail, as it appears in the Formal Methods
Application Database, maintained by Nico Plat, available on-line at the
address:
http://www.csr.ncl.ac.uk/projects/FMEInfRes.html
Furthermore, demonstrations of CADP are included in the release and are
available on-line:
http://cadp.inria.fr/ftp/demos/
E.1.2. Has CADP been used in any large-scale industrial projects?
E.2. Any other questions
E.2.1. How can I order the CADP toolbox?
URL: http://cadp.inria.fr/
E.2.2. Is there a CADP mailing-list?
E.2.3. Could I be added to the CADP mailing-list?
E.2.6. How can I obtain CLEOPATRE or XESAR?
E.2.7. How can I connect CADP to the Concurrency Workbench?
bcg_io your_filename.bcg your_filename.cwb
bcg_io your_filename.aut your_filename.cwb
E.2.8. How can I get the Fc2Tools?
E.2.9. How can I use the Fc2Tools to minimise a .bcg or a .aut file?
bcg_io file.bcg file.fc2
fc2explicit -s file.fc2 > file_min.fc2
bcg_io file_min.fc2 file_min.bcg
E.2.10. How can I use the Fc2Tools to compare two LTS files (in formats .aut or .bcg)?
bcg_io file1.bcg .fc2 bcg_io file2.bcg .fc2
fc2explicit -seq file1.fc2 file2.fc2
E.2.11. How can I visualize a .bcg or a .aut file using Autograph?
bcg_io file1.bcg .fc2
atg file1.fc2
E.2.12. Can I use the Fc2tools to verify a .exp file?
E.2.13. What's a deadlock state?
E.2.14. What's the VLTS benchmark suite?
E.2.15. In VLTS, is it the case that systems with deadlocked states are faulty systems and that deadlocked states were undesirable?
E.2.16. What is the nature of the VASY systems included in the benchmark? Is there any documentation as to what systems they are derived from?
E.2.16. Is it possible to use Discrete-Time Markov Chains (DTMCs) or Continuous-Time Markov Chains (CTMCs) as specification formalism for CADP?
Version 1.227 - Date 2024/01/13 10:02:39
Back to the CADP Home Page