Components and Ports¶

Leaf and Composite Ports¶

A port is either a leaf or composite port:

• A leaf port is one that has one or more function interface or signal declarations, and any other port elements, but does not have any field declarations.
• A composite port is one that has one or more field declarations, but does not have any function interface or signal declarations. If a composite port contains a field f : P, where P is also a port, then P is prohibited from containing a state machine.

Therefore, a port cannot validly have both function interface or signal declarations, and field declarations.

The following example is a leaf port declaration to repeatedly switch a component on and off:

port Switch {
  function on() : Nil
  function off() : Nil
  outgoing signal status(isOn : Bool)
  outgoing signal fault()

  machine {
    state Off {
      on() = {
        status(true);
        setNextState(On);
      }
    }
    state On {
      off() = {
        status(false);
        setNextState(Off);
      }
      spontaneous = {
        fault();
        setNextState(Off);
      }
    }
  }
}

Port Switch declares two functions, on() and off(). When called, these functions result in a corresponding signal being sent, and a state transition to reflect the change in status. For example, in the initial state Off, P can perform the call on(), resulting in the signal status(true) being sent to its client, and changing to state On. In state On, in addition to offering the function off(), the port can also perform a spontaneous transition resulting in a fault() signal being sent, and a state transition back to Off.

The following example is a composite port declaration, which restructures the example above by introducing two nested ports, also known as child ports, and extends the behaviour:

port SwitchComposite {
  port Control {
    function on() : Nil
    function off() : Nil
    outgoing signal status(isOn : Bool)
  }
  port Comms {
    function getStatus() : Bool
    outgoing signal fault()
  }

  val control : Control
  val comms : Comms

  machine {
    state Off {
      control.on() = {
        control.status(true);
        setNextState(On);
      }
      comms.getStatus() = true
    }
    state On {
      control.off() = {
        control.status(false);
        setNextState(Off);
      }
      comms.getStatus() = false
      spontaneous = {
        comms.fault();
        setNextState(Off);
      }
    }
  }
}

Port SwitchComposite declares two child ports, Control and Comms, each declaring a set of functions and signals, and declares an instance of each of these ports, called control and comms, respectively. Its state machine then specifies the overall port behaviour using these instances.

Signals¶

Every port declaration contains an implicit declaration of a type called Signal that represents a signal that has been instantiated with values for all of its parameters, but has not yet been sent. For example, if a port P defines a signal sig(x : Bool), then P.sig(true) is a value of type P.Signal that represents a signal that has not yet been sent. Ports also contain an implicitly declared function send(sig : Signal) : Nil, which is callable on an instance of type Provided<P>, and sends the given signal to all connected clients. For example, if client : Provided<P> and s : P.Signal, then client.send(s) will send the signal s over the port client.

The type Signal is comparable for equality precisely when every parameter of every signal of the base port and inherited ports has an instance of Eq. Signal does not have an instance of Default declared, but it is verifiable.

The following example illustrates how signals can be passed as parameters in functions and states in a simple port:

port P {
  function check(s : Signal) : Nil
  function cancel() : Bool
  outgoing signal ok()
  outgoing signal fail()

  machine {
    state Idle {
      check(sig : Signal) = setNextState(SendSignal(sig))
    }
    state SendSignal(s : Signal) {
      spontaneous = {
        send(s);
        setNextState(Idle);
      }
    }
  }
}

Port P declares the function interface check(s : Signal), which has a parameter of type Signal. This means that it can be called with either of the two signals declared in P. When called in state Idle, the state machine transitions to parameterised state SendSignal(sig), where sig is the signal received on the function call. In SendSignal(sig), the port will spontaneously emit the signal sig via the function send(sig), which is automatically declared in P.

The following example illustrates how the type Signal in P is referenced by a component that implements it:

@runtime(.MultiThreaded)
component C {
  val client : Provided<P>

  machine {
    state Idle {
      client.check(sig : P.Signal) = setNextState(SendSignal(sig))
    }
    state SendSignal(s : P.Signal) {
      after(milliseconds(10)) = {
        client.send(s);
        setNextState(Idle);
      }
    }
  }
}

The state machine of component C is very similar to that of port P above, with the exception that a timer transition is used in the SendSignal state instead of the spontaneous transition used in P. The signal type is referenced as P.Signal when used in the function and state parameters of C, in order to correctly identify its scope.

Port Inheritance¶

A port can be a subtype of another port by using port inheritance, written as follows:

port P1 : P2 {
  …
}

In this example, P1 inherits P2, and works in the same way as inheritance in other common programming languages. The term base port is used to refer to the port that is being inherited, and the derived port is used to refer to the port inheriting the base port. In this example, P1 is the derived port, and P2 is the base port.

When using port inheritance, it is not possible to mix leaf and composite ports, as this would lead to invalid port declarations. If a port inherits from a leaf port, then the derived port cannot have field declarations in it. Similarly, if a port inherits from a composite port, then the derived port cannot have function interface or signal declarations.

Consider the following example of a leaf port for a light, which has a single function to switch it on and off:

port Light {
  function switch(isOn : Bool) : Nil
}

Now consider specifying a port for a more complex light that, in addition to being able to switch it on and off, is also configurable with additional information. Instead of copying the function declaration from the Light port, and then adding the additional declarations, the configurable port can inherit Light:

port ConfigurableLight : Light {
  struct Config {
    var c1 : Int
    var c2 : Int
  }

  function switch(isOn : Bool, config : Config) : Nil
}

ConfigurableLight inherits the function declaration from Light, and adds an overloaded version of switch that has a second parameter with the configuration settings.

A port typically has a state machine as part of its declaration, which describes its behaviour in terms of the function calls and signals declared on that port, and those inherited from another port. When a port inherits another port, and either or both of them have state machines declared, then the behaviour of the derived port must comply with that of the base port it inherits. See Implements the Base Port Specification for details about what it means for a port to correctly comply with its base port, and the verification performed by the Coco Platform to verify this.

Implementation Components¶

An implementation component describes the complete behaviour of a component in terms of the functions and signals declared on its provided port, and the functions and signals it can call and receive respectively on its required ports. It must implement the functions and signals in accordance with its provided port specification, and may call any of the functions on its required ports. It must also be able to handle all of the signals that it can receive from its required ports. An implementation component is sufficiently detailed that the corresponding runtime code can be automatically generated from it.

An implementation component must have at least one provided or required port, and precisely one state machine declaration. It can also have at most one constructor, which can only consist of queue control functions. Implementation components must be labelled with the @runtime attribute.

The following example is part of a door controller system for an elevator:

@queue(6)
@runtime(.MultiThreaded)
component DoorControllerImpl {
  val client : Provided<DoorController>
  val motor : Required<MotorController>
  val detector : Required<CollisionDetector>

  machine {
    state Uninitialised {
      client.initialise() = {
        if (detector.initialise() && motor.initialise()) {
          setNextState(Ready);
          return true;
        }
        setNextState(Terminating);
        return false;
      }
    }
    state Terminating {
      // …
    }
    state Ready {
      // …
    }
  }
}

DoorControllerImpl has to implement DoorController as its provided port, and declares instances of MotorController and CollisionDetector as its required ports.

Encapsulating Components¶

An encapsulating component is used to define a collection of components, and specify how they are connected together. It can have zero or more provided or required ports, it cannot have a state machine, and it must be labelled with the @runtime attribute.

Further, an encapsulating component must have one constructor declaration, which can consist of connector functions only, specifying the connections between the encapsulating component’s ports and those of the component instances it owns. For example:

init() = {
    connect(p1, p2);
}

In this simple constructor, connect(p1, p2) specifies that port p1 is connected to port p2.

The following rules apply regarding the connections between component instances owned by an encapsulating component:

• For every component instance within the encapsulating component, at least one of its provided ports must be connected, and all of its required ports must be connected.
• Connections can only be defined between the ports of an encapsulating component and the provided and required ports of the top-most components it owns.
• The ports must be connected together in such a way that the overall collection of components and their ports within the encapsulating component is acyclic. An example of how this acyclic property is violated is if an encapsulating component has (instances of) two components C₁ and C₂, and a constructor specifying that: the required port of C₁ is connected to the provided port of C₂, and the required port of C₂ is in turn connected to the provided port of C₁. This forms a dependency cycle between C₁ and C₂, which is prohibited.
• All of the connections must also adhere to any shared access functions specified in the corresponding components.

There are four connector functions, each defined in turn below:

function connect<ProvidedPort, RequiredPort where IsPort<ProvidedPort>, IsPort<RequiredPort>, ProvidedPort <: RequiredPort>(left : Provided<ProvidedPort>, right : Required<RequiredPort>) : Nil¶

Connects a provided port left of one component with a required port right of another component.

function connect<ProvidedPort, RequiredPort where IsPort<ProvidedPort>, IsPort<RequiredPort>, ProvidedPort <: RequiredPort>(left : Required<RequiredPort>, right : Provided<ProvidedPort>) : Nil

Connects a required port left of one component with a provided port right of another component.

function connect<P where IsPort<P>>(left : Required<P>, right : Required<P>) : Nil

Connects a required port left of one component with a required port right of another component.

function connect<P where IsPort<P>>(left : Provided<P>, right : Provided<P>) : Nil

Connects a provided port left of one component with a provided port right of another component.

Consider the following example:

@runtime(.MultiThreaded)
component Radiator {
  val client : Provided<RadiatorController>
  val controller : RadiatorControllerImpl
  val sensor : SensorBase
  val valve : ValveBase

  init() = {
    connect(client, controller.client);
    connect(controller.sensor, sensor.client);
    connect(controller.valve, valve.client);
  }
}

Radiator is an encapsulating component that provides one port client, and owns three component instances, controller, sensor and valve. The encapsulating component’s provided port client is connected to the provided port client in the component instance controller. In turn, the controller’s required ports sensor and valve are connected to the corresponding provided ports of the component instances sensor and valve.

Now consider the following example of an encapsulating component comprising one instance of the Gui external component, one instance of the ZoneController component, and three instances of the Radiator component:

@runtime(.MultiThreaded)
component HeatingSystem {
  val gui : Gui
  val rad1 : Radiator
  val rad2 : Radiator
  val rad3 : Radiator
  val controller : ZoneControllerImpl

  init() = {
    connect(gui.zoneController, controller.client);
    connect(controller.radiators[0], rad1.client);
    connect(controller.radiators[1], rad2.client);
    connect(controller.radiators[2], rad3.client);
  }
}

As specified in the constructor, the component ZoneControllerImpl has an array of required ports of type Radiator, each of which is connected to the client provided ports of rad1, rad2 and rad3 respectively. Further, the required port zoneController of the external component instance gui is connected to the provided port client of controller.

The following diagram is a graphical representation of the component architecture defined by HeatingSystem:

External Components¶

An external component is one that describes some part of the system that is not defined in Coco, but nonetheless interacts with the Coco components being developed. They are used to support the integration of the code generated by the Coco Platform into existing code that was developed using other tools.

An external component is defined with the keyword external, and must either have at least one provided port or at least one required port, but not both. It must be labelled with the @runtime attribute. For example:

@runtime(.MultiThreaded)
external component SensorBase {
    val client : Provided<Sensor>
}

This external component SensorBase provides an instance of the port Sensor, which specifies the interactions that components using this SensorBase component can assume.

The following external component is an example of one with a required port:

@queue(2)
@runtime(.MultiThreaded)
external component Gui {
  val zoneController : Required<ZoneController>
}

External components with required ports can have a queue, as illustrated in this example above. The generated code for Gui will now contain a background thread that is used to process the signals. The queue attribute can be used in the normal way, which means that either bounded or unbounded queues can be generated.

External components may also call the setAccess functions to specify the access rights of their required ports with other components. For example, the following external component marks its required port as shared:

@queue(2)
@runtime(.MultiThreaded)
external component Gui {
  val zoneController : Required<ZoneController>
  init() = { setAccess(zoneController, .Shared); }
}

Access to Shared Ports¶

By default, a component has sole access to all of the events on its required ports. However, it is sometimes necessary for a component to be able to specify that other components can also access some of these events. This can arise, for example, when a port is being used by several other components. A component can specify how the other components can have access to its required ports by using the following functions:

function setAccess<Port where IsPort<Port>>(p : Required<Port>) : Nil¶

Gives the other components access to all events on p, and removes access to any of them by the current component.

function setAccess<Port, val size : Int where IsPort<Port>>(p : Array<Required<Port>, size>) : Nil

Same as the previous one, but applies to all of the ports on p.

function setAccess<Port where IsPort<Port>>(p : Required<Port>, accessLevel : PortAccess) : Nil

Gives the other components access to the events on p as specified by accessLevel.

function setAccess<Port, val size : Int where IsPort<Port>>(p : Array<Required<Port>, size>, accessLevel : PortAccess) : Nil

Same as the previous one, but applies to all of the ports on p.

The type PortAccess is defined as follows:

enum PortAccess¶

Specifies the access a component retains to a port after sharing it with other components, and has the following cases:

case OtherOnly¶

The current component is no longer allowed to make function calls or receive signals on the port.

case SignalOnly¶

The other components are allowed to make function calls and receive signals, but the current component can only receive signals.

case Shared¶

The other components share access with the current component, and so all of them can make function calls or receive signals.

The setAccess functions can use implicit member expressions in their arguments, for example, setAccess(r, .Shared).

Queues¶

An implementation or external component that has one or more required ports can have a queue by labelling it with the @queue attribute, which then stores the signals it receives from its required ports. If a component is not labelled with this attribute, then it is assumed not to have one.

There are two types of queues, namely bounded and unbounded queues.

A bounded queue is one that has a finite capacity of a specified size, both for verification and at runtime, for example:

@queue(Queue.Bounded(3))
@runtime(.MultiThreaded)
component C {
  …
}

This is an example of a component C with a bounded queue of size 3. Coco also allows users to write this as:

@queue(3)
@runtime(.MultiThreaded)
component C {
  …
}

If the queue is full, and a required port tries to send a signal to C, then this would be a dynamic error caught during verification.

An unbounded queue is one that is unbounded at runtime, but has a specified fixed capacity during verification in such a way that the verification is still sound. Although components can always be specified with unbounded queues, it is recommended that they are only used with the components that have required ports with @unbounded transitions.

The following example illustrates how a component is specified with an unbounded queue:

@queue(Queue.Unbounded(3))
@runtime(.MultiThreaded)
component C {
  …
}

Component C has an unbounded queue. The specified queue size of 3 is for the purposes of the verification. Unlike the unbounded signals, all other signals that are not unbounded will be treated in the same way as though it was a bounded queue. Therefore, it is still possible for these other signals to cause a queue overflow error.

If a component C has a required port P with @unbounded transitions, then it must have an unbounded queue, and its state machine must satisfy the following conditions:

• It does not use the function setUnique on any signals sent by P.
• It does not make more than one function call on P without returning to an idle state first.

These restrictions, together with the ones imposed on the ports that have unbounded transitions, are required to ensure that the verification is sound.

Queue Control¶

By default, a component’s queue simply stores all of the signals that it receives from its required ports, and the component then processes each of them in turn. However, in some cases it is useful to be able to treat some signal events differently, for example, by allowing components to ignore certain signals or by limiting the number of instances a given signal that can be stored in the queue. A component can control how signals are treated using the following built-in functions.

function unsubscribe<Port where IsPort<Port>>(r : Required<Port>) : Nil¶

Unsubscribes the component from a required port r. This prevents the component from receiving further signals from r, and also purges the queue of all signals from r, as if purge(r) was called.

function subscribe<Port where IsPort<Port>>(r : Required<Port>) : Nil¶

Subscribes the component to a required port r, and then receives signals from that port. By default, all of a component’s required ports are subscribed when the component’s state machine starts, unless they have been unsubscribed in the component’s constructor.

function setAllow<Port where IsPort<Port>>(r : Required<Port>, signal… : IsPort<Port>.Signal) : Nil¶

Allows the signals to be received by the component from a subscribed required port r, and ignores any other signals that are not listed. This is a variadic function, and can therefore have a variable number of arguments of type IsPort<Port>.Signal, for example, setAllow(r, .sigA) and setAllow(r, .sigA, .sigB, .sigC). setAllow is only permitted in a component’s Constructor, and can only be called once per required port.

function setUnique<Port where IsPort<Port>>(r : Required<R>, signal : IsPort<Port>.Signal) : Nil¶

Restricts the component’s queue to only storing one instance of signal from required port r. When a signal is received, and the component’s queue already contains an instance of it, then it will be overwritten with the new one in the same position in the queue. This function is only permitted in the component’s Constructor, and can only be called once per signal.

function purge<Port where IsPort<Port>>(r : Required<Port>) : Nil¶

Deletes all events in the component’s queue that came from required port r.

function purge() : Nil

Deletes all events in the component’s queue. A common use of this function is in the exit function in the state Main to ensure that the component’s queue is empty before entering the state Terminated.

The functions setAllow(…) and setUnique(…) can use implicit member expressions in their arguments, for example, setAllow(r, .sigA, .sigB) and setUnique(r, .sigA).

Logging¶

Coco has a builtin log function, which can be used in a component state machine to add logging information to the logging output stream.

external function log(s : String) : Nil¶

Parameter s:	the string to be written to the logging output stream.
Type s:	String

When executed at runtime, log(s) adds s to the logging output stream.