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. Manual A manual describing how to use the temporal logic facilities is available. Note that even though […]
States and state space nodes
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 […]
