Introduction

Services in that section are computed using GreatSPN, a well known software package for the modeling, validation, and performance evaluation of distributed systems using Generalized Stochastic Petri Nets designed in the universities of Torino and Genova (Italy).

For the conputation of invariants on Colored Petri nets, it has been coupled with our Colored Petri net unfolder.

The P/T net invariants menu

When the Petri net you have designed is syntactically correct, you can reach the services (in red).

Display of results

All results in GreatSPN are displayed the same way. Objets in the input Petri net are outlined and a floating window allows you to go from one structural property to the other one.

Display of a P-invariant by GreatSPN in CPN-AMI.

For P-invariants and T-oinvariants, ponderations are shown as temporary labels. In the previous figure, the Invariant has to be read : 1*B + 1*C + 1*G + 1*F + 1*D = constant.

The floatting window to go from one result to another.

The Floatting window allows the user to go from one result to an other (for example, one P-invariant to another one). In the example above, there are three inviariants. The third one is currently outlined in the model window. No floatting widow appear if there are no result (for example, no P-invariant in the Petri net model).

Please note that if the computation is tool long, you can cancel the execution by clicking on the STOP button in the execution window.

Display of Results for Colored Nets

Results are displayed in the historic window. Let us have a look on the typical philosopher example (model below).

The philosopher model.

The computation of P-invariants provide the following result. Please note that name of original colored places is postfixed with the color unfolding to increase readability.

Computation of P-invariants on the philosopher model.