It can be helpful to view the result of exploration even when you do not have a
precise question formulated, because it might reveal that the model program does
not behave as you intend. For example, you may see many more or many fewer
states and transitions than you expected, or you may see dead ends or cycles you
did not expect.
Exploration can also answer precisely formulated questions. It can perform a
safety analysis that identifies unsafe (forbidden) states, or a liveness analysis that
identifies dead states from which goals cannot be reached. To prepare for safety
analysis, you must write a Boolean expression that is true only in the unsafe states.
Exploration will search for these unsafe states. To prepare for liveness analysis,
you must write a Boolean expression that is true only in accepting states where the
program is allowed to stop (i.e., where the program??™s goals have been achieved).
Exploration will search for dead states, from which the accepting states cannot be
reached. Dead states indicate deadlocks (where the program seems to stop running
3 Exploration is similar to another analysis technique called model checking.
Overview 7
and stops responding to events) or livelocks (where the program keeps running but
can??™t make progress). The mpv tool can highlight unsafe states or dead states.
There is an important distinction between finite model programs where every
state and transition can be explored, and the more usual ???infinite??? model programs
that define too many states and transitions to explore them all.
Pages:
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33