## Discrete variables

This lesson introduces discrete variables. Consider the following specification:

``````automaton counter:
event increment, decrement;

disc int count = 3;

location:
edge decrement when count > 0 do count := count - 1;
edge increment when count < 5 do count := count + 1;
end``````

The `counter` automaton can be used to count certain things. The `increment` and `decrement` events are used to change the count. The count itself is stored in a variable named `count`. CIF has several different types of variables. Here, we use a discrete variable, as indicated by the `disc` keyword. The variable has an `int` data type, meaning it can have integer numbers as its value. It is initialized to value `3`.

The automaton has two edges, one for the `increment` event, and one for the `decrement` event. The edge for the `decrement` event has a guard that indicates under which circumstances the event can take place. The condition is indicated using the `when` keyword. In this case, the guard ensures that the count can only be decremented if it is currently positive. The guard of the edge for the `increment` event indicates that the count can only be incremented as long as it is less than five. In general, a guard must hold in the source location of the edge, for the edge to be enabled, and a transition to be possible. If the guard is not specified, it defaults to `true`, which always holds and does not restrict the edge in any way.

Both edges also have updates, indicated using the `do` keyword. Updates can be used to specify the effect of the transition on variables. In this case, the updates assign a new value to the `count` variable that is one less or one more than the current value. That is the value of the `count` variable is decremented or incremented by one.

This specification represents a counter that can be repeatedly incremented and decremented by one, and ensures that the value of variable `count` is always at least zero and at most five.

The state space of the `counter` automaton is as follows: