This page explains how to use the ProdInCosyVerif services. These allow to generate the state space from Symmetric or P/T nets and to query it. It relies on:
- prod: a tool developed by the Helsinki University of Technology (Laboratory of Computer Science), see here for more information about prod,
- dot: a command extracted from Graphviz.
Prod has been integrated in essentially for teaching purpose.
The Services Menu
ProdInCosyVerif services are available under the “Behavioral Verification” menu and it proposes the elements presented in the image below.
The following services are available:
- Statistics on the State Space: this service shows data about the reachability graph, but it requires to be generated first (that may take a while, as for other services 😉 ,
- Evaluate Formula (CTL or reachability): this service allows to query Prod about the reachability graph of the corresponding Petri Net specification,
- Watch Reachability Graph: this service allows to gather an image of the reachability graph, it is not advised to use it if the corresponding reachability graph is larger than 100 nodes (it is then very long to compute),
- Display States: this service allows to display the state of a reachability graph, e.g. the current markings corresponding to this configuration,
- Show Deadlocks: this service shows the deadlocks in the reachability graph (e.g. states without successor),
- Find a Path: this service allows to find a path between two states denoted by their id,
- Clean Persistent Files: this service cleans persistent files, it is useful if the state space is quite large or when you perform a new computation from scratch.
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 shown below.
It returns some information concerning the size of the reachability graph.
Evaluate Formula (CTL or reachability)
In this service, prior to select the model it concerns, you must enter a formula to be evaluated in the window shown below.
A typical answer you get in the result window (this 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 Graphviz drawing tool). An example of such an image is shown below. The red node corresponds to the initial state and black ones to states without successors. Inside nodes you can find 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.
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 😉 ).
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.
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.