These facilities make it possible to analyze state spaces by means of a CTL-like temporal logic. It is possible to formulate queries about states, but also queries about state changes (e.g., the occurrence of certain transitions). Strongly connected components are used to make the model checking more efficient.
A manual describing how to use the temporal logic facilities is available. Note that even though the manual is written for use with another tool, much of it is applicable to CPN Tools.
The manual describes how to install and load the facilities. These descriptions do not apply to CPN Tools. In version 1.2 (and after) of CPN Tools, it is no longer necessary to install the facilities, and the steps for loading the facilities are described below.
Loading the facilities
Before the temporal logic facilities can be used, some additional information must be loaded into the state space tool. To load the facilities you must:
- Enter the State Space Tool
- Calculating a State_Space (including the SCC graph)
- Evaluate the following ML code:
This net can be found in a subdir of cpntools called
Additional information about the facilities is available online: