Discrete variable value changes

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:

discvar change state space

The states are labeled with the name of the current location of automaton lamp and the current value of variable count.