8.6 Exercises
1. Write a stepper for the three newsreader implementations you wrote for the
problems in Chapter 5. Generate a test suite from the newsreader model program
Systems with Finite Models 149
in Chapter 5, and execute it on all three implementations (the correct one and
the two defective ones).
2. Write another model program, implementation, and stepper for the newsreader,
where each action returns the value of the page state variable at the time the
action exits. Write the stepper to check the return values. Make versions of this
implementation with the same two defects as in Exercises 3 and 4 in Chapter 5.
Generate a test suite from the model program. Execute the test suite on all three
of these implementations. Are the defects revealed earlier in the execution of the
test suite?
3. Write another model program, implementation, and stepper for the newsreader,
where each action returns the value of all three state variables as C# out parameters
at the time the action exits. Write the stepper to check the out parameters.
Make versions of this implementation with the same two defects as in
Exercises 3 and 4 in Chapter 5. Generate a test suite from the model program.
Execute the test suite on all three of these implementations. Are the defects
revealed earlier in the execution of the test suite?
4. Generate a test suite from the revised version of the reactive system model
program (without unsafe states or dead states) that you wrote for Exercise 5 in
Chapter 5.
Pages:
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218