Nondeterministic nets

A net is nondeterministic if the occurrence of an enabled transition can lead to a marking that cannot be uniquely determined by the binding of the transition's variables.

The following are examples of constructions that often cause nondeterministic behavior in a net:

• Random distribution functions are used to generate time delays or parts of token values.
• The ran color set function is used to generate time delays or parts of token values.
• A code segment or a function is used to remove a random element from a list on a place.

Non-deterministic nets are generally not well-suited for state space analysis.

Each time a state space is calculated, the state space tool uses different random numbers for various tasks, such as for generating a random variate from one of the Random distribution functions, or for picking an enabled transition from a set of enabled transitions. Using different random numbers will affect the way in which the state space is calculated. This in turn will have varying (and unpredictable) effects on the nondeterministic behavior in the net. As a result, for nondeterministic nets it is virtually impossible to generate the same state space twice. The reachable markings may be different in two different state spaces, and the size of the state spaces may also vary. Furthermore, a state space that is generated may appear to be inconsistent with behavior observed during a simulation.

In some nets it may be obvious for the user that there are only a limited number of possible outcomes where there is nondeterministic behavior in a net. For example:

• If a random element is to be chosen from a given list, then there are only a finite number of different choices that can be made.
• If the ran function is used to choose a random element from a small color set, then there are only a few values in the color set to choose from.
• If a random number is to be chosen from a relatively short interval using the Discrete function, then there are only few integers to choose from.

It is not, however, obvious to the state space tool that there are only a limited number of possible outcomes, nor is there any way to ensure that the state space tool considers every possibility. The best that the state space tool can do when calculating the successors of a given marking is evaluate Transition inscriptions for a given binding of the transition's variables and see what is returned. Since the result of evaluating a transition's inscriptions may not be uniquely determined by the given binding, it is not possible to deterministically calculate the state space.

In some cases it is possible to make a nondeterministic net deterministic in order to make it better suited for state space analysis. Some examples are shown below.

Suppose that a function is used to randomly determine which element should be removed from a list on a place. For example, in the following example the Discrete function is used to determine the index number of the element to be removed. This is an example of a nondeterministic net.

If you know that there is a relatively small upper limit on the length of the lists that can be found on the place, then it is possible to make the above nondeterministic net deterministic as follows. Rather than using a function to randomly pick an the index of the element from a list, a variable is used to indicate the index of the element that was to be returned. The variable is from a small color set, i.e. a color set with less than ca. 100 elements. This makes it possible for the state space tool to consider every option, because it can simply use brute force to try binding the variable idx to each of the known values in the color set. This net is deterministic.

Note that this solution cannot be used if you do not know the maximum length of the lists.

These examples can be downloaded:

• the non-deterministic removal of an element of a list
• the deterministic removal of an element of a list

Suppose that time delays and/or parts of token values should be generated randomly. If there are only a few possible time delays to choose from and/or there are only a few possible values to choose from for the token values, then it is often possible to make nondeterministic behavior deterministic.

Here is an example of a nondeterministic net in which the ran function is used to generate token values, and the Discrete function is used to generate time delays.

A state space for this net will always contain only four different nodes, but the markings that are represented in the state space can differ each time the state space is generated.

Since both the BOOL color set and the set of possible values that are returned by the delay function are small sets, it is again possible to replace the use of functions with variables, and thereby make the net deterministic. Here is an example of how this can be done:

The state space tool will always calculate the same state space for this net, and the state space contains 84 nodes.

These examples can be downloaded:

• the non-deterministic choice of token values and time delays
• the deterministic choice of token values and time delays

Verification