Introduction

The aim of this tool is to compute a linear charaterization of the reachability set. Results are split up into invariants and properties. Invariants can be used for any initial marking, provided that the constant in the contraints are modified according to the new initial marking. On the other hand, properties are (usually) dependant of the initial marking.

The current version computes the convex envelop of the reachability set.

The Linear Characterization menu

When the Place/Transition net you have designed is syntactically correct, you can reach the service (in red).

Display of Results

Here is a small example of Prefix output. First, we consider this small example model below.

A small Petri net example.

The linear caracterization (quiet mode) of this model is displayed in the historic window, has shown below.

Linear characterization of the example.

The first three properties correspond to place invariuants. The fourth one expresses that place G is always marked when place D is not. The fifth one expresses a similar condition between F and G. Finally, the sixth one signals that places A and D can never be marked together. The "Exact caracetrization" sentence indicates that the computed invariants and properties exactly describe the reachability set.