Part III
Systems with
Complex State
10 Modeling Systems
with Structured
State
In the previous chapters we saw model programs that could be exhaustively explored
into their corresponding finite state machines. In this chapter, we will show how the
concept of a model program can cover larger, even infinite, numbers of states and
transitions.
10.1 ???Infinite??? model programs
To understand this we can introduce data types like integers and strings to our model
program. Unlike the data types we have considered up to this point, numbers and
strings are drawn from very large, or even infinite, domains.
Here is an example of a model program that has a number of states bounded only
by the size of the integer data type:
namespace Counter1
{
static class Contract
{
static int counter = 0;
[Action]
static void Increment() { counter = counter + 1; }
[Action]
static void Decrement() { counter = counter - 1; }
}
}
What??™s interesing here is that even with just two actions and no parameters, the
number of states may grow without limit, or at least without a computationally
feasible limit.
155
156 Modeling Systems with Structured State
This kind of model program is finitely branching. In other words, there are only
a finite number of transitions available in each state. As the example shows, even a
finitely branching model may have a computationally infeasible number of states.
Pages:
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221