Next: List of Well-formedness Checks, Up: Well-formedness [Contents][Index]
Well-formedness checks on the behavior part of a model come in a
number of categories:
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,
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.
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
onin the behavior, an action is an event that is emitted inside the imperative body of a trigger.