Probe can be used to manually explore the transitions of a process as a tree,
which can be very helpful when debugging a process definition. Probe can be
launched on any process by typing
:probe P into the
prompt. Alternatively, Probe may be launched
on any state via a node (such as those in the Debug Viewer or
Process Graph Viewer) by clicking the Probe button.
As an example of how to use Probe, consider loading Dining Philosophers
:probe SYSTEM into the prompt; this will result in the following
window being displayed:
In the above, the transitions of the initial state (i.e.
SYSTEM) are shown
in sorted order of event. A line of the form
ev: P means that the process
can perform the event
ev and evolve into the process
P. Further, each of
these lines can be expanded to reveal the transitions of the resulting process,
yielding a tree of transitions. To expand the transitions of a process either
double click on the row, click on the triangle to the left of the row, or use
the right arrow keyboard button. To contract a row, either double click on the
row, click on the triangle or use the left arrow keyboard button.
For example, if we expand the first and the second rows, we see the following view:
Probe also highlights syntactically equivalent nodes in red. For example, in the
above screenshot there are two rows highlighted as the state reached by
thinks.0 and then
thinks.1 is identical to the
state reached by performing the events in the opposite order.
The trace required to reach the currently selected node is displayed at the bottom of the window.