10.5 Exercises
1. In what ways is a .NET array different from a Sequence?
182 Modeling Systems with Structured State
2. An object graph is a directed, possibly cyclic, graph that arises from relations
among values. For example, the instance fields of objects in an object-oriented
program represent an object graph. How can a cyclic object graph be represented
using the data types described in this chapter?
3. Extend the repository control system to account for forking. Forking divides the
source files of the repository into independently updated branches.
11 Analyzing Systems
with Complex State
In Chapter 6 we saw how a technique known as exploration can enumerate the
possible states and transitions of a finite model program. We saw how exploration
can ???unwind??? a model program into its corresponding finite state machine. We
showed how the finite state machine could be used for safety and liveness analysis,
as well as for generating test cases that cover all model behaviors.
In Chapter 7 we showed techniques that limit exploration to scenarios of interest.
This allowed us to choose behavioral aspects to explore, instead of always
considering the full space of possibilities.
In this chapter we show how these ideas apply to model programs that have
larger, even unbounded, numbers of states and transitions. We will also introduce
some additional techniques for handling large search spaces.
Pages:
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251