We use a better representation of behaviors that removes
the redundancy, representing a great many runs in a compact way: the FSM. Exploration
automatically generates an FSM from a model program.
94
Systems with Finite Models 95
Table 6.1. Newsreader scenario FSM: state transition table
Current state Action (invocation) Next state
Topics, WithText, ShowTitles() Topics, TitlesOnly,
ByMostRecent ByMostRecent
Topics, TitlesOnly, SortByFirst() Topics, TitlesOnly,
ByMostRecent ByFirst
Topics, TitlesOnly, SortByMostRecent() Topics, TitlesOnly,
ByFirst ByMostRecent
Topics, TitlesOnly, ShowText() Topics, WithText,
ByMostRecent ByMostRecent
To describe a run of a model program, we only need to show the actions (the
action method calls). More thorough analyses must use the states as well. When we
consider states and actions together, we find that an action often causes a change of
state: a state transition. FSMs are built up from state transitions, not just actions.
To completely describe each state transition, we must identify the current state before
the transition, the next state after the transition (also called the target state), and
the action. To completely describe each action, we must show the entire invocation
(the action name and all of its arguments) and the return value (if there is one).
An FSM is simply a finite collection of state transitions described in this way,
along with an identification of the initial state where every run begins, and optional
accepting states where runs are allowed to end (if no accepting states are identified,
runs may end in any state).
Pages:
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144