Next: , Up: Well-formedness   [Contents][Index]

11.1 Well-formedness Checks Categories

Well-formedness checks on the behavior part of a model come in a number of categories:

Top level

Interface, event and component definitions.


triggers and actions are expected at different places depending on the direction of their event.


The imperative part of the language (assigns, actions, function calls) are only allowed in an imperative statement or in a function body,


The use of statements within compounds is restricted,


The usage of reply,

Valued Actions and Calls

The use of non-void actions and calls,


The use of injected ports,


A function body should be imperative, and have a well-defined return.

Data Parameters

The use of data parameters,


The use of injected ports,


All ports should be bound correctly.

Note: A trigger is an event that occurs and is prefixed by on in the behavior, an action is an event that is emitted inside the imperative body of a trigger.