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