What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

---

Version 1.9 last updated on 2018/07/20 18:25:12

---

March 3, 2013. Warning: This Page was created in 2003 and is likely to be obsolete at present; it was only kept for backward compatibility.

1. Introduction

A patch is available here that allows support of the BCG format in the muCRL toolset (versions 2.9.4 and 2.10.1). Once installed, you can use the instantiator tool of muCRL to generate compact .bcg files instead of huge .aut files.

The patch uses the bcg_write API of CADP to build BCG files. This feature will be enabled only if you have CADP installed on the machine on which you compile the muCRL toolset. If CADP is not installed, the muCRL toolset will be kept unchanged.

This patch was developed by Frédéric Perret and Hubert Garavel (INRIA/VASY), and benefited from useful suggestions from Dr. Thomas Arts (Ericsson, Sweden).

2. Installation

We assume that muCRL is installed in the directory ~/muCRL. Just follow the instructions below.

1. To apply this patch, you must first replace a few muCRL source files with the ones given here.

• For muCRL 2.9.4

  1. Replace the existing file ~/muCRL/Makefile.in with the modified file Makefile.in
  2. Replace the existing file ~/muCRL/configure.in with the modified file configure.in
  3. Replace the existing file ~/muCRL/src/inst.c with the modified file inst.c

• For muCRL 2.10.1

  1. Replace the existing file ~/muCRL/Makefile.in with the modified file Makefile.in
  2. Replace the existing file ~/muCRL/configure.in with the modified file configure.in
  3. Replace the existing file ~/muCRL/src/instantiator.c with the modified file instantiator.c

Then, move to the ~/muCRL directory and execute the following commands:

2. ~/muCRL>make clean

   You should skip this step if muCRL had not been compiled before. If you are not sure, there is no risk to do it anyway.

3. ~/muCRL>autoconf

   This will parse the new configure.in file and build a new configure script.

4. ~/muCRL>./configure

   This will scan your system and parse Makefile.in to build a new Makefile. Please check that the following line appears in the ouput list:
   

   BCG library available? yes

   If the line above contains no instead of yes, there can be three possible explanations:

   • CADP is not installed on the system.
   • CADP is installed, but the environnement variable $CADP does not point to a valid directory ($CADP should point to the directory in which CADP is installed).
   • You used ./configure --disable-bcg

5. ~/muCRL>make install (or gmake install)

3. Usage

You can now use instantiator with option -bcg option to produce a BCG graph. By example:

~/work>instantiator -bcg foo.tbf

Please notice that, when the -bcg option is given:

• instantiator automatically sets the -i option that represents tau labels by the label string "i";

• the -monitor option of instantiator opens a new window for the BCG graphical monitor (see the bcg_write API) instead of writing lines of statistics to standard output.

---

Back to the CADP Home Page