Nondeterminism

 

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

Here is the specification of inc:

1

 inc(i: int)pre i > 0

           		post    

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, needs to map to a set of states:

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.