Verification

To verify a CPN you can use the state space tools, which are available as a palette.

Help topics for verification

• Attributes and options in state space tool
• Calculating the state space
• Draw state spaces with CPN Tools
• Draw State Spaces with Graphviz
• Enter the state space tool
• Limitations
• Make state space queries
• Nondeterministic nets
• Saving a standard state space report
• State space functions
• States and state space nodes
• Temporal logic for state spaces

• state space tool manual

Example nets

• Dining philosophers example
• Distributed database example
• Resource allocation example
• Simple protocol example

Time-consuming operations

Some operations in the state space tool can be quite time consuming, e.g. entering the state space tool or calculating a state space. During these operations, a light purple status bubble may appear in the index to indicate that a time-consuming operation is being executed.