The Message event has a Domain attribute for the Messages method that returns
the set containing the two message values, InRange and OutOfRange. This ensures
that the buffer and previous data state variables can have only those two values.
The four helper methods PollSensor, ResetSensor, StartTimer, and CancelTimer
are called by the handlers. They model commands to the sensor and timer by
assigning MessageRequested and TimeoutRequested.
5.8 Other languages and tools
The concepts taught in this chapter are common to many model-based testing and
analysis systems, not just the library and tools we use. Models store state and execute
Systems with Finite Models 93
actions. Models are made simple by slicing and abstraction, and are often finitized
before analysis. Models are written by coding action methods with enabling conditions.
But other systems often use different vocabulary for the concepts. For example,
an action method might be called an update rule, an enabling condition is a guard or
precondition, the combination of an action method with its enabling conditions is a
guarded update rule, and a model program written in this style is a guarded update
program. Other systems also use different programming languages (or different
coding conventions in the same language) for writing the model programs.
5.9 Exercises
1. Write a simple implementation of the newsreader model program of Section 5.
Pages:
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141