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.

Making a standard query

Making a standard query

The query functions that are available are described in the state space tool manual.

Exceptions

The ExcAvlLookup exception will be raised, if you attempt to access a node that is not found in the state space that has been calculated.

For example, if you use the Evaluate ML tool to evaluate the expression DeadMarking(2) before applying the Calculate state space tool, then the ExcAvlLookup exception will be raised, since node number 2 cannot exist in a state space that has not yet been calculated.

An ExcAvlLookup exception is raised

An ExcAvlLookup exception is raised

Related pages

Verification, state space tool manual

Enter the state space tool
Nondeterministic nets

You must be logged in to post a comment.