Discrete variables can only change value by explicitly assigning them a new value in the
do part of an edge. If an edge does not assign a value to a discrete variable, that variable keeps its current value. Consider the following CIF specification:
automaton lamp: event turn_on, turn_off; disc int count = 0; location off: initial; edge turn_on do count := count + 1 goto on; location on: edge turn_off goto off; end
This is the same
lamp automaton as used in the lesson on automata, but with a
count variable added. This variable is used to count the number of times that the lamp has been turned on. The edge for the
turn_on event increments the value of the variable by one, each time the lamp is turned on.
The edge for the
turn_off event does not assign a value to a variable, so variable
count keeps its value when the lamp is turned off.
The state space of this specification is:
The states are labeled with the name of the current location of automaton
lamp and the current value of variable