IsTrue(NewsReaderUI.ShowTitlesEnabled());
NewsReaderUI.ShowTitles();
Assert.IsTrue(NewsReaderUI.SortByFirstEnabled());
NewsReaderUI.SortByFirst();
Assert.IsTrue(NewsReaderUI.SortByMostRecentEnabled());
NewsReaderUI.SortByMostRecent();
Assert.IsTrue(NewsReaderUI.ShowTextEnabled());
NewsReaderUI.ShowText();
}
Figure 5.6. Simulation run of the newsreader model program coded as an NUnit test.
nondeterminism can execute many different runs, where actions occur in different
sequences. This is what we mean by environmental abstraction.
It is an error to invoke an action method in a state where any of its enabling
conditions is false. This error is handled (or prevented) differently by different tools.
During simulation (Section 5.5), the enabling condition acts as a run-time check:
if an action method is about to be invoked when its enabling condition is false,
the tool reports a failure. During exploration (Chapter 6), action methods whose
enabling conditions are false are simply not chosen for execution.
5.5 Simulation
Now that we have a model program, we can begin some model-based analysis. We
begin with simulation: run the model program and see what happens (we should have
some expectation of what should happen). Each run of the model program simulates
a run of the implementation. Simulation using model programs is sometimes called
animation.
It is possible to execute a model program without using any of the tools, by
writing an application or a test fixture that calls its methods.
Pages:
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115