CAESAR.BDD manual page
Table of Contents

Name

caesar.bdd - structural analysis of Basic Petri Nets

Synopsis

caesar.bdd [-dead] [-unit] [-version] [ filename.bpn ]

Description

Taking as input filename.bpn (or by default the standard input), which contains a Basic Petri Net encoded in a textual format described below (see the INPUT FORMAT section), caesar.bdd performs various structural analyses, depending on the option specified on the command-line, and writes the results to the standard output.

Options

-dead
Explore the set of reachable markings and determine the set of "dead" transitions, i.e., transitions that are not enabled in any reachable marking. The output is defined as follows: Let T be the number of transitions in the Basic Petri Net; caesar.bdd writes to the standard output a list of T values corresponding to each transition and ordered according to increasing transition numbers; the value written for each transition is 1 if the transition is dead, and 0 otherwise.

-unit
Explore the set of reachable markings and determine the pairs of "concurrent" units, i.e., pairwise different units U1 and U2 such that there exists at least one reachable marking containing one place of U1 and one place of U2. The output is defined as follows: Let U be the number of units in the Basic Petri Net; caesar.bdd writes to the standard output a list of U*(U+1)/2 values corresponding to the lower half of a matrix indexed according to increasing unit numbers; the value written at the intersection of raw i and column j is equal to 1 if units Ui and Uj are concurrent, and 0 otherwise.

-version
Display the current version number of the software and stop.

Input Format

The format of filename.bpn is defined by the following BNF grammar ("nb" stands for "number"; for details about the notion of "unit", see the papers on CAESAR available from http://vasy.inria.fr/publications): 
<basic-petri-net> ::= 
   places #<nb-of-places> <min-place-nb>...<max-place-nb>\n
   initial place <place-nb>\n
   units #<nb-of-units> <min-unit-nb>...<max-unit-nb>\n
   root unit <unit-nb>\n
   <unit-description>*\n
   transitions #<nb-of-trans> <min-trans-nb>...<max-trans-nb>\n
   <trans-description>*\n
<unit-description> ::=
   U<unit-nb>
   #<nb-of-places> <min-place-nb>...<max-place-nb>
   #<nb-of-subunits> <subunit-list>\n
<trans-description> ::=
   T<transition-nb> 
   #<nb-of-input-places> <input-place-list>
   #<nb-of-output-places> <output-place-list>\n
<input-place-list> ::= <place-nb>*
<output-place-list> ::= <place-nb>*
<subunit-list> ::= <unit-nb>*
<nb-of-places>        ::= <unsigned-integer>
<min-place-nb>        ::= <unsigned-integer>
<max-place-nb>        ::= <unsigned-integer>
<place-nb>            ::= <unsigned-integer>
<nb-of-units>         ::= <unsigned-integer>
<min-unit-nb>         ::= <unsigned-integer>
<max-unit-nb>         ::= <unsigned-integer>
<unit-nb>             ::= <unsigned-integer>
<nb-of-trans>         ::= <unsigned-integer>
<min-trans-nb>        ::= <unsigned-integer>
<max-trans-nb>        ::= <unsigned-integer>
<nb-of-subunits>      ::= <unsigned-integer>
<transition-nb>       ::= <unsigned-integer>
<nb-of-input-places>  ::= <unsigned-integer>
<nb-of-output-places> ::= <unsigned-integer>

Outputs

As caesar.bdd executes, various messages are displayed on the standard error stream. These messages give statistics on the Petri net and associated BDDs, and explain the reason of errors, if any.

Exit Status

The exit status of caesar.bdd may take the following values:
0:
normal termination (everything is alright)

1:
memory shortage (Petri Net and/or BDDs are too large)

2:
incorrect command-line arguments for caesar.bdd

3:
filename.bpn does not exist or is unreadable

4:
syntax error in filename.bpn

5:
caesar.bdd terminated by the user (SIGINT signal)

(any other value correspond to an unexpected error).

Author

Damien Bergamini (INRIA Rhone-Alpes)

Files

filename.bpn
Basic Petri Net (input)

Credits

To perform its structural analyses, caesar.bdd uses the Binary Decision Diagram package CUDD (Release 2.4.0) developed by Fabio Somenzi at the University of Colorado (Boulder, CO, USA).

See Also

CAESAR Reference Manual, caesar

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in file $CADP/INSTALLATION.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Known bugs are described in the Reference Manual of CAESAR. Please report new bugs to Hubert.Garavel@inria.fr

Table of Contents