## Automata

CIF models consist of components. Each of the components represents the behavior of a part of the system. Components can be modeled as automata, which form the basis of CIF. The following CIF specification, or CIF model, shows a simple automaton:

    automaton lamp:
      event turn_on, turn_off;

      location on:
        initial;
        edge turn_off goto off;

      location off:
        edge turn_on goto on;
    end

The automaton is named `lamp`, and not surprisingly represents the (discrete) behavior of a lamp.

Automaton `lamp` declares two events, named `turn_on` and `turn_off`. Events model things that can happen in a system. They represent changes. For instance, the `turn_on` event indicates that the lamp is being turned on. It represents the change from the lamp being off to the lamp being on. The event declaration in the `lamp` automaton declares two events. The event declaration only indicates that these events exist, it does not yet indicate when they can happen, and what the result of them happening is.

All automata have one or more locations, which represent the mutually exclusive states of the automaton. The `lamp` automaton has two locations, named `on` and `off`. Automata have an active or current location. That is, for every automaton one of its location is the active location, and the automaton is said to be in that location. For instance, the `lamp` automaton is either in its `on` location, or in its `off` location.

Initially, the lamp is on, as indicated by the `initial` keyword in the `on` location. That is, the `on` location is the initial location of the `lamp` automaton. The initial location is the active location of the automaton, at the start of the system.

In each location, an automaton can have different behavior, specified using edges. An edge indicates how an automaton can change its state, by going from one location to another. Edges can be associated with events, that indicate what happened, and thus what caused the state change. In each location, only the behavior specified by its edges is possible, for that automaton. No other behavior is possible.

The `lamp` automaton has an edge with the `turn_off` event, in its `on` location, going to the `off` location. Whenever the lamp is on, the `lamp` automaton is in its `on` location. Whenever the lamp is turned off, the `turn_off` event happens. The edge with that event indicates what the result of that event is, for the `on` location. In this case the result is that the lamp will then be off, which is why the edge goes to the `off` location.

The `lamp` automaton can go from one location to another, as described by its edges. This is referred to as 'performing a transition', 'taking a transition', or 'taking an edge'. The `lamp` automaton can keep performing transitions. The lamp can be turned on, off, on again, off again, etc. This can go on forever.