CADP FAQ

Frequently Asked Questions / Forum Aux Questions

about the CADP Software

This a collection of Frequently Asked Questions (FAQ) asked by the many users of CADP (Construction and Analysis of Distributed Processes) over the years. This FAQ was created in 1997 by Hubert Garavel and Mark Jorgensen. Since then, it was extended with contributions from Solofo Ramangalahy, Hubert Garavel, Nicolas Descoubes, David Champelovier, Radu Mateescu, Christine McKinty and Wendelin Serwe. Please visit also the CADP forum, which answers many questions not addressed yet in this FAQ. If you question has not been addressed in either this FAQ or the Forum, please ask it in the Forum or, if that's not possible, send it by email to cadp@inria.fr.

Separator


Table of contents

General questions

Questions about languages

Questions regarding CADP tools

Suggested enhancements

Miscellaneous


A  General questions Up

A.1  Installation and troubleshooting
    A.1.1  On which kind of machines/operating systems can I use CADP?
    A.1.2  What is CADP's size?
    A.1.3  Where can I find the installation directives?
    A.1.4  How can I upgrade my version of CADP?
    A.1.5  How can I obtain a license number for CADP?
    A.1.6  Who should be able to access the LICENSE file?
    A.1.7  Is the software restricted to use in a subnet or on single hosts?
    A.1.8  What information do you need to create a licence file for us?
    A.1.9  How long is the license valid for?
    A.1.10  How do I know when my licence will expire?
    A.1.11  I get the following error: "License Error: The license for this product(SPARC ompiler C) has expired"?
    A.1.12  The directory containing CADP on your FTP site is empty!
    A.1.13  The CADP tools do not find the "cpp" command?
    A.1.14  My license has expired. What should I do?
    A.1.15  Error Message: "wrong global checksum"?
    A.1.16  Error Message: "wrong binary checksum"?
    A.1.17  I am using CADP on several hosts. What is the easiest way to install it?
    A.1.18  The server and the clients have heterogeneous architectures. Does CADP supports it?
    A.1.19  The clients are used as X terminals. Should I mention them in the "rfl" command?
    A.1.20  Error Message: "no appropriate license"?
    A.1.21  Can I install CADP on my home PC?
    A.1.22  Would it be possible to use scp instead of rcp in rfl?
    A.1.23  My license expired. What should I do?
    A.1.24  What's the procedure to get a localhost based CADP license for a laptop?
    A.1.25  What should I do when I encounter problems with CADP?
    A.1.26  Where should I send bug reports?
    A.1.27  My administrator says that this CADP tool requires many environments that he might not have?
    A.1.28  Which version of the CADP environment did I download?
    A.1.29  Error Message: "Too many heap sections"?
    A.1.30  Error Message "libgc.a: warning: table of contents for archive is out of date; rerun ranlib(1)"?
    A.1.31  I can't find lotos.open, Maybe my installation is not correct?
    A.1.32  On Windows, Installator displays "error reading "sockXXX": connection reset by peer"
    A.1.33  On Windows, I get errors messages "$'\r': command not found"
    A.1.34  Why does CAESAR and/or CAESAR.ADT complain that "library file ``XXX.lib'' is unreadable"?
    A.1.35  The BCG tools do not find the "what" command !
    A.1.36  Error message: "bcg_file_area: include area does not exist ....."?
    A.1.37  Are there any restrictions on who can use CADP?
    A.1.38  How do I get a license for a machine that is not connected to the Internet or cannot send mail?
    A.1.39  RFL fails because it cannot establish an RSH connection
    A.1.40  How to get a CADP license for an additional machine?
    A.1.41  How can I extend the license?
    A.1.42  How can I tell whether RFL worked? Running tst after it fails.
    A.1.43  RFL fails with "`tty` Ambiguous" message
    A.1.44  RFL blocks at "RFL (phase 1): testing machine_name"
    A.1.45  RFL fails with scp usage message
    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?
    A.1.47  How can I get licenses for more machines?
    A.1.48  Error message; "No appropriate license"
    A.1.49  Why has my CADP license expired?
    A.1.50  Error message: "Wrong domain name"
    A.1.51  Can I get a copy of CADP on CD-ROM?
    A.1.52  Do diskless clients need licenses?
    A.1.53  Server with two IP addresses
    A.1.54  Can I use CADP on a laptop with no fixed IP address?
    A.1.55  Is it really necessary to run RFL remotely?
    A.1.56  My laptop doesn't have FTP. How can I install CADP?
    A.1.57  How can I check that installation and licensing was successful?
    A.1.58  How can I check that I'm runnng the latest version of CADP?
    A.1.59  Can I rename the installation directory after installation and licensing?
    A.1.60  Is it possible to install a new version of CADP while keeping the existing version?
    A.1.61  Are there any special considerations when generating licenses for a demo system?
    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?
    A.1.63  Error "can't find a usable init.tcl" when installing on Windows
    A.1.64  No files visible in FTP directory
    A.1.65  Do I need to run RFL after INSTALLATOR?
    A.1.66  Errors running cadp_cygwin.com
    A.1.67  Can I run CADP on a virtual machine?
    A.1.68  Error message says license file is unreadable
    A.1.69  Can I run CADP on my laptop when it is disconnected and connected?
    A.1.70  On Windows, must CADP be in C:?
    A.1.71  If I change my Linux installation, will my CAPD license still be valid?
    A.1.72  Questions about installator.shar
    A.1.73  Error "couldn't set locale correctly" during manual installation on Unix
    A.1.74  How can I tell what version of CADP I'm running?
    A.1.75  Error "uncompress: corrupt input"
    A.1.76  Will CADP run on my Linux system?
    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
    A.1.78  On Windows, CADP does not understand symbolic links
    A.1.79  Error message "ld terminated with signal 11 [Segmentation fault], core dumped"
    A.1.80  CADP errors on Mac when name changes
    A.1.81  Error message "*015 protection violation: ... wrong Internet address 192.168.56.1"
    A.1.82  Error message "*033 protection violation" on certain versions of Ubuntu

A.2  The INSTALLATOR tool
    A.2.1  Can I install through a proxy server?
    A.2.2  How do I launch "installator.com" on a Win32 system?
    A.2.3  Can I use Installator on a machine with no FTP?
    A.2.4  What's the interface to the manual installation procedure?
    A.2.5  Why does installation fail on Solaris with the message "stty: : Invalid argument"?
    A.2.6  Where should I store the installator.com file?
    A.2.7  Installator error message: "can't unset "state(data)": no such element in array"

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?
    A.4.2  How do you find out whether an action is reachable or not?
    A.4.3  What is the maximum size of the graphs CADP tools can handle?

A.5  Questions about equivalence checking
    A.5.1  How can I check refinement with the CADP tools?

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?
    A.7.3  Is there more documentation than in the man pages and in the $CADP/doc directory available?
    A.7.4  Demo 19 doesn't work: "Travelling crane - stop on upper end reached" .
    A.7.5  I'm new to CADP: what's the best way to get started?

B  Questions about languages Up

B.1  The LOTOS language
    B.1.1  Where can I find ISO standards written in LOTOS?
    B.1.2  How can I split my LOTOS description into several files?
    B.1.3  How can I replace recursions on the left-hand side of disable?
    B.1.4  Visibility problem with values received on gates?
    B.1.5  Is there an if-then-else instruction in LOTOS?
    B.1.6  Do you have tools that make LOTOS programming easier?
    B.1.7  What is LOTOS?
    B.1.8  What is Basic LOTOS?
    B.1.9  Does LOTOS allow to hide actions based on both gate names and values?
    B.1.10  What is the semantics of LOTOS?
    B.1.11  Does LOTOS support object-orientation?
    B.1.12  Can LOTOS handle concurrency?
    B.1.13  Is LOTOS executable?
    B.1.14  What sorts of systems can be described in LOTOS?
    B.1.15  Where can I find a LOTOS-mode for emacs?
    B.1.16  Which subset of LOTOS is accepted by CAESAR and CAESAR.ADT?
    B.1.17  How should I handle probabilistic or timed transitions in a LOTOS specification?

B.2  The EXP language
    B.2.1  NEW What is the EXP language of CADP?
    B.2.2  NEW Is the EXP language compositional?

B.3  The MCL (Mu-calculus) language

B.4  The SVL language
    B.4.1  Why does ALDEBARAN fail on some .exp files?
    B.4.2  Why using the parallel FC2 format may fail?

B.5  The XTL language
    B.5.1  How do I run XTL?
    B.5.2  Is it possible to have some additional documentation about XTL?
    B.5.3  How can I handle the data values contained in transition labels?
    B.5.4  Is XTL able to give an error-trail when a property is not true?
    B.5.5  Error: aucune possibilite de liaison pour la variable

B.6  The LNT language
    B.6.1  NEW What is the difference between LOTOS NT and LNT?
    B.6.2  NEW What are the differences between LNT2LOTOS and TRAIAN?
    B.6.3  NEW Where is the reference manual for LNT?
    B.6.4  NEW Does LNT support type aliasing (like "type ID is Nat")?
    B.6.5  NEW How to debug a LNT specification that makes a segmentation fault?
    B.6.6  NEW How to compile and execute an LNT specification?

B.7  Other languages
    B.7.1  What is the current status of E-LOTOS?
    B.7.2  Do you plan to adapt CADP to E-LOTOS?
    B.7.3  Are you aware of any model checking work in the context of Erlang?
    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 Up

C.1  The ALDEBARAN tool
    C.1.1  The -path option of ALDEBARAN does not give me the shortest path!
    C.1.2  How do I get the branching factor of a .bcg file?
    C.1.3  Why does my .aut files contain some actions with quotes and some actions without quotes?
    C.1.4  How to convert a .aut file to another format?
    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?

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?

C.5  The BCG_IO tool
    C.5.1  BCG_IO issues the "bcg_edge: previous state are not increasing in BCG_WRITE_EDGE" Error Message.

C.6  The BCG_LABELS tool
    C.6.1  How can I rename or hide transition labels in a BCG file?

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?
    C.8.2  NEW 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!
    C.8.4  NEW A hidden transition between non observationally equivalent states disappears after observational minimization!

C.9  The BCG_OPEN tool
    C.9.1  Error message "unknown version number 0.0 in bcg_compute_version" when running BCG_OPEN in two windows

C.10  The BCG_READ and BCG_WRITE APIs
    C.10.1  I am currently developing a tool, and would like to produce output in the BCG format. How can I do it?
    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?
    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"?
    C.13.6  How can I find out the number of states generated while CAESAR is running?
    C.13.7  Error Message: "theoretical limitation during restriction: process recursion through some forbidden operator"
    C.13.8  Is it possible to mix recursion and parallel composition?
    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  NEW 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"?
    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?
    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?
    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?
    C.14.13  In my ``.t'' file, I cannot use the C types generated from my LOTOS code.
    C.14.14  The Natural library only contains natural number digits up to 9. Can I go beyond this?
    C.14.15  In LOTOS, can I define natural numbers with more than 256 values?
    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?
    C.14.19  Is it possible to use naturals but to have them implemented using natural C integers?
    C.14.20  What do CAESAR_ADT_EXPERT_T and CAESAR_ADT_EXPERT_F mean? Which values should I give them?
    C.14.21  How do I use characters and strings in a LOTOS specification?
    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"?

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?
    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?
    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)'?
    C.23.13  I would like to know how to use ACTL formulas with Evaluator 3.x.
    C.23.14  How can I use RAFMC to express the property S||T precedes P?
    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
    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?
    C.23.21  Does MCL's parametrization on data mean that one can put variables in actions to quantify over them?
    C.23.22  What regular expressions on strings can be used with EVALUATOR?
    C.23.23  How can I verify long conjunctive formulas?
    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:
    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?

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
    C.31.1  The graph generated by CAESAR is too large. How can I verify my LOTOS description on-the-fly?
    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?
    C.36.2  Xsimulator can't find the "Times 24" font .
    C.36.3  Xsimulator doesn't react when there are too many transitions .
    C.36.4  How can I execute an xsimulator program on another machine?
    C.36.5  Can I use the simulator on a reduced graph?
    C.36.6  Where is the Windows version of XSIMULATOR?
    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?

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?
    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?
    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"?
    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
    C.41.1  What verification tool should I use: ALDEBARAN or XTL? XTL seems more adequate for the verification of properties. Are there properties that can be handled using ALDEBARAN?

D  Suggested enhancements Up

D.1  Wish list for the next versions of CADP

D.2  Processors/systems to be supported

E  Miscellaneous Up

E.1  Case-studies and research tools made with CADP
    E.1.1  Where can I find a list of practical applications of CADP?
    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?
    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?
    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?
    E.2.10  How can I use the Fc2Tools to compare two LTS files (in formats .aut or .bcg)?
    E.2.11  How can I visualize a .bcg or a .aut file using Autograph?
    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?



A. General questions

A.1. Installation and troubleshooting

Up 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.


Up 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.


Up 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 cadp@inria.fr.

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".


Up 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 cadp@inria.fr mentioning that you would like to upgrade.


Up 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.


Up 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


Up 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.


Up 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.


Up 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 !


Up 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.


Up 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.


Up 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.


Up A.1.13. The CADP tools do not find the "cpp" command?

Run 'tst' and update your $PATH as explained


Up 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).


Up 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:


Up A.1.16. Error Message: "wrong binary checksum"?

[Thu Sep 25 18:57:31 MEST 2003]


Up 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 cadp@inria.fr


Up 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.


Up 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.


Up 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 cadp@inria.fr


Up 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.


Up 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.


Up 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.


Up 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).


Up A.1.25. What should I do when I encounter problems with CADP?


Up A.1.26. Where should I send bug reports?

Send them by E-mail to cadp@inria.fr


Up 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.


Up 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.


Up 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.


Up 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.*


Up 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.


Up 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


Up 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


Up 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:


Up A.1.35. The BCG tools do not find the "what" command !

Run 'tst' and update your $path as explained.


Up 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.


Up 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.


Up 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.


Up 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` 


Up 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 cadp@inria.fr
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)).


Up 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 cadp@inria.fr


Up 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


Up 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.


Up 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.


Up 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.


Up 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.


Up 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 cadp@inria.fr
We will reply with the final license file covering all your machines.


Up 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.


Up 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.


Up 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.


Up 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.


Up 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.


Up 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.


Up 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".


Up 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.


Up 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.


Up 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.


Up 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).


Up 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.


Up 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.


Up 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).


Up 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.


Up 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.


Up 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).


Up 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.


Up 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").


Up 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.


Up 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/tst
and check the result.


Up 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   localhost
Then edit /etc/rc.local and append the following line (replacing mydomain with your real domaim name):
		domainname	mydomain


Up 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.


Up 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!


Up 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.


Up 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.


Up A.1.74. How can I tell what version of CADP I'm running?

Type the following command:

	   grep VERSION $CADP/VERSION | tail -1


Up 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.


Up 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.


Up 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.


Up 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.


Up 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.


Up 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'')
	   abandon
The solution is to run the $CADP/com/tst command, which will detect the problem and display instructions for defining a static hostname.


Up 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.


Up 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

Up 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.


Up 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.com 	
or
	   /bin/sh installator.com -beta


Up 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.


Up 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.


Up 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.


Up 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.


Up 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

Up 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.


Up 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.

The command to type will then be:

	lotos.open file.lotos  exhibitor < toto.seq

But in this case, no diagnostic sequence leading to "ERROR_ACTION" is computed.

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


Up 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

Up 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

Up A.7.1. Where can I find documentation on CADP?


Up 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.


Up 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


Up 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"


Up 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

Up 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" .


Up B.1.2. How can I split my LOTOS description into several files?

Two solutions:


Up 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


Up 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
	        )


Up 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:

You can replace V by a boolean variable:

		let OK:BOOL = V in (([OK] -> B1) [] [not (OK)] -> B2)

You can then write directly your conditional statement "if V then B1 else B2 endif"


Up 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 leduc@montefiore.ulg.ac.be, 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.


Up 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:


Up 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).


Up 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.


Up 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.


Up 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.


Up 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).


Up 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.


Up 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:


Up 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.


Up 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.*".


Up 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

Up B.2.1. NEW 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.


Up B.2.2. NEW 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

Up 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.


Up 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

Up B.5.1. How do I run XTL?

[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.


Up 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).


Up 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)".


Up 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.*".


Up 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]
	     abandon
What 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

Up B.6.1. NEW 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.


Up B.6.2. NEW 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.


Up B.6.3. NEW 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.


Up B.6.4. NEW 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 type
defines 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 type
You can also define a range type
	type ID is range 0 .. 100 of Nat end type


Up B.6.5. NEW 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_TMP
or
	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.bcg
or, if you have a particular main progress to specify:
	lnt.open -root My_PROCESS MY_PROGRAM.lnt generator OUT.bcg
This should end with an error message of the form
	lotos.open: running ``generator OUT.bcg'' for ``MY_PROGRAM.lotos''
	Segmentation fault
Launch then the debugger on the "generator" program, e.g.:
	gdb generator
and type the two commands to run the program and inspect the stack:
	run OUT.bcg
	where


Up B.6.6. NEW 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

Up 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


Up 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.


Up 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:

Development of a Verified Erlang Program for Resource Locking

Verifying Fault-Tolerant Erlang Programs

Formal Analysis of Erlang's Open Telecom Platform Library Components

Model-Checking Erlang


Up 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?

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).

C. Questions regarding CADP tools

C.1. The ALDEBARAN tool

Up C.1.1. The -path option of ALDEBARAN does not give me the shortest path!

[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

	aldebaran -path S FILE.bcg

might not give you the shortest path. You should use:

	bcg_info -path S FILE.bcg


Up C.1.2. How do I get the branching factor of a .bcg file?

[Fri Sep 26 18:19:47 MEST 2003]

This can be done by typing

	bcg_info -branching FILE.bcg


Up C.1.3. Why does my .aut files contain some actions with quotes and some actions without quotes?

[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:

	bcg_io $1.bcg $1.aut
on any BCG file.


Up C.1.4. How to convert a .aut file to another format?

[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:

	bcg_io $1.bcg $1.aut


Up C.1.5. "No more memory" error when reducing a state space

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).


Up C.1.6. Can Aldebaran produce a record of the renaming of states during propjection?

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.


Up C.1.7. Using branching equivalence, can Aldebaran display information about where two LTSs are not equivalent?

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.


Up C.1.8. What is the correct syntax for specifying the name of a gate in an AUT (.aut) file?

As stated in the aldebaran man page, the gate name must be enclosed in double quotes: "". The exception to this is i, the invisible action, for which double quotes must not be used (unless you really want a gate named "i").


Up C.1.9. How can I manipulate a trace produced with the -path option of ALDEBARAN?

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:

	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

Up C.2.1. Why does BCG_DRAW produce double-tipped arrows when drawing a BCG file?

[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.


Up C.2.2. Can BCG_DRAW produce output in xfig format?

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.


Up C.2.3. What is BCG format?

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".


Up C.2.4. How can I know the names of the BCG variables representing the variables of a LOTOS program?

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).


Up C.2.5. Can I use a normal editor to edit a BCG file?

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.



C.3. The BCG_GRAPH tool


C.4. The BCG_INFO tool

Up C.4.1. Is there a way to know the size of a bcg graph without calling ALDEBARAN?

[Fri Jun 6 16:14:14 MET DST 1997]

Yes. Type:

	  bcg_info FILE.bcg


C.5. The BCG_IO tool

Up C.5.1. BCG_IO issues the "bcg_edge: previous state are not increasing in BCG_WRITE_EDGE" Error Message.

[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.:

	des (0, 6, 7)
	(0, F, 6)
	(4, E, 5)
	(0, C, 3)
	(1, B, 2)
	(3, D, 4)
	(0, A, 1)

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:

            bcg_edge: previous state are not increasing in BCG_WRITE_EDGE

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



C.6. The BCG_LABELS tool

Up C.6.1. How can I rename or hide transition labels in a BCG file?

The BCG_LABELS tool provides these features and operates on BCG files. For instance,

		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

You can also have renaming patterns, including regular expressions. For instance,

		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".

Note that these renamings can also be performed using SVL scripts. The first example above can be rewritten in SVL as follows:

	"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

Up C.8.1. How can I minimize a .aut file using BCG_MIN?

[Mon Nov 8 10:06:38 MET 2004]

You first have to convert the .aut file into a .bcg file

	bcg_io FILE.aut FILE.bcg

Then, run bcg_min:

	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

For further details, please consult the bcg_min page.


Up C.8.2. NEW What is the largest graph minimized by BCG_MIN?

[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.


Up C.8.3. Stochastic branching reduction of two strongly equivalent graphs yields graphs of different sizes!

[Mon Feb 28 16:05:16 MET 2005]

Reducing two strongly bisimilar BCG graphs modulo branching stochastic bisimulation using BCG_MIN, precisely,

	bcg_min -branching -rate ...
may produce BCG graphs of different sizes, i.e., with different numbers of states and/or transitions.

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:

	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.


Up C.8.4. NEW A hidden transition between non observationally equivalent states disappears after observational minimization!

[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):

	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).

Observational minimization thus produces the following graph:

	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.

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.



C.9. The BCG_OPEN tool

Up C.9.1. Error message "unknown version number 0.0 in bcg_compute_version" when running BCG_OPEN in two windows

Running BCG_OPEN in two different windows caused the following problem:

	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

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.



C.10. The BCG_READ and BCG_WRITE APIs

Up C.10.1. I am currently developing a tool, and would like to produce output in the BCG format. How can I do it?

[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:

	LDFLAGS = "-L${BCG:-$CADP}/bin.`$CADP/com/arch` -lBCG_IO -lBCG -lm";

See file $CADP/src/open_caesar/generator.c for an example of BCG output.


Up C.10.2. Where can I find documentation on the definition of the BCG format?

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.


Up C.10.3. Is there a way to write comments in a BCG file?

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.



C.11. The BCG_STEADY and BCG_TRANSIENT tools


C.12. The BISIMULATOR tool


C.13. The CAESAR tool

Up 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'  

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).


Up C.13.2. Why does CAESAR stop during the "generation" phase?

[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.


Up C.13.3. How can I accelerate the graph generation?

[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.


Up C.13.4. How can I produce the minimal graph?

[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.


Up C.13.5. Error Message: "ld: fatal: file /tmp/caesar_6888.x: cannot msync file; errno=12"?

[Mon Apr 21 13:52:32 MET DST 1997]

	   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 ..

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 .)


Up C.13.6. How can I find out the number of states generated while CAESAR is running?

[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

	   bcg_info FILE.bcg


Up C.13.7. Error Message: "theoretical limitation during restriction: process recursion through some forbidden operator"

[Tue Nov 4 17:33:45 MET 1997]

This problem occured with the following LOTOS code:

	process P [G] : noexit := 
		G ? ... ; ...  
		||| 
		i; P [G] 
	endproc

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:

	P [G] ||| P [G] ||| ... ||| P [G]

or

	i; P [G] ||| i; P [G] ||| ... ||| i; P [G]


Up C.13.8. Is it possible to mix recursion and parallel composition?

[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?

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

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:

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


Up C.13.9. Error Message: "root process having value parameters"

[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.


Up C.13.10. What is the maximum size of LOTOS specifications CAESAR can handle?

[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}".


Up C.13.11. Where can I find information about the EXEC/CAESAR environment?

[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.


Up 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?

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.


Up C.13.13. NEW Why does CAESAR a segmentation fault during the "simulation" phase?

[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 cadp@inria.fr



C.14. The CAESAR.ADT tool

Up C.14.1. CAESAR.ADT does not find the `indent' command?

Run 'tst' and update your $path as explained or invoke CAESAR.ADT with option -indent


Up C.14.2. Does CAESAR.ADT deal with parameterized types?

[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.


Up C.14.3. Does CAESAR.ADT deal with renamed types?

Yes, the 'renamedby' construct is handled properly.


Up C.14.4. Where can I find the LOTOS standard library (containing predefined types such as booleans, bits, integers, etc)?

[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.


Up C.14.5. Error Message: "Theoretical limitation: domain of an infinite (or complex) sort cannot be enumerated"?

[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:

		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

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:

	#define ITERATOR(X) for (X=element_of_sort; X < limit_itr_of_sort; X=next_element) 

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.

		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;
		}

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).


Up C.14.6. What is the meaning of the following annotations: "(*! implementedby X comparedby Y enumeratedby Z printedby T *)"?

[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.


Up C.14.7. How can I restrict iteration on integers from 0..255 to 0..n?

[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:

#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)

With previous versions of CADP (before 2004), you should have used the following lines:

#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))


Up C.14.8. Where can I find the concrete C implementation for Y_QUEUE.lib and Y_SET.lib?

[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).


Up C.14.9. How do I use library files that are not in $CADP/lib nor in the current directory?

[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.


Up C.14.10. Are there short-circuit "and" and "or" expressions in LOTOS?

[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:

	library BOOLEAN

with:

	library X_BOOLEAN

and create .t file containing the following lines:

        #define CAESAR_ADT_EXPERT_T 4.4
        #include "X_BOOLEAN.h"

and a .f file containg the line:

	#define CAESAR_ADT_EXPERT_F 4.4

In the X_BOOLEAN library, the "and" and "or" operators are always short-circuit.


Up C.14.11. In the generated .h file, why do fatal errors call "kill(getpid(), 15)" rather than "exit(1)"?

[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.


Up C.14.12. How can I use the C code generated for enumerated types in my own C program?

[Thu Nov 28 10:31:25 MET 2002]

You add special comments "implementedby" to the constructors.
The syntax to use the constructors on your C program is F() (for example TRUE() or FALSE(), do not forget the parentheses).


Up C.14.13. In my ``.t'' file, I cannot use the C types generated from my LOTOS code.

[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:

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.


Up C.14.14. The Natural library only contains natural number digits up to 9. Can I go beyond this?

[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:

		type ExtendedNatural is Natural
		opns 
			10, 11, 20 : -> Nat
		eqns
			ofsort Nat
				10 = Succ (9);
				11 = Succ (10);
				20 = 10 + 10;
		endtype

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.


Up C.14.15. In LOTOS, can I define natural numbers with more than 256 values?

[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

	        library X_NATURAL endlib

instead of

	        library NATURAL endlib

You should also create in your current directory a ".t" file containing the following lines

		#define CAESAR_ADT_EXPERT_T 5.0
		#include "X_NATURAL.h"

and a ".f" file containing

		#define CAESAR_ADT_EXPERT_F 5.0

(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).


Up C.14.16. When I run caesar or lotos.open, it complains that I haven't got a ".f" file

[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.


Up C.14.17. Can I import C types and functions into my LOTOS description?

[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.


Up C.14.18. How can I define the 'eq' operator on enumerated types?

[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:

        ofsort bool

		x eq x = true;
		x eq y = false;

The equations for 'ne' would be:

		x ne y = not (x eq y);


Up C.14.19. Is it possible to use naturals but to have them implemented using natural C integers?

[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:

	$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.


Up C.14.20. What do CAESAR_ADT_EXPERT_T and CAESAR_ADT_EXPERT_F mean? Which values should I give them?

[Tue Sep 2 09:46:45 MEST 2003]

At the beginning of your .t file (if you write one), you have to write:

		#define CAESAR_ADT_EXPERT_T 5.1
and to add a similar line in your .f file, with CAESAR_ADT_EXPERT_F.

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.


Up C.14.21. How do I use characters and strings in a LOTOS specification?

[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:

         ------------------------------- 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"


Up C.14.22. How can I split my .t and .f files into several files?

[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.


Up C.14.23. How can I use floating-point constants in my LOTOS specification?

[Wed Sep 3 08:34:03 MEST 2003]

See the demo_19 (in $CADP/demos/demo_19) to see how this can be done.


Up C.14.24. Can I use LOTOS types in my .t file?

[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.


Up C.14.25. How can I debug the code produced by CAESAR.ADT for my LOTOS 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.


Up C.14.26. Why does caesar.adt complain that "file ``.h'' is unwritable"?

[Mon Nov 8 10:06:38 MET 2004]

If you get a message that looks like this:

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

Up C.23.1. How can I evaluate mu-calculus formulas in EUCALYPTUS?

[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').


Up C.23.2. xeuca hangs when I try to evaluate a mu calculus file. All I see is "running evaluator .."?

[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.


Up C.23.3. Where can I find a example of mu-calculus formula accepted by Evaluator?

[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.


Up C.23.4. What is _alternation-free_ modal mu calculus?

[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.


Up C.23.5. What are the advantages of EVALUATOR with respect to XTL?

[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 "< >":

	< "SEND" . ("tau"* . "ERROR")* . "tau"* . "RECV" > true

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).


Up C.23.6. How to handle the data values contained in transition labels?

[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.


Up C.23.7. Can you recommend a publication on the relation between the modal mu-calculus and weak/strong/branching bisimulation?

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.


Up C.23.8. Can I use CTL to express properties on LNT specifications?

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.


Up C.23.9. When writing MCL macros, is it necessary to use parentheses around arguments?

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

	  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


Up C.23.10. Is there a general method to "promote" a property of a process to a property of a system?

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.


Up C.23.11. When a MCL formula is evaluated to true on an LTS, why is the diagnostic so big?

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.


Up 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)'?

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:

	   [ not (A) ] false
which is written in the $CADP/src/xtl/hml.xtl library of XTL as
	   Box (TAU, false)


Up C.23.13. I would like to know how to use ACTL formulas with Evaluator 3.x.

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:

	(* 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))

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").


Up C.23.14. How can I use RAFMC to express the property S||T precedes P?

This property is:

	     ((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).

The property can also be expressed as

	 [ (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.

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).


Up 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?

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


Up C.23.16. What is written to evaluator.bcg?

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").


Up C.23.17. Expressing a property in regular alternation-free mu-calculus

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:

	    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.


Up C.23.18. When a property is false, how do I read or extract the counterexample?

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.


Up C.23.19. How can I measure the time is takes to evaluate a temporal logic formula?

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).


Up 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?

Yes. In MCL, you can specify the following formula:

	  [ 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}'.


Up C.23.21. Does MCL's parametrization on data mean that one can put variables in actions to quantify over them?

Yes. For example, it is possible to write formulas like:

	    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").


Up C.23.22. What regular expressions on strings can be used with EVALUATOR?

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.


Up C.23.23. How can I verify long conjunctive formulas?

Detailed question: Using Evaluator 3, How can I verify a formula such as the following:


	 [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.

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.


Up C.23.24. EVALUATOR 4 and LTL formulas

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 "< ... > @".



C.24. The EXECUTOR tool


C.25. The EXHIBITOR tool

Up C.25.1. The graph B does not match the sequence:

	  (~ A)*
	  B 

This is normal as there is a conflict between A and B. Use the -conflict option, or write

	  (~ A & ~ B)*
	  B

Please refer to the updated exhibitor manpage


Up C.25.2. I get the following Error: "ld: fatal: file exhibitor: cannot write file; errno=28"?

[Fri Nov 7 15:07:04 MET 1997]

This problem occurs when your disk is full ! Check it out, and make some room.


Up C.25.3. How can I use EXHIBITOR to search for a given action?

[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:

	<until> "ERROR !12"

or

	<until> [ERROR.*]

It is best to do this type of search on-the-fly using lotos.open



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

Up C.30.1. Why is there no time column in OCIS, as on the snapshots of the CADP web page?

[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.


Up C.30.2. What is the difference between OCIS and SIMULATOR/XSIMULATOR?

[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.


Up C.30.3. How can I see timing information in OCIS?

[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.


Up C.30.4. . How can I see message sequence charts in OCIS?

[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.


Up C.30.5. How can I display an execution sequence using OCIS?

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).


Up C.30.6. How can I get a printout of an execution sequence using OCIS?

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.



C.31. The OPEN/CAESAR library

Up C.31.1. The graph generated by CAESAR is too large. How can I verify my LOTOS description on-the-fly?

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:

        	lotos.open foo.lotos xsimulator

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.


Up C.31.2. Where can I find the interface descriptions of the OPEN/CAESAR environment?

[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/*".


Up C.31.3. Where can I find information on how to write a hide or rename file?

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



C.32. The PREDICTOR tool


C.33. The PROJECTOR tool

Up C.33.1. What are the intuitive semantics of the semi-composition operator?

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.



C.34. The REDUCTOR tool

Up C.34.1. What is the on-the-fly reduction algorithm used by Reductor?

[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.


Up C.34.2. How can I use CADP to determinize a finite state automaton?

Use the REDUCTOR tool with the -trace and -total options. See the reductor man page for information about the tool and its options.


Up C.34.3. Is it possible to free an LTS from invisible actions with CADP?

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.



C.35. The SEQ.OPEN tool


C.36. The SIMULATOR/XSIMULATOR tools

Up C.36.1. I get a core dump as soon as I run XSIMULATOR, on Solaris 2?

[Mon Apr 21 13:52:32 MET DST 1997]

	    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

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


Up C.36.2. Xsimulator can't find the "Times 24" font .

[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:

	    xsimulator.tcl:   {Label  "OPEN/CAESAR    XSIMULATOR" -*-times-bold-r-normal--24-*-*-*-*-*-*-* }

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).


Up C.36.3. Xsimulator doesn't react when there are too many transitions .

[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:

		lotos.open file.lotos simulator


Up C.36.4. How can I execute an xsimulator program on another machine?

[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:

	  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

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.

	  setenv CADP /home/user1/Xsim

if you are using csh, or

	  CADP=/home/user1/Xsim ; export CADP

if you are using sh.


Up C.36.5. Can I use the simulator on a reduced graph?

[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


Up C.36.6. Where is the Windows version of XSIMULATOR?

[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

	$CADP/bin.win32/xsimulator.a
	$CADP/bin.win32/duplex.exe

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.


Up C.36.7. Why do I get the message "duplex buffer is full: skipping ... lines"?

[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.


Up C.36.8. Why does Xsimulator gives awful colors on my 256-color monitor?

[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:

	$CADP/src/xsimulator/main.tcl
	$CADP/src/xsimulator/windows.tcl

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).



C.37. The SVL tool


C.38. The TERMINATOR tool

Up C.38.1. Can TERMINATOR detect all deadlocks?

[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>



C.39. The TGV tool

Up C.39.1. How can I "stress test" the TGV tool?

The automaton below represents a set of execution traces and can be used as a "stress test" for TGV because of its high complexity.

	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)


Up 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)?

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.



C.40. The XEUCA (Eucalyptus) interface

Up C.40.1. Is there a a nice X interface for CADP and how can I invoke it?

Yes ! It's called Eucalyptus an is invoked by typing xeuca .


Up C.40.2. What is Eucalyptus?

First of all 2 european/canadian projects from 1994 to 1996. For more information visit the WWW page:
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.


Up C.40.3. What differences are there between versions (0.*-1.*) and Versions 2.*?

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.


Up C.40.4. I was looking for an Eucalyptus home page, is there any?

Yes ! http://vasy.inria.fr/eucalyptus.html


Up C.40.5. Error Message: "ld.so.1: /.../tcl-tk/bin.sun5/wish: fatal: libX11.so.4: can't open file: errno=2"?

[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:

		*** Variable ``$LD_LIBRARY_PATH'' should be properly set so as
		    to give access to X11 or OpenWindows dynamic libraries


Up C.40.6. I have problems in using EUCALYPTUS 1.0 (or 1.1).

[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.


Up C.40.7. Error message using BCG files from mCRL2: "unknown version number 144.22 in bcg_compute_version"

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.



C.41. The XTL tool

Up C.41.1. What verification tool should I use: ALDEBARAN or XTL? XTL seems more adequate for the verification of properties. Are there properties that can be handled using ALDEBARAN?

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.

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

Up E.1.1. Where can I find a list of practical applications of CADP?

You may find a list of Case-Studies on the WWW page:
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/


Up E.1.2. Has CADP been used in any large-scale industrial projects?

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.



E.2. Any other questions

Up E.2.1. How can I order the CADP toolbox?

See the WWW page
URL: http://cadp.inria.fr/


Up E.2.2. Is there a CADP mailing-list?

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 cadp@inria.fr.


Up E.2.3. Could I be added to the CADP mailing-list?

[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.


Up E.2.6. How can I obtain CLEOPATRE or XESAR?

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 Jean-Luc.Richier@imag.fr. 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.


Up E.2.7. How can I connect CADP to the Concurrency Workbench?

[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.

        bcg_io your_filename.bcg your_filename.cwb

or:

        bcg_io your_filename.aut your_filename.cwb


Up E.2.8. How can I get the Fc2Tools?

[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


Up E.2.9. How can I use the Fc2Tools to minimise a .bcg or a .aut file?

[Thu Nov 6 09:52:14 MET 1997]


Up E.2.10. How can I use the Fc2Tools to compare two LTS files (in formats .aut or .bcg)?

[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.


Up E.2.11. How can I visualize a .bcg or a .aut file using Autograph?

[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.


Up E.2.12. Can I use the Fc2tools to verify a .exp file?

[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.


Up E.2.13. What's a deadlock state?

A deadlock state has no successors. This can be checked with the bcg_user.h API.


Up E.2.14. What's the VLTS benchmark suite?

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/.


Up E.2.15. In VLTS, is it the case that systems with deadlocked states are faulty systems and that deadlocked states were undesirable?

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.


Up 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?

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.


Up E.2.16. Is it possible to use Discrete-Time Markov Chains (DTMCs) or Continuous-Time Markov Chains (CTMCs) as specification formalism for CADP?

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.


Version 1.227 - Date 2024/01/13 10:02:39
Back to the CADP Home Page