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