## Annotations

Annotations can be added to elements of a CIF specification, to annotate them with extra information. Annotations are a form of structured data, and the CIF type checker checks their validity. Tools that take CIF specifications as input can process the annotations that are attached to elements of the specification, and use the supplied information.

Annotations differ from comments. Comments can also be used to add additional information to a specification. However, comments are completely free form, as you can write anything in them. They can even be used to (temporarily) comment out some parts of the specification. Furthermore, comments are purely for the benefit of the modeler. They are never interpreted by a tool.

Annotations have two main purposes:

- Annotations allow for extensibility, as anyone can add annotations, whether it is general purpose, company-specific, or even for private use.

- Annotations allow to test out language extensions before fully integrating them into the language.

Annotations can be added to most elements of CIF specifications that have a name (like components and variables), or can have a name (like locations and invariants), as well as some other elements (like edges).

The following built-in annotations are bundled with CIF:

- `controller:properties`

- `doc`

- `partial`

- `state`

Annotations are an extension mechanism, and anyone can define and register their own annotations. Different CIF installations may therefore have different registered annotations. A CIF specification may thus have a warning in one installation, if the annotation is for instance not registered in that installation, while in another installation the annotation does not have a warning, as there it is registered. Different people could define the same annotation in different ways, such that their own installations interpret that annotation differently and impose different constraints for it. Hence, a specification with such annotations may be valid in one installation, and invalid in another.

For more detailed information on annotations, see the reference manual.

### Controller properties annotations

A controller properties annotation can be added to a CIF specification that represents a controller that satisfies certain properties. The annotation should not be manually added to specifications. Instead, it should be added by tools such as the CIF controller properties checker tool, once the tool has checked that the properties hold for the specification. For instance, such a tool may add the following to a CIF specification that has bounded response:

    @@controller:properties(boundedResponse: true, uncontrollablesBound: 2, controllablesBound: 5)

For more detailed information on controller properties annotations, see the reference manual.

### Documentation annotations

Documentation can be added to all elements of the specification that support annotations:

    @doc("The lower limit sensor of the elevator.")
    @doc("Safety sensor.")
    input bool ElevatorDownSensor;

The documentation may span multiple lines, by using explicit newline characters:

    @doc(
        "doc with multiple\n" +
        "lines of\n" +
        "text"
    )
    input bool i;

This also may be abbreviated as follows, by using multiple arguments:

    @doc(
        "doc with multiple",
        "lines of",
        "text",
    )
    input bool i;

It is also possible to use for instance constants from the model in the documentation text:

    const int MAX_NR_OF_PRODUCTS = 3;

    @doc(fmt("Sensor 1/%d.", MAX_NR_OF_PRODUCTS))
    input bool s1;

This documentation can then be used by CIF tools in various ways. For instance, if the the CIF code generator is used to generate Java code for the above example, then the documentation is included in the generated code:

    /**
     * Input variable "ElevatorDownSensor".
     *
     * <p>
     * The lower limit sensor of the elevator.
     * </p>
     *
     * <p>
     * Safety sensor.
     * </p>
     */
    public boolean ElevatorDownSensor;

For more detailed information on documentation annotations, see the reference manual.

### Partial specification annotations

CIF supports defining library models that can be imported by multiple different other models, to allow reuse and reduce duplication among models. For instance, consider the following CIF model that defines some events that are to be used in both a plant model a simulation model:

    controllable c_start;
    controllable c_stop;

A library model is typically not a complete specification, but rather only a partial specification. It contains the common parts, while other models that import the library model provide the differing parts.

The CIF type checker checks models for common problems, such as unused events. For partial specifications this may lead to false positives. For instance, in the model above, the `c_start` and `c_stop` events are not used in the library model itself. The plant and simulation model that import it likely do use the events, ensuring that the events are used in the full specification. Since the type checker does not know where a library will be imported, it may incorrectly warn about such unused events.

To indicate to the type checker that a model is a partial specification, you can add the `@@partial` annotation. This indicates to the type checker that it shouldn’t report warnings that are typically false positives in partial specifications, such as unused events:

    @@partial

    controllable c_start;
    controllable c_stop;

For more detailed information on partial specification annotations, see the reference manual.

### State annotations

A state annotation adds state information to a location in an automaton. States consist of the current locations of automata and the current values of variables. The typical use of state annotations is for generated models that contain an automaton representing a state space of another model, where each location of that automaton represents a state of the state space. For instance, the CIF explorer may generate CIF models with state spaces represented as automata. For the example from the lesson on synchronizing events, it may generate the following model:

    group producer:
      event produce;
      event provide;
    end

    group consumer:
      event consume;
    end

    automaton statespace:
      alphabet producer.produce, producer.provide, consumer.consume;

      @state(consumer: "idle", producer: "producing")
      location loc1:
        initial;
        edge producer.produce goto loc2;

      @state(consumer: "idle", producer: "idle")
      location loc2:
        edge producer.provide goto loc3;

      @state(consumer: "consuming", producer: "producing")
      location loc3:
        edge producer.produce goto loc4;
        edge consumer.consume goto loc1;

      @state(consumer: "consuming", producer: "idle")
      location loc4:
        edge consumer.consume goto loc2;
    end

This state space consists of four states, each represented by a location of the `statespace` automaton. For instance, the first state is represented by location `loc1`, which corresponds to the state where the `consumer` is `idle` and the `producer` is `producing`.

A location may have multiple state annotations in case it represents multiple states. For instance, the event-based DFA minimization tool may merge locations representing different states to a single location representing multiple states.

For more detailed information on state annotations, see the reference manual.