By limiting the state variables to the control state, we ensure that the model
program is finite. In fact, it is quite small. The state space of a program is the set of
all states that it can reach. Here we have only three state variables, each with only
two values, so at most there can only be 2 ?— 2 ?— 2 or eight states in this program??™s
state space. The implementation??™s state space is ???infinite,??? because it includes the
topics and messages, which include strings, a data type that has an ???infinite??? number
of values. Our choice of state variables has finitized the model program. This is an
example of data abstraction.
5.4 Coding the model program
Now that we have selected the actions and state variables, we can code the model
program (Figures 5.4 and 5.5). The modeling library and tools support programs
that are coded in a few particular styles. In order to work with the tools, a model
program must be coded in one of these styles. In this chapter we introduce the style
we use for most of the examples in this book. A complete reference for writing
model programs in this style appears in Appendix A. Other styles are introduced in
Chapter 7, Section 7.3.2.
Systems with Finite Models 65
using NModel;
using NModel.Attributes;
using NModel.Execution;
namespace NewsReader
{
static class NewsReaderUI
{
// Types for each state variable
enum Page { Topics, Messages };
enum Style { WithText, TitlesOnly };
enum Sort { ByFirst, ByMostRecent };
// State variables, initial state
static Page page = Page.
Pages:
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108