Table 6.2 and Figure 6.2 show the state transition table and
the state transition diagram, respectively, for the true FSM of our newsreader model
program (Chapter 5, Figures 5.4 and 5.5). Notice that the states and transitions in
Figure 6.1 also appear in Figure 6.2 (the initial state is shaded in both diagrams).
Here in Table 6.2, we use a more compressed format than in Table 6.1. We merge
several transitions into each row by using X to indicate ???don??™t care??? values in the
current state (where any value of particular variable is handled the same way, or is
simply ignored) and a dash (??“) for ???don??™t change??? values in the next state (where
the value of a particular variable is the same as in the current state). It turns out that
here this compression results in just one row for each action. Notice that each row
in Table 6.1 is also represented (in compressed format) in Table 6.2.
98 Exploring and Analyzing Finite Model Programs
Table 6.2. Newsreader true FSM: state transition table
Current state Action Next state
Topics, X, X SelectMessages Messages, ??“, ??“
Messages, X, X SelectTopics Topics, ??“, ??“
Topics, WithText, X ShowTitles ??“, TitlesOnly, ??“
Topics, TitlesOnly, X ShowText ??“, WithText, ??“
Topics, TitlesOnly, ByMostRecent SortByFirst ??“, ??“, ByFirst
Topics, TitlesOnly, ByFirst SortByMostRecent ??“, ??“, ByMostRecent
X indicates ???don??™t care??? values in the current state, where any value will do
??“ indicates ???don??™t change??? values in the next state, where the value is the same as in the current state.
Pages:
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149