## 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:

- Algebraic parameters

- Event parameters

- Location parameters

- Automaton parameters

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).