From a DES Editor window, open the Tools menu and select
Verify DES Integrity or click on the Verify DES Integrity button
on the toolbar. This will verify
the DES is Consistent.
From a DES Editor window, open the Tools menu and select
Check Reachability or click on the Check Reachability button
on the toolbar. This will check that every
state is reachable from the initial state.
From a DES Editor window, open the Tools menu and select
Check Nonblocking or click on the Check Nonblocking button
on the toolbar. This will check that every
reachable state is coreachable (i.e. a path exists from the state to a marked state).