16.2 Nondeterminism
Nondeterminism means here that there may be multiple possible observable actions
enabled in a given model program state. Although the main emphasis of this chapter
is on reactive systems, nondeterministic behavior arises also because of reasons
other than reactive behavior.
A common reason for nondeterminism is that the model program is written at a
much higher abstraction level than the system that is being modeled. This typically
means that there may be many possible IUT states corresponding to a single model
program state and therefore the exact behavior of the IUT is not known in a given
model program state. Usually the model program needs to be more abstract because
it is a contract and there may be multiple possible implementations that conform to
that contract.
The implementation that is being modeled may also exhibit random behavior. This
will also cause nondeterminism in the model program. The difference compared to
nondeterminism due to abstraction is that the model program may be more or less
at the same abstraction level as the IUT.
In general, reactive behavior leads to spontaneous reactions from the IUT that
need to be queued as observable actions by the conformance tester. This leads
to asynchronous stepping that is the topic of Section 16.3. There is an important
special case of nondeterminism, discussed next, that does not require asynchronous
262 Reactive Systems
namespace BagModel
{
[Feature]
static class Draw
{
static Bag
B { get { return Contract.
Pages:
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345