CAESAR.BDD manual page

Table of Contents## Name

caesar.bdd - structural and behavioural analysis of Nested-Unit Petri
Nets
## Synopsis

**caesar.bdd** *option* [ *filename***.nupn** ]
## Description

Taking as input
*filename***.nupn** (or by default the standard input), which contains a Nested-Unit
Petri Net (NUPN) encoded in the **nupn**
format, **caesar.bdd** performs
various structural or behavioural analyses, depending on the *option* specified
on the command-line, and writes the corresponding results to the standard
output. Error messages, if any, are displayed on the standard error.
## Options

## NUPN (Nested-Unit Petri Net) Format

See the **nupn**
manual page for a detailed definition of the NUPN file format.
## Interrupts

**caesar.bdd**
handles certain POSIX interrupt signals (namely, SIGINT, SIGQUIT, SIGALRM,
and SIGTERM) and adapt its behaviour in consequence. Upon reception of
such a signal:
## User-specified Timeouts

The environment
variable *N*, the exploration of the marking graph will stop after *N* seconds.
If this variable is not set or set to zero, no timeout will occur. Upon
expiration of a timeout:
## Exit
Status

The exit status of **caesar.bdd** may take the following values:

## Authors

Damien Bergamini and Hubert Garavel (INRIA Rhone-Alpes)
## Files

## Credits

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

[Gar15] Hubert
Garavel. "Nested-Unit Petri Nets: A Structural Means to Increase Efficiency
and Scalability of Verification on Elementary Nets." In R. Devillers and
A. Valmari, editors, Proceedings of the 36th International Conference on
Application and Theory of Petri Nets and Concurrency (PETRI NETS'15), Brussels,
Belgium. Lecture Notes in Computer Science, vol. 9115, Springer, 2015. Related
slideshow available from http://cadp.inria.fr/publications/Garavel-15-a.html
## See Also

**caesar**
, **nupn**
, **nupn_info**
## Bugs

Please report new bugs to Hubert.Garavel@inria.fr

**-check**- Perform syntactic, structural and behavioural analysis of the Nested-Unit
Petri Net to verify whether the stated constraints of the NUPN format are
satisfied. The
**-check**option performs additional checks and warns about redundant or void units, places that are never marked, and transitions that may never fire, etc.; these checks rely upon sufficient conditions, so that there is no guarantee that all never-marked places and never-fired transitions are reported. In addition to these static checks, the**-check**option also explores the marking graph using BDDs (Binary Decision Diagrams), prints the number of states reached at each iteration, and checks whether all reachable markings are one safe and unit safe; such checks are inconclusive if the marking graph is too large for being generated. - Important:
- For performance
reasons, the other options of
**caesar.bdd**assume that the contents of*filename***.nupn**are correct; these options often perform less stringent verifications than**-check**, or even no verification at all. In particular, options**-dead-transitions**,**-concurrent-units**, and**-exclusive-places**do not perform dynamic checks but rely on an optimized encoding of markings: such options may produce invalid results if some markings are not one safe or not unit safe. When dealing with an unknown Nested-Unit Petri Net, it is therefore advisable to first analyze its contents with**-check**before using any other option than**-check**. **-arcs**- Display the number of arcs in the Nested-Unit Petri Net.
**-bits**- Display the number of bits needed to encode (using the best encoding) the markings of the Nested-Unit Petri Net.
**-concurrent-units (formerly -unit)**- Explore the
set of reachable markings and determine the pairs of "concurrent" units,
i.e., pairs of units Ui and Uj that satisfy the predicate Disjoint (Ui,
Uj) specified in the
**nupn**format definition, and such that there exists at least one reachable marking containing one place of Ui and one place of Uj. The output is defined as follows: Let U be the number of units in the Nested-Unit 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. The upper half of the matrix is not output because it is symmetric. **-creator**- Display the name of the creator tool specified by the
`!creator`

pragma if it is present in the Nested-Unit Petri Net, or the empty string if this pragma is absent. This pragma is specified in the "PRAGMA CREATOR" section of the**nupn**format definition. **-dead-transitions (formerly -dead)**- Explore (parts of) the set of reachable markings to 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 Nested-Unit 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. **-density**- Display the density of the incidence matrice of the the Nested-Unit Petri Net, i.e., the number of arcs divided by twice the product of the number of places by the number of transitions.
**-encodings**- Display statistics about the number of bits required to represent the markings of the Nested-Unit Petri Net using various possible encodings.
**-exclusive-places**- Explore the set of reachable
markings to determine the pairs of "exclusive" places, i.e., pairs of places
Pi and Pj such that Pi = Pj or there exists no reachable marking containing
both Pi and Pj. The exploration of the set of reachable markings may be
incomplete if a timeout (see below) is specified. The NUPN is said to be
"presumably unit safe" if either the exploration was complete and the NUPN
was found to be unit safe, or the exploration was incomplete and the NUPN
contains the "
`!unit_safe`

" pragma. The output is defined as follows: Let P be the number of places in the Nested-Unit Petri Net;**caesar.bdd**writes to the standard output a list of P*(P+1)/2 values corresponding to the lower half of a matrix indexed according to increasing place numbers; line i corresponds to place Pi (belonging to unit Ui) and raw j corresponds to place Pj (belonging to unit Uj); the value written at the intersection of raw i and column j is a character equal to:

- "`=`

": if Pi = Pj (diagonal elements), or if the NUPN is presumably unit safe and both places belong to the same unit, i.e., Ui = Uj;

- "`<`

": if the NUPN is presumably unit safe and the unit of Pi is contained in the unit of Pj, i.e., Sub* (Ui, Uj), where the Sub* predicate is specified in the**nupn**format definition;

- "`>`

": if the NUPN is presumably unit safe and the unit of Pi contains the unit of Pj, i.e., Sub* (Uj, Ui);

- "`~`

": if the NUPN is not presumably unit safe and both places are different and belong to the same unit, i.e., (Pi != Pj) and (Ui = Uj);

- "`[`

": if the NUPN is not presumably unit safe and the unit of Pi is contained in the unit of Pj, i.e., Sub* (Ui, Uj);

- "`]`

": if the NUPN is not presumably unit safe and the unit of Pi contains the unit of Pj, i.e., Sub* (Uj, Ui);

- "`0`

": if none of the above applies, and a marking containing both Pi and Pj was reached;

- "`1`

": if none of the above applies, and the exploration was complete and no marking containing both Pi and Pj was reached;

- "`.`

": if none of the above applies, and the exploration was incomplete and no marking containing both Pi and Pj was reached.

In summary, two places are exclusive if their matrix cell is "`=`

", "`<`

", "`>`

", or "`1`

"; they are non-exclusive if their matrix cell is "`0`

"; the answer is unknown if their matrix cell is "`~`

", "`[`

", "`]`

", or "`.`

". The upper half of the matrix is not output because it is symmetric, modulo permutations of "`<`

" and "`>`

", and of "`[`

" and "`]`

". **-height**- Display the height of the unit tree of the Nested-Unit Petri Net. All leaf units have height one, and the root unit only increases the height if this unit is not void (i.e., has at least one local place).
**-hwb**- Display the HWB code of the Nested-Unit Petri Net. This
code has the form
*height*-*width*-*bits*, where the three fields are those numbers computed by options**-height**,**-width**, and**-bits**, respectively. Fields*height*and*width*are omitted if*width*is equal to the number of places, i.e., if the NUPN is trivial. **-initial-places**- Display the list of places present in the initial marking. These places are displayed on a single line, separated with spaces.
**-initial-tokens**- Display the number of tokens present in the initial
marking. If present in the Nested-Unit Petri Net, the
`!multiple_initial_tokens`

pragma is taken into account. This pragma is defined in the "PRAGMA MULTIPLE_INITIAL_TOKENS" section of the**nupn**format definition. **-leaf-units**- Display the numbers of all leaf units (i.e., units that have no sub-unit) in the Nested-Unit Petri Net.
**-max-place**- Display the highest place number in the Nested-Unit Petri Net.
**-max-transition**- Display the highest transition number in the Nested-Unit Petri Net; if there is no transition, this number is equal to zero.
**-max-unit**- Display the highest unit number in the Nested-Unit Petri Net.
**-mcc**- Undocumented option
used to prepare or complete the model forms of the Model Checking Contest.
This option computes various structural and behavioural properties of the
Nested-Unit Petri Net. The
`unit_safe`

pragma, if present, is taken into account. If the`!multiple_arcs`

pragma or the`!multiple_initial_tokens`

pragma is present in the Nested-Unit Petri Net, the**-mcc**option computes structural and behavioural properties for the original (non safe) Petri Net rather than for the NUPN itself. **-min-place**- Display the lowest place number in the Nested-Unit Petri Net.
**-min-transition**- Display the lowest transition number in the Nested-Unit Petri Net; if there is no transition, this number is equal to one.
**-min-unit**- Display the lowest unit number in the Nested-Unit Petri Net.
**-multiple-arcs**- Display the arguments of the
`!multiple_arcs`

pragma if it is present in the Nested-Unit Petri Net, or the empty string if this pragma is absent. This pragma is specified in the "PRAGMA MULTIPLE_ARCS" section of the**nupn**format definition. **-multiple-initial-tokens**- Display
the arguments of the
`!multiple_initial_tokens`

pragma if it is present in the Nested-Unit Petri Net, or the empty string if this pragma is absent. This pragma is specified in the "PRAGMA MULTIPLE_INITIAL_TOKENS" section of the**nupn**format definition. **-places**- Display the number of places in the Nested-Unit Petri Net.
**-pnml**- Write to the standard output the translation
in PNML (Petri Net Markup Language) the network given as input in the NUPN
format. The PNML output will contain a "NUPN-toolspecific" section as defined
on the http://mcc.lip6.fr/nupn.php
page. If the input network contains errors,
the translation may stop prematurely, leaving an incomplete PNML file.
It is therefore recommended to invoke the tool as follows:

**caesar.bdd -pnml**[*filename***.nupn**] >*filename***.pnml**|| rm -f*filename***.pnml** **-redundant-units**- Display the numbers of all redundant units (i.e., units that have a single sub-unit) or the empty string if there are no such units in the Nested-Unit Petri Net.
**-root-unit**- Display the number of the root unit of the Nested-Unit Petri Net.
**-transitions**- Display the number of transitions in the Nested-Unit Petri Net.
**-trivial**- Display "1" if the Nested-Unit Petri Net is trivial, or "0" otherwise.
**-units**- Display the number of units in the Nested-Unit Petri Net.
**-version**- Display the current version number of the software.
**-void-nonroot-units**- Display the numbers of all void units (i.e., units having no local place) that are different from the root unit or the empty string if there are no such units in the Nested-Unit Petri Net. If the net is correct, the empty string should be displayed.
**-void-root-unit**- Display the number of the root unit if this unit is void (i.e., has no local place) or the empty string otherwise.
**-void-units**- Display the numbers of all void units (i.e., units having no local place, possibly including the root unit) or the empty string if there are no such units in the Nested-Unit Petri Net.
**-width**- Display the width of the unit tree of the Nested-Unit Petri Net. This width is equal to the number of leaf units.

- The execution of options
**-dead-transitions**and**-concurrent-units**terminates immediately, returning the exit code 5 (see below). - The execution
of options
**-check**,**-exclusive-places**, and**-mcc**stops the BDD-based exploration of reachable markings, and completes using pessimistic assumptions (i.e., the fact that parts of the marking graph have not been explored) delivering less precise, yet correct results.

`$CAESAR_BDD_TIMEOUT`

can be used to specify a maximal duration
for marking graph exploration. If this variable is set to a strictly positive
integer - The execution of options
**-check**,**-dead-transitions**, and**-concurrent-units**terminates immediately, returning the exit code 5 (see below). - The execution of option
**-exclusive-places**stops the BDD-based exploration of reachable markings, and completes using pessimistic assumptions. - The
execution of option
**-mcc**completes by computing behavioural properties using faster algorithms that rely on pessimistic assumptions.

The functionality provided by this environment variable is not available on Windows.

- 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***.nupn**does not exist or is unreadable

- 4:
- syntax or semantic error in
*filename***.nupn**

- 5:
**caesar.bdd**terminated by the user (SIGINT or SIGQUIT) or upon timeout (SIGALRM or SIGTERM)

Any other value corresponds to an unexpected error.

*filename***.nupn**- Nested-Unit Petri Net (input)
*filename***.places**- Table of place names (input,
**-mcc**option only) *filename***.trans**- Table of transition names (input,
**-mcc**option only)

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

Directives
for installation are given in files **$CADP/INSTALLATION_*.**

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