Automaton definition parameters

In the previous lesson, an automaton definition with parameter was used. The parameter was an algebraic parameter, which is only one of the different kinds of automaton definition parameters. This lesson explains each of them:

This lesson also explains how to use multiple parameters.

Algebraic parameters

An algebraic parameter is similar to an algebraic variable. Arbitrary values or expressions of matching type can be provided as arguments in automaton instantiations. For instance, consider the following partial CIF specification:

event int accept, provide;

automaton def Buffer(alg int capacity):
  disc list int buf = [];

  location:
    initial;
    edge accept?        when size(buf) < capacity do buf := buf + [?];
    edge provide!buf[0] when size(buf) > 0        do buf := buf[1:];
end

buffer1: Buffer(5);

Automaton definition Buffer has an algebraic parameter that indicates the capacity of the buffer. The buffer can accept something when it has not yet reached its capacity. It can provide something when the buffer is not empty. Automaton instantiation buffer1 has value 5 as its argument. Value 5 is an integer number, which matches the integer type (int) of the capacity parameter.

Algebraic parameters can be used inside an automaton definition, wherever a value is expected, e.g. in guards, updates, initial values of discrete variables, and invariants. The expression that is provided by the instantiation is essentially filled in wherever the parameter is used. The above is equivalent to:

event int accept, provide;

automaton buffer1:
  disc list int buf = [];

  location:
    initial;
    edge accept?        when size(buf) < 5 do buf := buf + [?];
    edge provide!buf[0] when size(buf) > 0 do buf := buf[1:];
end

Event parameters

Event parameters allow different instantiations to synchronize with different events or to communicate over different channels. For instance, consider the following partial CIF specification:

event int generate, pass_along, exit;

automaton def Buffer(event int accept, provide):
  disc int buffer;

  location accepting:
    initial;
    edge accept? do buffer := ? goto providing;

  location providing:
    edge provide!buffer goto accepting;
end

buffer1: Buffer(generate, pass_along);
buffer2: Buffer(pass_along, exit);

Automaton definition Buffer is parametrized with two channels, one to accept a product into the one place buffer, and one to provide it to some other part of the system. The first buffer (buffer1) accepts products via the generate channel, and provides products via the pass_along channel. The second buffer (buffer2) accepts products via the pass_along channel, and provides products via the exit channel. The first buffer uses the pass_along channel as its provide channel parameter, and the second buffer uses that same pass_along channel as its accept channel parameter. The first buffer thus provides its items to the second buffer.

Event and channel parameters can be used inside an automaton definition, wherever an event or channel is expected, e.g. on edges and in alphabets if explicitly specified. The event or channel that is provided by the instantiation is essentially filled in wherever the parameter is used. The above is equivalent to:

event int generate, pass_along, exit;

automaton buffer1:
  disc int buffer;

  location accepting:
    initial;
    edge generate? do buffer := ? goto providing;

  location providing:
    edge pass_along!buffer goto accepting;
end

automaton buffer2:
  disc int buffer;

  location accepting:
    initial;
    edge pass_along? do buffer := ? goto providing;

  location providing:
    edge exit!buffer goto accepting;
end

Channel parameter usage restrictions

If an event parameter is actually a channel (it has a data type), it may also be called a channel parameter. By default, a channel parameter can be used to send, receive, or synchronize. However, it is also possible to restrict the allowed usages. By putting certain event usage restriction flags after the name of the channel parameter, only those usages are allowed. The available flags are ! to allow sending, ? to allow receiving, and ~ to allow synchronizing. Duplicate flags are not allowed, the ! should be before the ? flag, and the ! and ? flags should be before the ~ flag.

By restricting the usages, you can immediately see how a channel parameter is used within the automaton definition, as only the usages indicated by the parameter are allowed. It serves as sort of documentation of the intention of the channel parameter. This is much simpler than finding the actual usages of the parameter in the automaton. However, note that the parameter indicates the allowed usages, and doesn’t guarantee that the event/parameter is actually used at all.

Another benefit of restricting the usages, is that it makes it possible to spot mistakes. You might for instance use a channel parameter on an edge (e.g. edge e), but forget to include the send part (e.g. edge e!1). If the parameter only allows sending, the accidental synchronization (edge e) is reported as an invalid use. Without the usage checking, you might not encounter the problem until for instance simulation, where it is much more difficult to find the cause.

For the example above, we have the following header of the Buffer definition:

automaton def Buffer(event int accept, provide):

We can change this as follows:

automaton def Buffer(event int accept?, provide!):

This makes it clearer that the accept channel is used to receive a product into the buffer, and the provide channel is used send a product from the buffer.

Location parameters

An earlier lesson explained how a location can be used as a variable. Using location parameters, automaton definitions can be supplied with different locations. For instance, consider the following CIF specification:

automaton def Machine(location other_processing):
  location heat_up:
    initial;
    edge when not other_processing goto processing;

  location processing:
    edge tau goto cool_down;

  location cool_down:
    edge tau goto heat_up;
end

machine1: Machine(machine2.processing);
machine2: Machine(machine1.processing);

Automaton definition Machine represents a machine that can heat up, process something, cool down, and repeat that forever. The system consists of two of those machines. The machines can not start processing if the other machine is already processing. That is, the machines perform mutually exclusive processing. If the first machine is in its processing location, the other can’t also be processing (in its own processing location). To prevent a machine from starting to process if the other machine is already processing, each machine needs to know whether the other is already processing. Therefore, automaton definition Machine is parametrized with a location parameter other_processing, that indicates whether the other machine is currently processing (in its processing location). This parameter is used as a guard that determines whether a transition from location heat_up to location processing is allowed. Automaton instantiation machine1 provides the first machine with the processing location of the second machine, by using machine2.processing as its instantiation argument.

Location parameters can be used inside an automaton definition, wherever a boolean value is expected, e.g. in guards. The location that is provided by the instantiation is essentially filled in wherever the parameter is used. The above is equivalent to:

automaton machine1:
  location heat_up:
    initial;
    edge when not machine2.processing goto processing;

  location processing:
    edge tau goto cool_down;

  location cool_down:
    edge tau goto heat_up;
end

automaton machine2:
  location heat_up:
    initial;
    edge when not machine1.processing goto processing;

  location processing:
    edge tau goto cool_down;

  location cool_down:
    edge tau goto heat_up;
end

Automaton parameters

When multiple declarations (variables, locations, etc) from one automaton are to be supplied as parameters to another automaton, it is also possible to supply the entire automaton as a parameter, but only if the provided automaton is an instantiation of an automaton definition. Consider for instance the following CIF specification:

automaton def Sensor():
  event go_on, go_off;

  location off:
    initial;
    edge go_on goto on;

  location on:
    edge go_off goto off;
end

sensor1: Sensor();
sensor2: Sensor();

automaton def Actuator(Sensor sensor):
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on  when sensor.on  goto on;

  location on:
    edge turn_off when sensor.off goto off;
end

actuator1: Actuator(sensor1);

Automaton definition Sensor models a sensor that can go on an off. Both sensor1 and sensor2 are actual sensors. Automaton definition Actuator models an actuator that can be turned on if a sensor is on, and be turned off if that same sensor is off. The actuator1 automaton is provided sensor1 as sensor. If sensor1 goes on, actuator1 is turned on, and if sensor1 goes off, actuator1 is turned off. sensor2 going on or off has no effect on actuator1.

Automaton parameters can be used inside an automaton definition, to refer to declarations inside the automaton supplied for the automaton parameter. The automaton that is provided by the instantiation is essentially filled in wherever the parameter is used. The above is equivalent to:

automaton sensor1:
  event go_on, go_off;

  location off:
    initial;
    edge go_on goto on:

  location on:
    edge go_off goto off:
end

automaton sensor2:
  event go_on, go_off;

  location off:
    initial;
    edge go_on goto on:

  location on:
    edge go_off goto off:
end

automaton actuator1:
  event turn_on, turn_off;

  location off:
    initial;
    edge turn_on  when sensor1.on  goto on;

  location on:
    edge turn_off when sensor1.off goto off;
end

Multiple parameters

It is possible to use multiple parameters of the same kind, as well as different kinds of parameters:

automaton def X(event a, b; alg real c; event d):
  ...
end

event z;

x: X(z, z, 3 * 5, z);

Automaton definition X has four parameters: a, b, c, and d. Since a and b are both event parameters, a comma (,) is used to make sure the event keyword does not need to be repeated for parameter b. Algebraic parameter d is of a different kind, and is therefore separated using a semicolon (;).

Automaton instantiation x instantiates X with the event z (for the first, second, and fourth parameters), and value 15.0 (3 * 5, for the third parameter).