Contrast to specification.
deterministic. A reactive system where if an observable action happens in a certain
state, then the same observable action will happen again when the same state is
visited. This fact can be used by an adaptive strategy.
difference. A set that contains the elements of a set that are not found in a second
set. Or, the operation on two sets that returns their difference.
directed graph. A graph where each link has a direction. An FSM can be represented
by a directed graph where the nodes represent states and the links represent
transitions, and each link is directed from the current state to the next state.
disabled. Not enabled.
disjunction. An expression that contains the or operator, || in C#. Contrast to
conjunction.
distributed system. A system with more than one computer. A distributed system
is also a concurrent system.
domain. A set from which the values for a parameter of an action are drawn during
exploration. In order to be explorable, each parameter for every action in a model
program must have a finite domain.
dynamic function. A key/value relationship that evolves during the run of a system.
A dynamic function can be represented by a map.
edge. Link.
enabled. An action is enabled when it can occur, when it is allowed to be invoked,
when its enabling condition is true.
320 Glossary
enabling condition. A predicate associated with an action.
Pages:
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410