Before you can calculate a state space, you must enter the state space tool. If the state space is expected to be small, you can simply apply the Calculate state spaceCalculate state space tool to a sheet containing a page from the net. If the state space is expected to be large, you may need to change the options for the Calculate state space tool. […]
Attributes and options in state space tool
Setting report options The content of a state space report is set by changing the options for the Save state space report tool. To change the textual format of place and transition names, see “Setting string representation options” below. Setting string representation options The string representation options allow the user to specify how the st-functions (which are fully described in the state space tool manual) […]
Draw state spaces with CPN Tools
Several tools from the state space tools can be used to draw parts of a state space. State spaces can only be drawn after entering the state space tool and calculating the state space. Display state space node To display a particular state space node, apply the Display State Space Node tool to a page. An option for the tool determines which node will be […]
Draw State Spaces with Graphviz
Beside drawing state spaces in CPN Tools, it is possible to export state space graph and SCC graph structure from CPN Tools to Graphviz. Graphviz is open source graph drawing software developed at AT&T Research Labs. With functions that are described below, the graph structure of (partial) state spaces and SCC graphs can be exported to files that can be then used as input files […]
Enter the state space tool
In older versions of CPN Tools, before a state space can be calculated and analyzed, it is necessary to generate the state space code, i.e., the ML code which is used to calculate and analyze state spaces. This code is generated when you enter the state space tool. Note in in more recent versions of CPN Tools, like in version 4.0.1) the tool enters the […]
Make state space queries
Queries are used to investigate the properties of a CPN. It is, e.g., possible to investigate the reachability, boundedness, home, liveness, and fairness properties using standard queries; and non-standard queries can be created by writing CPN ML functions. Queries are made by creating auxiliary text containing the query function, and then using the Evaluate ML tool to evaluate the text. The query functions that are […]
Nondeterministic nets
A net is nondeterministic if the occurrence of an enabled transition can lead to a marking that cannot be uniquely determined by the binding of the transition’s variables. The following are examples of constructions that often cause nondeterministic behavior in a net: Random distribution functions are used to generate time delays or parts of token values. The ran color set function is used to generate […]
Saving a standard state space report
After you have calculated a state space, and optionally the SCC graph, it is possible to save a standard state space report with the calculations. To save a report, apply the Save state space report tool to a sheet containing a page from the net. A save dialog box will appear. Specify the location and name of the report file you want to create. The […]
State space functions
The manual for the state space tool describes the majority of the functions that can be used to calculate and examine state spaces. This page provides an overview of functions that are not necessarily included in the manual. Node descriptors A node descriptor is a string representation of a node in a state space. (Nodes are defined in the manual.) By default, a node descriptor […]
Limitations
Errors can occur if any of the state space tools are applied while portions of a net are being syntax checked. It is highly recommended that you do not apply state space tools while there are any yellow highlights on places, arcs, transitions, pages, or net names. If the Replace by subpage tool is applied and the corresponding subpage(s) contains state space nodes and/or state […]
