The state machine has a check function that can return all defects of the state machine - if there are any. It is recommended to use the check function in the development stage (in debug mode).

The check function traverses the entire state machine hierarchy (visiting all vertices) starting at the state machine's root and the continuing recursively into its children an so forth. It verifies each element corresponding to the specification's constraints. Checks are also applied for each transition.

Detailed information about the findings can be displayed via the logging system. The free function write_defects_to_log can be used for this purpose.