Basics of Contracts

A building block is encapsulated by a contract, that describes the order in which parameters or pins can enter or exit the block. To have a contract has various benefits:

  • With a contract, you can understand the coarse behavior of a block, without knowing its internal details.
  • The analyzer can check if a block is integrated correctly.
  • You can integrate blocks into your system that aren't even finished yet, and develop a system top-down.

The figure bellow shows the block Speech Buffer from the outside (external point-of-view) with its corresponding contract on the right hand-side. To open a block contract, you can choose action “Show Contract” from the corresponding block's context menu.

Intuitively, we first need to initialize the block via pin init. Thereafter, pin speak can be used. At last, we terminate the block via pin stop and receive a confirmation via pin stopped.

States and Transitions

A block contract is specified by a state machine, which consists of states and transitions. During its life cycle, a contract typically starts in the initial state, goes through some normal states before it terminates into one of its final states.

  • An initial state () is the first state of a block. It usually means that the block is switched off, meaning that its internal behavior is not doing anything. Each block contract must have exactly one initial state.

  • A normal state describes a certain phase in the building block, in which different things may happen. In all normal states, a building block is considered to be active. States with the same name are identical, so the same state may be shown several times within a diagram.

  • A final state () indicates that a block is switched off again, and this state therefore corresponds to the same state as the initial state. A block contract must have at least one final state.

As shown in the figure above, the contract of block Speech Buffered has five states:

  • an initial state
  • state active
  • state stopping
  • two final states

A transition connects a source state to a target state. It is labelled with the pins of a building block. This indicates

  • the incoming flow(s) that can be accepted by the building block.
  • the outgoing flow(s) that must be handled by its environment, i.e., its enclosing block.

The source and target state of a transition can be the same. This is called self-transition. In order to improve the readability of contracts, we include this type of transitions directly below the state name (see state active in the following figure).

Transition labels include a slash (/) to improve the readability of the transitions. We'll cover its exact definition later. For now, simply think of the slash of separating the first input pin from the first output pin.

The contract of block Speech Buffered has five transitions:

  • init/: Transition from the initial state to state active. This is the first transition and will activate block Speech Buffered.
  • speak/: Self-transition from and to state active. This indicates that the enclosing block can repeatedly give inputs via pin speak.
  • stop/: Transition from state active to state stopping. Notice that after an incoming flow via pin stop, the block will no longer receive an input via pin speak.
  • /stopped: Transition from state stopping to a final state. A confirmation that the block is terminated is given to the enclosing block.
  • stop/stopped: Transition from state active to a final state. The block receives a stop command from the environment and confirms the termination right away.

As described above there are two alternative terminations for block Speech Buffered:

  • Via transitions “stop/” and then “/stopped”. This is the case when termination takes time because some internal activities need to be executed before the block can terminate. Here, after receiving “stop” input, the block enters state “stopping” and some time later emits event via pin “stopped” and terminates.
  • Via transition “stop/stopped”. This is the case when termination can occur immediately.

Parameter Nodes and Pin Types

You may have noticed the different color of the pins on block Speech Buffered. These are also useful to understand the behavior of the block.

  • White-background input pin (e.g., pin init) is used to start the block. Hence, it is only used to label transitions from the initial state.
  • White-background output pin (e.g., pin stopped) is used to indicate the termination of the block. Therefore, it is only used to label transitions towards final states.
  • Black-background input (e.g., pin speak, stop) and output pins allow in general flows to enter and respective exit the block when the block is active.

Tabular Form

Within the tool, block contracts are written in a tabular form. Every row of the table describes a transition. The columns display the source state of the transition, the transition label (parameter nodes) and the target state of the transition. The tabular form of the contract of block Speech Buffer is depicted in the following figure.

Every row of the table above corresponds to exactly one transition in the contract diagram in the first figure on this page. For example, the first row of the table above corresponds to the initial transition in the contract diagram.