5) or interactive exploration (Chapter 6, Section 6.2.3), but
may be easier to set up and repeat.
To make this easy to understand, we return to the simple news reader example. Let
us see what happens when the contract model program cannot execute the scenario.
We choose the run that we simulated in Chapter 5:
ShowTitles(); SortByFirst(); SortByFirst(); ShowText();
We encode this run as a scenario in an FSM text file with these contents:
FSM(0, AcceptingStates(), Transitions(
t(0,ShowTitles(),1), t(1,SortByFirst(),2), t(2,SortByFirst(),3),
t(3,ShowText(),4)),
Vocabulary("ShowTitles","ShowText","SelectMessages","SelectTopics",
"SortByFirst","SortByMostRecent"))
This FSM text file contains an entry at the end that defines the vocabulary of the
scenario machine, the names of all its actions. If this entry is omitted, the vocabulary
is understood to be the actions that appear in the transitions. Here we need to list the
vocabulary because it includes actions that do not appear in any of the transitions
of this particular scenario. When we use composition to check whether the contract
model program can execute a particular run, we must include the whole vocabulary
of the contract model program in the scenario model program. In the product, any
actions of the contract model program that do not appear in the scenario vocabulary
Systems with Finite Models 133
0
1
ShowTitles()
2
SortByFirst()
3
SortByFirst()
4
ShowText()
Figure 7.
Pages:
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197