The effect of strengthening the precondition of Increment
is the same as the state filter we described in the previous section.
11.2.4 Scenarios and composition
We showed how to use model program composition as a means of scenario control in
Section 7.3. This technique works well for models that have complex state because
it is a very general way to control exploration that can finitize parameter domains
and strengthen preconditions.
For example, we could make the infinitely branching Counter model program
shown in Section 11.1 explorable using composition. To do this, we would create a
finite state machine with only one state and five self-looping transitions.
FSM(0, AcceptingStates(0),
Transitions(t(0, ModularIncrement(0), 0),
t(0, ModularIncrement(1), 0),
t(0, ModularIncrement(2), 0),
t(0, ModularIncrement(3), 0),
t(0, ModularIncrement(4), 0)))
If we compose this FSM with the Counter model program using the technique
described in Section 7.3.2, the result is a model program that is explorable. To do
this, we could put the FSM into a text file CounterArgs.txt and include it as an
argument to the mpv tool:
mpv /r:Counter.dll Counter.Factory.Create /fsm:CounterArgs.txt
Note that the FSM in this example had only one state. Its effect was the same as
the Domain attribute shown in Section 11.1.
In general, it is possible to consider scenarios provided by arbitrary model programs.
Pages:
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257