CUI LSV LIPN LIP6
MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Displayed
Oct 21, 2017
Prod in CosyVerif

Introduction

This page explains how to use the ProdInCosyVerif services. These allow to generate the state space from a Symmetric or P/T nets and to query it. It relies on:

Prod as been integrated in essentially for teaching purpose.

The Services Menu

ProdInCosyVerif services are available under the "Behavioral Verification" menu and proposes the elements presented in the image below (number in names are not significative, they just set up a "logical" order in the menu).

the menu

The following services are available:

The Services

Let us know detail the services.

Generate State Space

This command does not require any parameter. To launch it, you just have to select a model using the appropriate mechanism such as the Coloane selection window show below.

selection window

It returns some information concerning the size of the reachability graph is provided.

Evaluate Formula (CTL or reachability)

In this service, prior to select the model it concern, you must enter a formula to be evaluated in the window shown below.

formula window

A typical answer you get in the result window (tis formula was not verified on the model we selected) is shown below.

This service relies on the prod model checker developed
at the Helsinki University of technology  (laboratory of
computer  science,  http://www.tcs.hut.fi/Software/prod)

Integration in CosyVerif by F. Kordon (UPMC, 2013)

Prod binaries checked OK
Gph2dot checked OK
Evaluating the provided CTL formula
0 paths
Built set %1

To know more about the syntax of Prod, please refer to this memento.

Watch Reachability Graph

When the reachability graph is of reasonable size (up to 150 nodes), you can get a precomputed image from it (layout is computed by the GraphWiz drawing tool). An example of such an image is shown below. The red node corresponds to the initial state and black ones to state without successor. Inside nodes is the identifier that allows you to fetch the corresponding marking via the command "Display States". Name of the arcs are labeled by the fired transition. Arcs are coloured to disambiguate the relation between states in the reachability graph.

a
reachability graph

This service also outputs the GraphViz description (dot format). This allows to use it and generate other formats with the appropriate tool. A pdf image is also provided (no need to recompile it ;-).

Display States

To watch the marking associated to a state in the reachability graph, you just have to specify its id (the number allocated by prod). By definition, 0 is always the initial state of the system. Other states identifiers can be gathered via queries to prod.

If you specify more than one state to be displayed, please separate each number by a space.

Show Deadlocks

This command does not require any parameter.

Find a Path

You just specify, as for the "Display States" service, the starting state and the ending state by their identifier. You must specify only two states in the parameter window (separated by a space). Prod shows the path as shown below, from the initial one you specify (first value) to the ending one (last value). Arrows display the binding of involved transitions.

Built set %1

PATH
Node 0, belongs to strongly connected component %%0
  outside: 4<..>
  keys: 2<..>
  bags: 3<..>
Arrow 0: transition getKey1, precedence class 0
Node 1, belongs to strongly connected component %%0
  outside: 3<..>
  gotKey1: <..>
  keys: <..>
  bags: 3<..>

1 paths
Built set %2

Clean Persistent Files

This command does not require any parameter.