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.
-
declaration
Port
¶ [«visibility»] port «identifier» [: «types»] [final] { «port elements» } «port element» := «function interface declaration» | «signal declaration» | «field declaration» | «state machine declaration» | «enum declaration» | «port declaration» | «static constant declaration» | «struct declaration» | «type alias declaration» | «external type declaration»
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: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 anArray
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
orsignal
declarations, and any other port elements, but does not have anyfield
declarations. - A composite port is one that has one or more
field
declarations, but does not have anyfunction interface
orsignal
declarations. If a composite port contains a fieldf : P
, whereP
is also a port, thenP
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:
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.
-
declaration
Component
¶ [«visibility»] [external] component «identifier» [: «type»] { «component elements» } «component element» := «field declaration» | «variable declaration» | «constructor declaration» | «state machine declaration» | «static constant declaration»
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>
, orSymmetricArray<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>
orArray<Required<P>, size>
, which declares that the component has a port instance of the given type. For example: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.
-
declaration
Constructor
¶ [«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:
Instead this currently has to be written with distinct identifiers for the variables, for example:
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:
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:
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:
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 portr1
that is connected to a provided portpShared
, andpShared
is shared with other clients, thenpShared
cannot be connected to a required port of a component that is directly or indirectly connected to a required port ofC
. The following architecture is an example of one that is prohibited:
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
:
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:
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:
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:
An external component may have both provided and required ports:
This gives additional flexibility when building architectures consisting of Coco and non-Coco code, for example:
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:
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:
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:
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.
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:
This is an example of a component C
with a bounded queue of size 3. Coco also allows users to write this as:
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:
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)
andsetAllow(r, .sigA, .sigB, .sigC)
.setAllow
is only permitted in a component’sConstructor
, 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 signalsig(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 stateMain
to ensure that the component’s queue is empty before entering the stateTerminated
.
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.