check_fsm - Checks the transition relation for totality.


check_fsm [-h] [-m | -o output-file]

Checks if the transition relation is total. If the transition relation is not total then a potential deadlock state is shown out.

Command options:

-m
Pipes the output generated by the command to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".
-o output-file
Writes the output generated by the command to the file output-file.
At the beginning reachable states are computed in order to guarantee that deadlock states are actually reachable.
Last updated on 2010/05/19 22h:26