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.
lamp declares two events, named
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
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
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.
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
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.