 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| • |
An oracle indicates to the top-level simulator
|
|
|
function the id of the next instance to simulate
|
|
|
| • |
How
fine-grained should a simulation be?
|
|
|
|
– |
Transitions are considered atomic: the simulation might
|
|
|
miss
some possible real-life process interleaving scenarios
|
|
|
|
– |
Actions
are considered atomic: some
actions, such as
|
|
|
procedure calls, are more time consuming than simple actions,
|
|
|
such
as goto and nextstate
|
|
|
| • |
We
are implementing mechanisms to handle
|
|
|
both
cases, so that appropriate process
|
|
|
interleaving can be selected for each application
|