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 is a string representation of the entire marking of a CPN that corresponds to a particular Node in a state space. The following functions can be used to generate and manipulate node descriptors.

  • NodeDescriptor n Returns a string representation of the net marking corresponding to Node n
  • OGSet.NodeDescriptorOptions nodeToStrFun Changes the contents of node descriptors
  • NodeFilterGen() Returns template code for defining contents of node descriptors

Examples of use

Suppose that the state space tools have been used to calculate the full state space for the example net of the Resource allocation example.

The Evaluate ML tool can be used to generate a string representing the marking of the net that corresponds to Node 3 in the state space.

State space node descriptor

State space node descriptor

If the string is fairly long and therefore difficult to read, the ML print function can be used to print the string.

Print a node descriptor

Print a node descriptor

This node descriptor contains quite a lot of information: the first line shows the number of the node; each place instance is shown in the form <Page name>'<Place name> Instance, and the marking of every place is shown, even if the marking is empty. To make the node descriptor more compact, you can start by generating and saving template code for defining the contents of node descriptors.

Save template code generated by NodeFilterFun

Save template code generated by NodeFilterFun

Open the file containing the template code in a text editor (below, left). Edit the function as desired, for example, to remove the line with the number of the node, and remove newlines after the marking of each place (below, right)

Template code for changing contents of node descriptors

Template code for changing contents of node descriptors

After editing template code for changing contents of node descriptors

After editing template code for changing contents of node descriptors

Finally, string representation options can be changed for place instances (below, left), place markings (below, center), and node descriptors (below, right).

Changing string representations of state space elements

Changing string representations of state space elements

Printing the node descriptor for Node 3 will now result in a much more compact representation of the marking where place instances are shown by simple place names, empty markings are omitted, and the node number is also omitted.

More compact node descriptor

More compact node descriptor

Arc descriptors

An arc descriptor is a string representation of an arc in a state space. (Arcs are defined in the manual.) By default, an arc descriptor is a string representation showing the source and destination nodes of the arc together with the corresponding binding element. The following functions can be used to generate and manipulate arc descriptors.

  • ArcDescriptor a Returns a string representation of the information associated with Arc a
  • OGSet.ArcDescriptorOptions arcToStrFun Changes the contents of arc descriptors
  • ArcFilterGen() Returns template code for defining contents of arc descriptors

Examples of use

Suppose that the state space tools have been used to calculate the full state space for the example net of the Resource allocation example.

The Evaluate ML tool can be used to generate the arc descriptor for Arc number 5 in the state space.

Arc descriptor

Arc descriptor

This arc descriptor shows that Arc 5 is an arc from Node 3 to Node 6, and it corresponds to an occurrence of instance 1 of transition T2 on page Top where the variable x is bound to the value q.

Related pages

Verification, State space tool manual

Saving a standard state space report
Limitations

You must be logged in to post a comment.