The state of a CPN is a marking of the net, i.e. a distribution of tokens on the places of the net. Each node in a state space represents a state/marking of the corresponding CPN. It is possible to transfer states between the simulator and the state space tool.

Nodes, i.e. states, in a state space are denoted by positive integers. By convention, 1 denotes the initial node of the state space, i.e. node 1 corresponds to the initial state of the corresponding CPN.

Transferring states from state space to simulator

To transfer a node from the state space tool to the simulator, apply the

State space to simulator

State space to simulator

State space to simulator tool to a page in a net.

The number in the State space to simulator tool in the state space tools is the number of the node in the state space that will be transferred from the state space tool to the simulator when the tool is applied.

A status bubble will indicate whether or not the state was transferred successfully.

To change the number of the node to be transferred, change the option for the State space to simulator tool.

Transferring states from simulator to state space

To transfer a state from the simulator to the state space tool, apply the

Simulator to state space

Simulator to state space

Simulator to state space tool to a sheet containing a page from the net. A status bubble will indicate whether or not the state was successfully transferred to the state space tool.

 Related pages

Verification, state space tools

Temporal logic for state spaces

You must be logged in to post a comment.