Components and Ports

A fundamental building block in Coco is the concept of a component that describes a system or sub-system and has defined interfaces with its environment. A component interacts with its environment by sending and receiving events across these interfaces via ports, where an event is either a synchronous function call and an asynchronous signal.

A port describes the visible events that a component can perform with its environment. These events are either functions that the component implements or signals that it emits, which other components in the system can call or receive respectively. In addition to defining the APIs, the port also specifies what sequences of function calls and signals are allowed.

Ports

A port describes the API for some part of a system. It can optionally have a state machine to formally define how the API behaves in terms of the sequence of function calls and signals that are allowed. Ports only describe the interface behaviour so therefore omit any implementation details.

declarationPort

where «types» is a comma-separated list of port types.

A port is declared with a name, and can optionally inherit one or more ports. It can also be labelled with the keyword final, which means that other ports cannot inherit from it.

The body of a port declaration consists of a collection of the following elements:

  • The function interface declaration is used to declare functions on a port. For example:

    function begin() : Nil
    function check(v : Int) : Bool
    
  • Similarly, the signal declaration is used to declare outgoing signals on a port. For example:

    outgoing signal ok()
    outgoing signal error(flag : Bool)
    
  • The field declaration’s type must either be a port or an Array of ports. For example:

    val oneControlPort : ControlPort
    val manyControlPorts : Array<ControlPort, 5>
    
  • The state machine declaration specifies the behaviour of a component that is visible across the port, and is defined in terms of the function calls and signals declared in the port, or inherited from another port.

  • Ports can also contain nested types.

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. Further, any port declarations within a composite or leaf port are prohibited from having state machines, regardless of whether they are used in a field declaration or not.

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.

A port can inherit multiple ports, written as follows:

port P1 : P2, P3 {
  
}

This means that P1 inherits all the function and signal declarations from both P2 and P3. Although P1, P2 and P3 are not allowed to have identical function interface and signal declarations, Coco supports function and signal overloading, as illustrated in the example below. There can be inheritance dependencies between P2 and P3, for example, P2 can inherit P3, but there cannot be cyclical inheritance dependencies between them.

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, and a signal to indicate that an error has occurred:

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

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. Further, the error() signal can include an error code to provide more information about what went wrong. 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 : NonVerified<Int>
    var c2 : NonVerified<Int>
  }

  external type ErrorId

  function switch(isOn : Bool, config : Config) : Nil
  outgoing signal error(id : ErrorId)
}

ConfigurableLight inherits the function and signal declarations from Light. It also adds an overloaded version of the switch function that has a second parameter with the configuration settings, and the error signal parameterised with the error code.

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 both of them have state machines, 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 all of its base ports, and the verification performed by the Coco Platform to verify this.

Components

A component describes a part of the overall system, and can only interact with its environment via its provided or required ports.

There are three types of components: An implementation component that specifies a complete description of the functionality of a component from which runtime code is generated; an encapsulating component that can own instances of other components and combine them together to form a larger part of a system; and an external component that represents some part of the system not defined in Coco, but which nevertheless interacts with Coco components.

A component declaration introduces a new type with the name specified by the identifier in the declaration.

declarationComponent

where the optional «type» is a component type, and has to be a reference to an external component declaration.

The field declaration’s type must be one of the following:

  • Provided<P>, Array<Provided<P>, size>, or SymmetricArray<Provided<P>, size>, which declares that the component has a port instance of the given type. For example:

    val client : Provided<DoorController>
    val clients : Array<Provided<DoorController>, 5>
    val manyClients : SymmetricArray<Provided<DoorController>, 2>
    
  • Required<P> or Array<Required<P>, size>, which declares that the component has a port instance of the given type. For example:

    val motor : Required<MotorController>
    val manyMotors : Array<Required<MotorController>, 3>
    
  • A component type or an array of a component type, which declares that the component has a component instance of the given type. For example:

    val motor : MotorControllerImpl
    val allMotors : Array<MotorControllerImpl,5>
    

Components can have constructors, which specify how instances of components are constructed and connected together.

declarationConstructor
[«visibility»] init(«parameters») = «block expression»

«parameter» := «identifier» : «type»

where parameters cannot include reference types.

A constructor can take parameters, such as timeout periods, which can be passed on to components upon construction. The body of a constructor is a block expression, and can consist of assignment expressions, connector functions, shared access functions, and the queue control functions (with the exception of the purge() functions), depending on the component’s type. In the body of a constructor, all initialisers (i.e. variable assignments) must come first in the block expression, before any other statements.

Note

Coco does not currently support the use of self in constructors, so users cannot currently write:

component C {
  val client : Provided<P>
  private val period : Duration

  init(period : Int) = {
    self.period = seconds(period);
  }
  
}

Instead this currently has to be written with distinct identifiers for the variables, for example:

component C {
  val client : Provided<P>
  private val period_ : Duration

  init(period : Int) = {
    period_ = seconds(period);
  }
  
}

However, this feature is on the roadmap to be added in the near future.

Components can declare private variables (denoted by the keyword private), which must be of non-verified types. The following example is of a component with two private variable declarations, where the first one is initialised inline, and the second one is initialised in the component’s constructor with its parameter:

component C {
  val client : Provided<P>
  private val a : NonVerified<Bool> = true
  private val b : NonVerified<Int>

  init(y : Int) = {
    b = y;
  }

  machine {
    
  }
}

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, and assignment expressions to initialise variables using the constructor parameters. 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.

The following example illustrates the use of constructor parameters, and how they can be used to initialise private variables in an implementation component:

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

  init(period : Duration) = {
    period_ = period;
  }

  machine {
    state Initial {
      client.run() = setNextState(Running)
    }
    state Running {
      after(period_) = {
        client.finished();
        setNextState(Initial)
      }
    }
  }
}

In this example, component C has a constructor that takes a parameter period of type Duration, and is used to initialise the private variable period_ of the same type. This allows users to declare multiple instances of C each passing different values for the time durations, for example:

component Enc {
  val c1 : C = C(seconds(10))
  val c2 : C = C(seconds(100))
  
}

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 assignment expressions to initialise component instances using constructor parameters, and connector functions, which specify the connections between 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 example illustrates the use of constructor parameters in an encapsulating component, and how they can be used to initialise component instances it owns:

@runtime(.MultiThreaded)
component System {
  val client : Provided<P>
  val manyC : ManyC
  val c0 : C
  val c1 : C

  init(t0 : Duration, t1 : Duration) = {
    c0 = C(t0);
    c1 = C(t1);
    connect(client, manyC.client);
    connect(manyC.source[0], c0.client);
    connect(manyC.source[1], c1.client);
  }
}

In this example, the encapsulating component System declares two instances c0 and c1 of component C, which has a parameterised constructor of the following form:

component C {
  val client : Provided<P>
  private val period_ : Duration

  init(period : Duration) = {
    period_ = period;
  }

  machine {
    
  }
}

The encapsulating component System initialises c0 and c1 in its constructor with the constructor’s parameters t1 and t2. Coco also supports instances of components with constructors being initialised inline, for example, c0 and c1 could be initialised as follows:

  val c0 : C = C(seconds(10))
  val c1 : C = C(seconds(100))

For an instance of an array of components with constructors, each array index has to be initialised individually, as illustrated in the following example:

@runtime(.MultiThreaded)
component System3 {
  val client0 : Provided<P>
  val client1 : Provided<P>
  val source : Array<C, 2>

  init() = {
    source[0] = C(seconds(10));
    source[1] = C(seconds(100));
    connect(client0, source[0].client);
    connect(client1, source[1].client);
  }
}

The instance source is an array of two components of type C, which has a constructor. Each instance in the array has to be initialised in the encapsulating component’s constructor.

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 C1 and C2, and a constructor specifying that: the required port of C1 is connected to the provided port of C2, and the required port of C2 is in turn connected to the provided port of C1. This forms a dependency cycle between C1 and C2, which is prohibited.
  • All of the connections must also adhere to any shared access functions specified in the corresponding components.
  • For single-threaded encapsulating components, there are some restrictions on multi-client architectures (i.e. where there are components with required ports that are shared with other components). In particular, if a component C has a required port r1 that is connected to a provided port pShared, and pShared is shared with other clients, then pShared cannot be connected to a required port of a component that is directly or indirectly connected to a required port of C. The following architecture is an example of one that is prohibited:
ST Architecture 2 (prohibited) C r1 r2 C3 pShared C2 r3

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:

HeatingSystem rad1 : Radiator controller : RadiatorControllerImpl valve : ValveBase sensor : SensorBase client client valve sensor client client rad2 : Radiator controller : RadiatorControllerImpl valve : ValveBase sensor : SensorBase client client valve sensor client client rad3 : Radiator controller : RadiatorControllerImpl valve : ValveBase sensor : SensorBase client client valve sensor client client controller : ZoneControllerImpl client radiators[0] radiators[1] radiators[2] Gui zoneController

See also

Components with Symmetric Provided Ports for a summary on how to connect with components that have symmetric arrays in their provided ports.

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 have at least one provided or required port. 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); }
}

An external component may have both provided and required ports:

@queue(2)
@runtime(.MultiThreaded)
external component MotionDetector {
  val client : Provided<Detector>
  val sensor : Required<Sensor>
}

This gives additional flexibility when building architectures consisting of Coco and non-Coco code, for example:

System client : Light Ⓟ source : Hal Ⓡ System System System light : LightImpl light : LightImpl light LightImpl client : Light Ⓟ source : Detector Ⓡ sensor : SensorImpl sensor : SensorImpl sensor SensorImpl client : Sensor Ⓟ hal : Hal Ⓡ detector : MotionDetector detector : MotionDetector detector MotionDetector client : Detector Ⓟ sensor : Sensor Ⓡ

In this example architecture above, the external component MotionDetector is using and being used by Coco components.

External Implementation Components

In addition to external components, Coco also allows users to refer to implementations of external components defined elsewhere in the code. This is achieved by declaring an external implementation component, as illustrated in the following example:

@runtime(.SingleThreaded)
external component LightBase {
  val client : Provided<Light>
}

@CPP.mapToType("my_ns::LightImpl", .Value, .User("LightImpl.h"))
external component LightImpl : LightBase {}

The external implementation component LightImpl refers to a handwritten subclass of the corresponding abstract base class represented by the external component LightBase. This is also sometimes referred to as component inheritance, where the child component LightImpl inherits the parent component LightBase, written as LightImpl : LightBase. External implementation components can be directly referred to in encapsulating components, as illustrated in the following example:

@runtime(.SingleThreaded)
component Enc {
  val client : Provided<Light>
  val light : LightImpl

  init() = {
    connect(client, light.client);
  }
}

This encapsulating component creates an instance light of the actual implementation LightImpl defined elsewhere in the code. Using external implementation components make it easier to instantiate and manage encapsulating components in the handwritten code, and also means that Coco manages the component’s lifetime.

External implementation components can also have constructors, as illustrated in the following example:

enum LightMode {
  case Flashing
  case Steady
}

@CPP.mapToType("LightImpl", .ConstReference, .User("LightImpl.h"))
external component ConfigurableLightImpl : LightBase {
  init(setting : LightMode) = {}
}

@runtime(.SingleThreaded)
component ConfigurableEnc {
  val client : Provided<Light>
  val light : ConfigurableLightImpl

  init() = {
    light = ConfigurableLightImpl(.Steady);
    connect(client, light.client);
  }
}

If an external component has setAccess functions declared in its constructor, then a child component that inherits this external component will also inherit these setAccess functions, and is not allowed to override them. Consider the following example:

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

  init() = {
    setAccess(zoneController, .Shared);
  }
}

@CPP.mapToType("my_ns::GuiImpl", .Value, .User("GuiImpl.h"))
external component GuiImpl : Gui {}

In this example, the external implementation component GuiImpl inherits the external component Gui, and therefore also inherits the setAccess functions declared in Gui.

Note

When using external components, users must write their own implementations for them, which are not verified by the Coco Platform.

Components with Symmetric Provided Ports

Some components that have multiple provided ports treat all elements of the array symmetrically, in that they do not distinguish any particular element of the array. Coco has a special way of verifying these sorts of components using SymmetricArray. Rather than verify the component with the actual array size, which can be large depending on the number of clients it has, Coco will automatically compute the minimum array size it needs to verify in order to guarantee that the component will work correctly for an array of any size greater than this minimum threshold.

Consider the following port declaration:

port LockableResource {
  function lock() : Bool
  function unlock() : Nil
  function action() : Nil
  outgoing signal finished()

  machine {
    state Unlocked {
      lock() = nondet {
        {
          return false;
        },
        {
          setNextState(Locked.Ready);
          return true;
        },
      }
    }

    state Locked {
      unlock() = setNextState(Unlocked)

      state Ready {
        action() = setNextState(Running)
      }

      state Running {
        spontaneous = {
          finished();
          setNextState(Ready);
        }
      }
    }
  }
}

In the Unlocked state, the port can perform a lock() request, which nondeterministically succeeds or fails. If it succeeds, then it can perform some action, represented by the function action(), and send the signal finished() upon completion, or it can perform an unlock() request. The following component declaration is an example of a component that has a symmetric array of provided ports of type LockableResource, and treats all entries identically and independently of their index value:

@runtime(.MultiThreaded)
component ResourceImpl {
  val client : SymmetricArray<Provided<LockableResource>, 100>

  machine {
    state Unlocked {
      client[val i].lock() = {
        setNextState(Locked(i).Idle);
        return true;
      }
    }

    state Locked(owner : SymmetricArrayIndex) {
      client[val j | j != owner].lock() = false
      client[owner].unlock() = setNextState(Unlocked)

      state Idle {
        client[owner].action() = setNextState(Running)
      }

      state Running {
        after(seconds(10)) = {
          client[owner].finished();
          setNextState(Idle);
        }
      }
    }
  }
}

Even though this component can be used by multiple clients, it only allows one client to acquire the lock and perform an action at a given time. The component treats all of its clients identically, and only needs to know which client has acquired the lock and can therefore access the resource, while ensuring that the others are unable to do so.

The size parameter of the array is of the special type SymmetricArrayIndex. It represents the actual number of clients that will be connected to the component at runtime, as opposed to the size verified, which Coco will automatically compute regardless of the argument given for the size. The number of provided port instances that are verified is visible in the assertions view.

Components with symmetric arrays can be used in encapsulating components in the usual way. The only minor difference is how they are referenced in the connect functions when specifying how the instances are connected together, as highlighted by the following example:

@runtime(.MultiThreaded)
@queue(2)
component TestResourcesImpl {
  val client : Provided<TestResources>
  val r1 : Required<LockableResource>
  val r2 : Required<LockableResource>

  machine {
    // …
  }
}

@runtime(.MultiThreaded)
component System {
  val client : Provided<TestResources>
  val tester : TestResourcesImpl
  val resource : ResourceImpl

  init() = {
    connect(client, tester.client);
    connect(resource.client, tester.r1);
    connect(resource.client, tester.r2);
  }
}

In this example, the component TestResourcesImpl has two required ports of type LockableResource. The encapsulating component System declares instances of TestResourcesImpl and ResourceImpl (declared above), and connects the two required ports of the TestResourcesImpl instance with the provided port of the ResourceImpl instance. Unlike normal arrays, where the index must be specified when connecting with an array of ports (for example, connect(resource.client[1], )), no index is specified for symmetric arrays. Instead, each client is connected to a free slot, and an error is raised if there is not a free one.

Note

Coco currently supports the use of symmetric arrays for provided ports in implementation components only.

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. A signal instance only refers to the signal name, and does not include any values passed as arguments. For example, a signal of the form sig(true) in a component’s queue will be overwritten by the incoming signal sig(false).

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

Log function

Coco has a builtin log function, which can be used in a component state machine to add custom 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.

See also

Format string expression, which shows how data can be included within the log messages.

Logging Events.