## Controller annotations

Controller properties annotations add properties of a controller to a specification. For basic information on controller properties annotations, see the language tutorial. Here we discuss further details.

Controller properties annotations (`@@controller:properties`) can only be added to the specification itself, not to elements of the specification.

The annotation has the following constraints, in addition to the general constraints that apply to all annotations:

- A specification may have at most one controller properties annotation.

- It is allowed for the annotation to not have any arguments, but in that case the annotation can also just be removed.

- The annotation supports the following arguments, and no other arguments are allowed:

  - `boundedResponse`:

    Indicates whether the specification has bounded response.

    Must have a boolean literal value. A `true` value indicates the specification has bounded response, and a `false` value indicates it does not have bounded response. If this argument is present and its value is `true`, then the `uncontrollablesBound` and `controllablesBound` arguments must also be present. If the argument is not present, or its value is `false`, these other two arguments must not be present.

  - `uncontrollablesBound`:

    Indicates the bound on the number of iterations for the event loop for uncontrollable events, if the specification has bounded response.

    Must have a non-negative integer literal value. This argument may only be present if the `boundedResponse` argument is also present, and its value is `true`.

  - `controllablesBound`:

    Indicates the bound on the number of iterations for the event loop for controllable events, if the specification has bounded response.

    Must have a non-negative integer literal value. This argument may only be present if the `boundedResponse` argument is also present, and its value is `true`.

  - `confluence`:

    Indicates whether the specification has confluence.

    Must have a boolean literal value. A `true` value indicates the specification has confluence, and a `false` value indicates it may not have confluence.

  - `finiteResponse`:

    Indicates whether the specification has finite response.

    Must have a boolean literal value. A `true` value indicates the specification has finite response, and a `false` value indicates it may not have finite response.

  - `nonBlockingUnderControl`:

    Indicates whether the specification is non-blocking under control.

    Must have a boolean literal value. A `true` value indicates the specification is non-blocking under control, and a `false` value indicates it is not non-blocking under control.