Implement verification for incorrect causalities.

[jrbeaumont]

For example, if an internal transition causes an input transition, this is erroneous.

Are there further checks of this style?

[snowleopard]

There may also be a report on timing assumptions and concurrency reductions that have been detected in the specification: an input causing another input is usually a timing assumption, and an output causing another output is called a concurrency reduction.