next up previous
Next: Putting Everything So Far Up: No Title Previous: Actions that Terminate Exceptionally

Nondeterminism

 

So far, tex2html_wrap_inline551 has been a function, that is, for each state, s, and action, a, tex2html_wrap_inline551 mapped us to at most one next state. Suppose I have a RandomCounter machine with an inc action that takes an integer argument:

tex2html_wrap759

Here is the specification of inc:

1

 inc(i: int)pre i > 0


           		post  tex2html_wrap_inline749

According to the specification, inc can either increment the counter's value by the value of its argument i or by twice that value. Thus, there are two possible states that you might end up in after doing the inc action given some integer argument. Since there is more than one, tex2html_wrap_inline551 needs to map to a set of statesgif:

tex2html_wrap_inline757

As an observer, you don't know which state transition will occur when you feed inc the integer 4. You must be prepared to deal with either possibility. The choice of which post-state is taken is made by the machine itself. Notice that the nondeterminism shows up in the specification of inc in the use of logical disjunction in the post-condition.


Norman Papernick
Mon Mar 18 15:31:49 EST 1996