When modeling a protocol, the messages are actions.
pruning. To limit exploration by systematically excluding some transitions. Examples
of pruning techniques include state filters, strengthening enabling conditions,
state groupings, and stopping rules. Pruning is a way to finitize. Contrast to
sampling.
pure. A statement or expression that has no side effects. An enabling condition or
any other predicate must be pure.
random. A simple strategy that randomly selects an enabled action to execute next.
reachable. Of a state, that it is visited by some possible run. A reachable state
might be visited during exploration. Of an object, that it occurs within a global state
variable, or occurs within an instance field of a reachable object. The keys of a field
map contain all reachable instances of its class.
reactive system. A system that responds to its environment. In a reactive system,
some of the actions are observable. Contrast to closed system.
reference equality. Where two variables are equal when occupy the same location
in memory. In C#, the default equality for objects. Contrast to structural equality.
restricted model. A scenario model program created by restricting a contract model
program, especially by limiting domains.
review. Inspection.
reward. A quantity that a strategy seeks to maximize, by choosing the best action
in each state.
run.
Pages:
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421