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 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:

Category Annotation

Controller

controller:properties

Documentation

doc

State

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 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.

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.