Introduction

The flow analysis which generates invariants is a suitable tool for verifying safeness properties is a suitable tool for verifying the liveness properties. In order to give a quick overview of these tools, we study one simple example. Coloured invariants have been implemented for a subclass of AMI-Nets that verifies the following properties:

• Color domains are products of classes.
• Color functions are linear combinations of basic functions tuples :
  • Identity : X,
  • Successor : X++k (or Predecessor X- -k),
  • Diffusion : C.all ( all the elements of the class C),
  • Constant : C.k ( element k in class C).
• No guard is associated to transitions

This tool implements a modified version of the General Algorithm for coloured flow computation described in [Couvreur 90].

The Colored invariants menu

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

Display of Results

Let us consider the famous philosopher example (model below) and one of the computed place invariants. The invariant formula is provided in a result window and outlined in the model window. Please note that coefficients of the formula are colour functions instead of integers (like in P/T nets). In the invariant displayed below, the ponderation of any place is free variable having the color domain of the corresponding place (here, C).

A Coloured flow shown in the model window.

A result window provides the exact formula. When clicking on it, this resultg is copyed in the historic window for reuse in other documents.

The formula of the invariant outlined in the model window.