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
counter automaton can be used to count certain things. The
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
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: