GreatSPNinCosiVerif

This page explains how to use the GreatSPNinCosiVerif services. These allow to compute some structural properties for P/T nets. It relies on GreatSPN: a tool developed by the university of Torino (Dipartimento Di Informatica). Please have a look here for more information about GreatSPN.

These services of GreatSPN have been integrated in to enable some structural analysis.

The Services Menu

GreatSPNinCosiVerif services are available under the “Structural Analysis” menu and proposes the elements presented in the image below.

The following services are available:

  • Place invariants: this service computes a minimal generative family of P-positive invariants of the model,
  • Transition invariants: this service computes a minimal generative family of T-positive invariants of the model,
  • Minimal Syphon: this service compute the minimal syphons of the model,
  • Minimal traps: this service computes the minimal traps of the model.

The Services

All services are operated similarly. You just need to select the one you want in the menu and then select the model you want to process. Then the result is displayed in the output text window as shown below (for P-invariants).