State Machines¶

State machines are used to specify the behaviour of ports and components. A port declares the interfaces implemented by a component on a specific boundary, and may also specify the ordering in which all interactions across the port can occur by declaring a state machine in the port declaration. Port state machines are often nondeterministic as they only specify a partial view of how a component interacts on a given boundary, in terms of the events that are visible across that boundary, and omits any of the component’s implementation details. In contrast, the implementation of a component is specified by declaring a state machine in the component declaration. This state machine has to be sufficiently detailed that the runtime code can be generated from it.

A state machine declaration introduces a new type with the name specified by the identifier in the declaration. A state machine also introduces a type State, which ranges over the possible states of the machine.

declarationState Machine¶

«visibility» machine [«identifier»] [: «identifier»] {
  «state machine elements»
}

«state machine element» :=
  «function declaration»
  | «state declaration»
  | «static constant declaration»
  | «type declaration»
  | «variable declaration»

A state machine is declared with the keyword machine followed by a name, which is optional. A state machine can inherit another state machine, denoted by the second identifier after the colon. In this case, both of them must be declared with a name.

In a port state machine declaration, non-verified types (i.e. types that do not have an instance of Verified) are not allowed anywhere except in parameters of event transitions. The reason for this exception is that these parameters must precisely match their types specified in the corresponding function or signal declarations.

States¶

In a state machine, there are two types of states, namely an event state and an execution state. An event state is one that can receive incoming events and respond by executing the corresponding transition’s event handler. Further, port state machines can also execute special actions spontaneously in event states. In contrast, an execution state is one that can only execute the block of code defined in that state.

declarationState¶

«event state» | «execution state»

Every state machine has two built-in event states called Main and Terminated. The state Main is the ancestor of all user-defined states, and all declarations in the state machine are declarations in Main. The state Terminated denotes the termination of a state machine.

Within a state, the special terms self and context can be used to refer to specific instances of ports and components. self has the type of the state machine and gives explicit access to the contents of the instance of the state machine in which it is used. context refers to the port or component containing the current or parent state machine. context has the type of that port, component or state machine and provides access to instances of the fields of a component.

Event States¶

An event state is one that can receive incoming events, such as function calls and signals, and respond by executing the corresponding event handlers. Further, a port state machine can also execute special actions spontaneously, and component state machines can execute timer expiry events in event states.

declarationEvent State¶

state «identifier»[(«parameters»)] {
  «event state elements»
}

«event state element» :=
  «entry function declaration»
  | «enum declaration»
  | «exit function declaration»
  | «function declaration»
  | «state declaration»
  | «state invariant declaration»
  | «static constant declaration»
  | «struct declaration»
  | «transition declaration»
  | «type alias declaration»
  | «variable declaration»

where the parameters must be immutable values (for example, they cannot be references).

The following event state elements are only valid in the topmost event state Main: enum, struct, and type alias declarations.

If an event state has a parameter that is not comparable for equality, then it cannot have nested states, and is not allowed to call the setNextState functions, the latter of which is checked by the verification.

A state that has a parameter that is not comparable for equality is allowed to call the setNextStateReEnter functions, because any entry or exit functions will be executed regardless of whether the setNextStateReEnter function causes the state machine to transition to a different state instance of the state or not.

declarationEntry Function¶

entry() = «expression»

An entry function is executed upon entry into a state S in which it is declared. The expression is allowed to have a state transition function only if the target state is a direct descendant of S, and does not cause S to be re-entered.

declarationExit Function¶

exit() = «expression»

An exit function is executed upon exit of the state in which it is declared. The expression is not allowed to contain any state transition functions.

declarationState Invariant¶

assert(«expression»)

where the expression must be a simple one of type Bool, and must be strictly side-effect free.

State invariants can be declared in any event state. When the execution of a transition has completed, any relevant entry and exit actions are executed, and then all invariants in the current state are checked. This includes invariants declared in the current state, and in all its ancestor states. An invariant is violated if its expression evaluates to false. For further details on the execution semantics of state machines, see Executing a State Machine.

Execution States¶

In contrast with an event state, an execution state simply executes a block expression to completion, and does not have any transitions declared within it.

declarationExecution State¶

execution state «identifier»[(«parameters»)] {
  «block expression»
}

where the parameters must be immutable values (for example, they cannot be references).

The block expression in an execution state specifies a block of code to be executed when the state is entered.

Consider the following example:

@runtime(.MultiThreaded)
component C {
  val client1 : Provided<P1>
  val client2 : Provided<P1>
  val source : Required<P2>

  machine {
    state Idle {
      client1.begin() = setNextState(Running)
      client2.begin() = setNextState(Running)
    }
    execution state Running {
      var isDone : Bool;
      isDone = source.check();
      client1.status(isDone);
      client2.status(isDone);
      setNextState(Idle);
    }
  }
}

Component C has two states, an event state called Idle, which has transitions declared within it, and an execution state called Running consisting of a block expression, which will be immediately executed upon entry into the Running state. The block expression declares a local variable called isDone of type Bool, and assigns the return value from calling the function check() on its required port source. This is followed by sending two signals via its provided ports client1 and client2, and finally calling the state transition function setNextState(Idle). When all actions in the block expression have been executed, the state machine changes state to Idle.

The one exception where a component state machine can receive an incoming signal when it is in an execution state is via a simple await statement or compound await expression, as illustrated in the following example:

@runtime(Runtime.MultiThreaded)
@queue(1)
component C {
  val client : Provided<P>
  val source : Required<R>

  machine {
    state Idle {
      client.begin() = {
        source.check();
        setNextState(Waiting);
      }
    }
    execution state Waiting {
      await {
        source.isDone(v) if (v) => {
          client.done();
          setNextState(Idle)
        },
        _ => {},
      }
      setNextState(Idle);
    }
  }
}

In this example, when the component in the execution state Waiting, it waits to receive one of the signals from its required port source. If it receives isDone(true), then the component sends done() to its client and returns to the state Idle. If it receives any other signal, then the await is unresolved and C will remain in this state. In the event that C is not guaranteed to eventually receive isDone(true), then it will become deadlocked.

Note

Execution states in component and port state machines must contain a state transition function to another state, otherwise the state machines would become unresponsive. See responsiveness for ports and responsiveness for components for further details, and how execution states can cause these verification checks to fail.

Note

Execution states can only be used in the multi-threaded runtime, as they are executed on a component’s background thread. See Multi-threaded Runtime and Executing a State Machine for further details.

Parameterised States¶

An event state and execution state can be parameterised. When a state is declared with parameters, then each instance of the state is treated as a distinct state, as opposed to treating the parameterised state and all instances of it as a single state. This distinction is particularly relevant when using the state transition functions.

Consider the following example:

port Switch {
  function on() : Nil
  function off() : Nil

  machine {
    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(!isOn))
      if (isOn) off() = setNextState(S(!isOn))
    }
  }
}

Port Switch allows the functions on() and off() to be called alternately, starting with on(). This is specified by a simple state machine comprising a parameterised state S(isOn : Bool) with parameter isOn of type Bool. The state machine starts in state S(false), where isOn is instantiated to the default value of Bool. In this state, it can only perform function on(), and transition to the state S(true). In S(true), it is only able to perform function off(), and transition back to S(false). Although there is only one parameterised state defined in this state machine, Coco treats the two instances of this state as two distinct states, namely S(true) and S(false).

Note

Instances of parameterised states are treated as distinct states in Coco. This impacts how the state transition functions behave when used in parameterised states.

Main State¶

Every state machine has a built-in event state called Main, which is the ancestor of all user-defined states within the state machine. All declarations in the state machine are declarations in Main. When a state machine is started, the initial state it enters is the first user-defined state in Main. If there are no user-defined states, then the state machine will start in state Main. This default behaviour can be overidden by declaring a entry function in Main.

Terminated State¶

Every state machine has a builtin event state called Terminated, which represents the termination of a component. No declarations can be added to this state, and all incoming events are illegal. A transition to Terminated is the final action of a state machine, and the state machine cannot be restarted from this state. When a component state machine enters Terminated, the following actions are executed in its entry function:

Unsubscribe from all of its required ports;
Unregister from all of its required ports, which means that they will recursively terminate. Termination cascades through the system from top to bottom.
Call purge to delete all of the signals from the its queue.

Terminated is a sibling of Main, and therefore a state transition to Terminated from any state will execute the exit function declared in Main (in addition to any others executed in the transition to Terminated).

See also

Termination section for details about Coco’s default termination behaviour.

Unused Transition section for details and examples of how the default termination behaviour can be overridden using unused transitions.

State Hierarchy¶

Every event state except for Terminated can have nested states to any depth, forming a rooted tree of parent-child relationships with Main as the root. The parent of a state S is the state connected to S on the path to the root. Every state has a unique parent, except for the root Main which has no parent. A child of a state S is a state of which S is the parent. A sibling to a state S is any other state in the tree which has the same parent as S.

A descendant of a state S is any state that is either itself, the child of S, or is (recursively) the descendant of any of the children of S. Conversely, an ancestor of a state S is any state that is either itself, the parent of S, or is (recursively) the ancestor of the parent of S.

A common ancestor of two states S and T is a state in the tree that has S and T as descendants. All user-defined states have at least one common ancestor, namely Main. The lowest common ancestor (LCA) of two states S and T is the deepest state in the tree that has S and T as descendants. Since a state can be a descendant of itself, then if some state T is a descendant of another state S, then the lowest common ancester of S and T is S. For example, consider the following port state machine:

port P {
  …
  machine M {
    state A {
      state A1 {}
      state A2 {}
    }
    state B {}
  }
}

The following diagram provides a simple graphical representation of the state hierarchy of P’s state machine, starting with Main as the root:

In this example, Main is the LCA of states A and B, as well as for other pairs of states such as A1 and B. Similarly, A is the LCA of the following pairs of states: A and A1; A and A2; and A1 and A2.

State Transition Functions¶

State transitions are specified using the built-in state transition functions, which specify the target state and how to reach it. If an event handler calls one of these functions, then when it finishes, the state machine performs a state transition from the current state to the specified target state. Otherwise, the state machine remains in the current state.

There are four state transition functions, each defined in turn below.

function setNextState(target : State) : Nil ¶

Sets the value of the target state that the state machine will transition to upon exiting the current state. The state machine transitions to target by taking the shortest path from the current state via the lowest common ancestor.

If target is equal to the current state, then the state machine does not change state, and it does not exit or re-enter the current state. In contrast, if target is not equal to the current state, then the state machine will change state by exiting all of the states along the path of ancestors starting from the current state up to but excluding the lowest common ancestor, executing the corresponding state exit actions along the way. This is followed by entering all the states along the path of descendants from but not including the lowest common ancestor down to the state target and executing their state entry actions respectively.

function setNextState(target : State, commonAncestor : State) : Nil: Sets the value of the target state that the state machine will transition to upon exiting the current state, and specifies the common ancestor it must go through. This function only differs from the setNextState function with a single argument in that, in this case, the state machine will transition to the target state via the state commonAncestor instead of the default lowest common ancestor. If commonAncestor is in fact the lowest common ancestor, then the effect of this function is the same as calling setNextState(target).

function setNextStateReEnter(target : State) : Nil ¶

Sets the value of the target state that the state machine will transition to upon exiting the current state. It only differs from the setNextState function with a single argument in that the state machine does exit and re-enter the lowest common ancestor when it transitions to the target state.

Therefore, unlike setNextState(target), if target is equal to the current state, then the state machine will exit the current state executing the state exit actions, and re-enter the current state executing the state entry actions.

function setNextStateReEnter(target : State, commonAncestor : State) : Nil: Sets the value of the target state that the state machine will transition to upon exiting the current state, and specifies the common ancestor it must go through. It only differs from the setNextStateReEnter function with a single argument in that the state machine will transition to the target state via the state commonAncestor instead of the default lowest common ancestor state.

The following example illustrates the differences between these transition functions:

port P {
  function f1() : Nil
  function f2() : Nil
  function f3() : Nil
  function f4() : Nil
  function f5() : Nil

  machine {
    state S1 {
      // Stays in S1 without exiting or re-entering S1
      f1() = setNextState(S1)

      // Exits S1, and re-enters S1
      f2() = setNextStateReEnter(S1)

      // Stays in S1 without exiting or re-entering S1
      f3() = setNextState(S1, S1)

      // Exits S1, and re-enters S1
      f4() = setNextState(S1, Main)

      // Exits S1, and then enters S2 and S2.S3
      f5() = setNextState(S2.S3)
    }
    state S2 {
      state S3 {
        // Exits S3 and enters S4
        f1() = setNextState(S4)

        // Exits S3 and S2, and then enters S2 and S4
        f2() = setNextState(S4, Main)

        // Exits S3, S2 and Main, and then enters Main, S2 and S4
        f3() = setNextStateReEnter(S4, Main)
      }
      state S4 {
        // Exits S4 and S2, and then enters S2 and S3
        f4() = setNextStateReEnter(S3)
      }
    }
  }
}

The state transitions in this example are visualised in the following state diagram:

State transition functions can also be used in Parameterised States, where the instances of the parameterised states are treated as distinct states. Consider the following example:

port ToggleSwitch {
  function on() : Nil
  function off() : Nil
  outgoing signal toggled()

  machine {
    state S(isOn : Bool) {
      exit() = toggled()

      on() = setNextState(S(true))
      off() = setNextState(S(false))
    }
  }
}

The port ToggleSwitch has a simple state machine comprising one parameterised state S with parameter isOn of type Bool, which represents the status of the switch. The state can perform two function calls on() and off() to turn the switch on and off respectively, and an exit() function that sends a signal when the status of the switch changes. By default, the state machine starts in the instantiated state S(false) where it can perform either function call. When on() occurs, the state is changed to S(true), whereas off() does nothing. Similarly, in state S(true) when off() occurs, the state changes to S(false).

The state transition function used in both cases is setNextState, which means that if the target state is the same as the current state, then the state is not exited and re-entered, and therefore the exit() function is not executed. In this example, when the state machine is in state S(true) and performs the function on(), it remains in the same state, and therefore does not execute the exit() function. In contrast, when it performs the function off(), it changes state to S(false) and executes the exit() function, which emits the signal toggle(). This behaviour is mirrored in state S(false), where function on() causes a state change and the exit() function to be executed. So the signal toggle() is only emitted when the status of the switch changes, which is precisely the intention of this port specification.

This example illustrates how instances of parameterised states are treated as distinct states, and the impact they have when using the state transition functions.

The following port model has the same behaviour as ToggleSwitch above, but is defined without using parameterised states:

port ToggleSwitchLong {
  function on() : Nil
  function off() : Nil
  outgoing signal toggled()

  machine {
    state Off {
      on() = {
        toggled();
        setNextState(On);
      }
      off() = {}
    }
    state On {
      off() = {
        toggled();
        setNextState(Off);
      }
      on() = {}
    }
  }
}

Transitions¶

A transition specifies state machine behaviour in an event state. There are four types: An event transition, which specifies the behaviour resulting from an incoming function call or signal event; a spontaneous transition, which specifies the behaviour resulting from a spontaneous event; a timer transition, which specifies the behaviour resulting from a timer expiry event; and an unused transition, which is used to override the default termination behaviour.

declarationTransition¶

«transition» :=
  «event transition»
  | «spontaneous transition»
  | «timer transition»
  | «unused transition»

A transition is enabled precisely when the current state in which it is defined in an ancestor of the current state of the state machine, and it is either unguarded or has a guard which evaluates to true.

Event Transition¶

An event transition specifies the behaviour of a state machine resulting from an incoming event, referred to as a receive event, which is either a function call or signal. Component and port state machines can both receive incoming function calls, whereas only component state machines can receive incoming signals. These signal events are received from the component’s required ports asynchronously, and stored in its queue. The component state machine only reacts to a signal event when it is taken out of its queue.

declarationEvent Transition¶

[if («expression»)] «receive event» = «event handler»

where the expression is a guard on the transition. It must be a simple expression of type Bool, and is strictly side-effect free. If it evaluates to true, then the transition is enabled, otherwise it is disabled.

eventReceive Event¶

[«event source».]«identifier»(«parameters»)

where the event source specifies which port the event can be received from, as specified below.

Type annotations in the parameters of receive events are optional, providing it is unambiguous which one is being referred to. For example:

port P {
  function status(isDone : Bool) : Nil

  machine {
    status(x) = {
      …
    }
  }
}

In port state machines, non-verified types are not allowed anywhere except as parameters of event transitions. The only reason for this exception is that these parameters must precisely match their types specified in the corresponding function or signal declarations.

If a parameter in an event transition is a non-verified type, then the undefined expression (_) must be used as its parameter name. For example, consider the following function call:

checkData(_ : NonVerified<Int>) = {}

Similarly, in a port state machine, if the return type of an event transition is a non-verified type then the undefined expression (_) must be used as the return value. For example:

external type Data

port P {
  function getMessage() : Data

  machine {
    getMessage() = _
  }
}

An event source specifies which ports the events can be received from.

declarationEvent Source¶

«identifier»
| «event source» '[' «pattern» ']'
| «event source» '[' «pattern» '|' «expression» ']'

where the expression must be of type Bool, and strictly side-effect free.

In a port state machine, the event source is always the port itself, or one of its child ports. In a component state machine, the event source must be explicitly given for every event transition:

port P {
  function f() : Nil

  machine {
    f() = nil
  }
}

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

  machine {
    client.f() = source.f()
  }
}

Ports and components can declare arrays of ports:

port P3 {
  port P31 {
    function f31() : Int
  }

  val p31 : Array<P31, 2>

  machine {
    var x : Int

    state S1 {
      p31[0].f31() = {
        x = 6;
        return x;
      }
      p31[1].f31() = {
        x = 7;
        return x;
      }
    }
  }
}

In this example, the event source in the first transition in state S1 is p31[0], which denotes the array index of the port from which the event f31() is received. The two transitions in S1 can also be rewritten as follows:

p31[val p].f31() = { x = p + 6; return x; }

The constant p is assumed to be of type Int by default.

The following is an example of nested port arrays using direct array indexing to identify the event source:

port P3 {
  port P31 {
    function f31() : Nil
  }
  port P32 {
    val p31 : Array<P31, 2>
  }

  val p32 : Array<P32, 2>

  machine {
    function f2(p : Int, q : Int) : Nil = assert(p == q)

    p32[0].p31[0].f31() = f2(0, 0)
    p32[1].p31[1].f31() = f2(1, 1)
  }
}

In this example, transitions are specified for two of the four possible cases:

p32[0].p31[0].f31() = f2(0, 0)
p32[1].p31[1].f31() = f2(1, 1)

They can be written more succinctly as follow:

p32[val p].p31[val q | p == q].f31() = f2(p, q)

The expression p == q acts as a guard enabling the transition for events from p32[0].p31[0].f31() and p32[1].p31[1].f31().

See also

Array type.

Array subscript expression.

Event Handlers¶

An event handler specifies the actions that will be executed in response to an incoming event.

syntaxEvent Handler¶

«expression» | «illegal» | «offer»

Consider the following example, where the event handler is simply an expression:

port P {
  function f() : Nil
  outgoing signal sig()

  machine M {
    f() = sig()
  }
}

When function f() is called, the state machine of P emits signal sig().

handlerIllegal¶

illegal

The illegal handler specifies that an event is not allowed to occur. Consider the following example of a component state machine:

state S {
  client.f1() = illegal
  client.f2() = {}
  source.sig1() = client.sig1()
  source.sig2() = illegal
}

In state S, the function client.f1() and signal source.sig2() are illegal, which means that the component is not able to handle these events in this state.

handlerOffer¶

offer {
  «offer clauses»
  [otherwise «event handler»,]
}

«offer clause» := [if («expression»)] «event handler»,

The offer handler allows multiple cases to be specified resulting from an incoming event. An offer clause specifies a single case, which can either be an expression or illegal. It can be guarded by a simple expression of type Bool, and is strictly side-effect free. If the guard evaluates to true or is omitted, then the event handler is enabled; otherwise it is disabled.

If none of the offer clauses are enabled, then either the event handler on the otherwise clause will be executed, or in the absence of an otherwise clause, the transition is disabled in that state.

Consider the following example:

port P {
  function f(l : Bounded<0, 5>) : Nil
  outgoing signal low()
  outgoing signal medium()
  outgoing signal high()

  machine {
    f(level : Bounded<0, 5>) = offer {
      if (level < 2) low(),
      if (level > 3) high(),
      otherwise medium(),
    }
  }
}

When function f(level) is called, then P will emit one of the signals low(), medium() or high(), depending on the value of level. If level is 0 or 1, then only the first offer clause is enabled; if it is 4 or 5 then only the second offer clause is enabled; and if it is 2 or 3, then both of the offer clauses are disabled and the otherwise clause is executed.

Consider the following example of an event transition:

f1(p : Bool, q : Bool) = offer {
  if (p && q) setNextState(Terminated),
}

This transition can only be expressed using the offer handler, because the guard expression uses the parameters of the transition’s incoming event f1(p : Bool, q : Bool).

Note

A port state machine can have multiple offer clauses enabled; in this case, the offer clause is chosen nondeterministically. In contrast, a component state machine is not allowed to have multiple offer clauses enabled. If it does, then this would be caught as a dynamic error.

Offer versus Nondet¶

Although offer and nondet have some similarities when a nondet is used as an event handler, there are some key differences between them.

Unlike offer, a nondet is an expression, and can therefore be used much more widely than event handlers. Its purpose is to allow users to explicitly express nondeterministic behaviour in a concise way within specification contexts, such as port declarations, and external functions, which are used for verification purposes only, and from which no code is generated. Nondet expressions cannot be used in implementation contexts, such as component declarations. It is a dynamic error for a nondet expression to have no enabled clauses, and no otherwise expression.

In contrast, an offer is an event handler, and not an expression, which means that it can only be used as a handler for specifying the actions that will be executed in response to an incoming event (i.e. function call or signal). An offer can be used in ports and components. If an offer has no enabled clauses, and no otherwise expression specified, then it results in the transition being disabled in that state. This is particularly useful in hierarchical state machines when declaring transitions at different levels of the state hierarchy, as illustrated in the following example:

port P1 {
  function doSomething(status : Bool) : Nil
  outgoing signal update()
  outgoing signal inactive()

  machine {
    doSomething(_) = inactive()

    state On {
      doSomething(status) = offer {
        if (status) update(),
      }
    }
  }
}

In this example, a transition is declared at the top level in Main for the function doSomething(_), and will fire in any of its child states that do not have an enabled transitions for this function. In this case, the only such state is On, where the transition for doSomething(status) results in an offer with a single guarded clause. If status evaluates to true, then the offer clause is executed and the signal update() is sent. In contrast, if status evaluates to false, then this transition disabled, and the transition for doSomething(_) declared in its parent state Main will be executed in On instead, resulting in the sending of the signal inactive():

The offer handler in state On cannot be replaced with a nondet expression, as this has a different meaning in the case where the guard is false:

  machine {
    doSomething(_) = inactive()

    state On {
      doSomething(status) = nondet {
        if (status) update(),
      }
    }
  }

In this example, when status evaluates to true, then the only nondet clause will be executed, thereby sending the signal update(), as is also the case when using offer in P1 above. Where their respective behaviour differs from one another is when status evaluates to false resulting in no enabled clauses. Unlike P1 where the transition for doSomething(false) declared in On is disabled, P2 will result in a runtime error during verification, as illustrated by the following counterexample:

Spontaneous Transition¶

A spontaneous transition specifies the behaviour resulting from a spontaneous event in a port state machine. They are used to model actions that can occur by a component that implements the port, but are not visible across the component boundary that the port is specifying. An idle port can nondeterministically choose to fire an enabled spontaneous transition at any time without any external input, and components using the port have to be able to handle all consequences thereof.

declarationSpontaneous Transition¶

[if («expression»)] spontaneous = «expression»

A spontaneous transition can be guarded by a simple expression of type Bool. If the guard evaluates to true, then the transition is enabled, otherwise it is disabled. The guard must be side-effect free.

Consider the following example:

port P1 {
  function begin() : Nil
  outgoing signal done()

  machine {
    state Idle {
      begin() = setNextState(Started)
    }
    state Started {
      spontaneous = {
        done();
        setNextState(Idle);
      }
    }
  }
}

In state Started, P1 will always perform the spontaneous transition resulting in the signal done() being emitted, and a state change to Idle.

A state can have multiple spontaneous transitions, for example:

port P2 {
  function begin() : Nil
  outgoing signal done()
  outgoing signal error()

  machine {
    state Idle {
      begin() = setNextState(Started)
    }
    state Started {
      spontaneous = {
        done();
        setNextState(Idle);
      }
      spontaneous = {
        error();
        setNextState(Terminated);
      }
    }
  }
}

In state Started, P2 will always execute one of the spontaneous transitions, the choice of which is nondeterministic. This means that a component using this port can depend on receiving one of the resulting signals, namely done() or error(), but it cannot control or determine which one it will receive. Therefore, a component using this port must be able to handle both cases.

A state can have a combination of event transitions and spontaneous transitions enabled, for example:

port P3 {
  function begin() : Nil
  function stop() : Nil
  outgoing signal done()
  outgoing signal error()

  machine {
    state Idle {
      begin() = setNextState(Started)
    }
    state Started {
      spontaneous = nondet {
        {
          done();
          setNextState(Idle);
        },
        {
          error();
          setNextState(Terminated);
        },
      }
      stop() = setNextState(Idle)
    }
  }
}

In state Started, P3 can either execute the spontaneous transition, or execute the function stop(). If the spontaneous transition is executed, then it will send a signal, and move to a different state where stop() is illegal. P3 can nondeterministically decide to fire the spontaneous transition at any time, and therefore a component using this port is not guaranteed to be able to call stop(), because it cannot determine when P3 is in state Started.

Optimizing How Spontaneous Transitions Are Handled¶

A spontaneous transition can either: send signals directly within the transition itself; send signals indirectly, for example by transitioning to a state with an entry function that sends a signal, or calling a function that sends a signal; or not result in the sending of signals at all.

In the case where a spontaneous transition results in the sending of a signal directly within the transition itself, Coco is able to perform certain optimizations during the verification. Specifically, Coco is able to automatically assume that these spontaneous transitions will eventually fire without the user having to label them with the @eventually attribute.

For spontaneous transitions that do not send any signals, Coco is not able to soundly make this assumption for certain classes of verification properties. For spontaneous transitions that send signals indirectly, Coco cannot always statically determine whether they result in actually sending signals or not, and therefore cannot always apply this optimization either. In these latter two cases, Coco may require users to annotate spontaneous transitions with @eventually, which would be raised during the verification. For example, if a component is dependent upon a spontaneous transition eventually firing in one of its required ports in order to pass one of its verification assertions, but Coco is not able to automatically assume this, then that assertion will fail. Assuming that the user’s intention is for the spontaneous transition to eventually fire, then they can specify this by labelling it with @eventually. Further details and examples of this can be found in the verification section.

When specifying a spontaneous transition that results in the sending of signals, and there is little or no common code that needs to be factored out involving these signals, then the recommended approach is to send the signals directly within the transition itself in order to exploit the optimization summarised above. The following series of port declarations illustrate how a spontaneous transition can send signals indirectly versus directly:

port SignalInEntry {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal ready()

  machine {
    state Init {
      begin() = setNextState(Starting)
    }
    state Starting {
      spontaneous = setNextState(Running)
    }
    state Running {
      entry() = ready()

      doSomething() = {}
    }
  }
}

When the spontaneous transition in the state Starting fires, the state machine transitions to Running and sends the signal ready() upon entry. Although the execution of the spontaneous transition results in the sending of ready(), it does so indirectly by executing the entry function in Running.

The following variation of the port declaration illustrates another way a signal can be sent indirectly:

port SignalInFunction {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal ready()

  machine {
    function doAction(sig : Signal, target : State) : Nil = {
      send(sig);
      setNextState(target);
    }

    state Init {
      begin() = setNextState(Starting)
    }
    state Starting {
      spontaneous = doAction(SignalInFunction.ready(), Running)
    }
    state Running {
      doSomething() = {}
    }
  }
}

In this example, when the spontaneous transition is executed, it will call the function doAction(…) which results in the sending of ready() indirectly.

In contrast, the following port has the same behaviour as the two ports above, but sends the ready() signal directly within the spontaneous transition instead:

port SignalInTransition {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal ready()

  machine {
    state Init {
      begin() = setNextState(Starting)
    }
    state Starting {
      spontaneous = {
        ready();
        setNextState(Running);
      }
    }
    state Running {
      doSomething() = {}
    }
  }
}

This is the recommended pattern to follow in this instance, as there is no advantage to be gained from factoring out the sending of ready() in this case, and it allows Coco to optimize the way it performs the verification without requiring users to explicitly label the spontaneous transition with @eventually.

Unreliable Attribute¶

A spontaneous transition can be annotated with the special attribute @unreliable, or a variant thereof with a parameter that is a simple expression of type Bool. If the parameter evaluates to true, then the attribute is applied to the corresponding transition, otherwise it has no effect.

When a spontaneous transition is labelled with @unreliable, then this means that it may or may not ever fire. This attribute is useful in a number of different modelling scenarios, for example, in a port state machine that is modelling potential error signals coming from some underlying piece of hardware. In this case, the errors might or might not occur, so a component using this port has to be able to handle these signals but cannot depend upon them occurring.

Consider the following example:

port P1 {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
      @unreliable
      spontaneous = error()
    }
  }
}

In states S(true) and S(false), the port might or might not execute the spontaneous transition, the choice of which is nondeterministic. Therefore, a component requiring this port cannot depend on the signal being sent, even in the event that no function calls are made.

The @unreliable attribute can also have a parameter of type Bool. In a given state, when the parameter evaluates to true, then the corresponding spontaneous transition is unreliable; otherwise, it is treated as a normal spontaneous transition without the @unreliable attribute:

port P2 {
  function on() : Nil
  function off() : Nil
  outgoing signal update()

  machine {
    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
      @unreliable(!isOn)
      spontaneous = update()
    }
  }
}

In state S(true) the value of the @unreliable parameter is false and therefore it is not applied to the corresponding spontaneous transition. In contrast, in state S(false) the value of the @unreliable parameter is true and therefore the corresponding spontaneous transition is unreliable.

A state can have multiple unreliable spontaneous transitions, for example:

port P3 {
  function on() : Nil
  function off() : Nil
  outgoing signal update()
  outgoing signal error()

  machine {
    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
      @unreliable
      spontaneous = update()
      @unreliable
      spontaneous = error()
    }
  }
}

In states S(true) and S(false), all of the spontaneous transitions are unreliable. Therefore, component requiring this port might receive the signals update(), error(), or no signals at all, even if no function calls are made.

A state can also have multiple spontaneous transitions, where a subset of them are annotated with the @unreliable attribute, for example:

port P4 {
  outgoing signal update()
  outgoing signal error()

  machine {
    state S {
      spontaneous = update()
      @unreliable
      spontaneous = error()
    }
  }
}

In state S, there are two spontaneous transitions where one of them is labelled as unreliable. In this case, one of the spontaneous transitions will fire, the choice of which is nondeterministic. A component using this port can depend on receiving one of the resulting signals, either update() or error(), but it cannot determine which one it will receive, and therefore must be able to handle both cases.

Note

A state in which multiple spontaneous transitions are enabled where a proper subset of them are annotated with the @unreliable attribute is equivalent to the case where none of the spontaneous transitions are annotated with the @unreliable attribute.

Unbounded Attribute¶

When building port models, there are cases where signals have to be modelled as being unbounded in order to accurately reflect the components implementing them. If the component receiving them only has a bounded queue of a fixed size, then these signals will fill up the queue and trigger a dynamic error during verification indicating a queue overflow error.

To handle these unbounded signals, Coco has a special attribute called @unbounded, which can be used to label a spontaneous transitions that send signals. This means that the verification will explore all possible scenarios including the case where the spontaneous transition can fire an arbitrary but finite number of times in succession, thereby sending an arbitrary but finite number of signals. When verifying a component that has a required port with an @unbounded attribute, if the verification passes then this means that the component is correct for an arbitrary but finite number of signals sent by that required port.

Consider the following example of a simple port, comprising a spontaneous transition that is labelled with the @unbounded attribute:

port P {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    @unbounded
    spontaneous = error()

    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
    }
  }
}

This port can receive alternate on() and off() calls, starting with on(), and can spontaneously send an arbitrary number of error() signals in any state. Without the @unbounded attribute, a component using this port would have to restrict the number of error() signals in its queue (for example, by using the setUnique function), otherwise the verification would fail with a queue full error. If such restrictions are applied solely for the purpose of making the components verifiable, but do not reflect the actual behaviour of the system, then the verification would be unsound. In contrast, with the @unbounded attribute, a component using this port can be verified in a sound way without such restrictions on the signals.

There is also a parameterised variant of the unbounded(p) attribute, where p is a simple expression of type Bool. If p evaluates to true, then the corresponding spontaneous transition is guaranteed to eventually occur, and is equivalent to annotating the transition with @eventually and @unbounded. For example, the following two ports P1 and P2 are equivalent:

port P1 {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    @unbounded(true)
    spontaneous = error()

    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
    }
  }
}

port P2 {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    @eventually
    @unbounded
    spontaneous = error()

    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
    }
  }
}

In both P1 and P2, the spontaneous transition resulting in the error() signal is guaranteed to eventually occur.

In contrast, if p in the unbounded(p) attribute evaluates to false, then the corresponding transition is not guaranteed to occur, and is equivalent to annotating the transition with @unreliable and @unbounded. For example, the following two ports P3 and P4 are equivalent:

port P3 {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    @unbounded(false)
    spontaneous = error()

    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
    }
  }
}

port P4 {
  function on() : Nil
  function off() : Nil
  outgoing signal error()

  machine {
    @unreliable
    @unbounded
    spontaneous = error()

    state S(isOn : Bool) {
      if (!isOn) on() = setNextState(S(true))
      if (isOn) off() = setNextState(S(false))
    }
  }
}

In both P3 and P4, the spontaneous transition resulting in the error() signal may or may not occur, the choice of which is nondeterministic.

There are some restrictions when using the @unbounded attribute. Specifically, a spontaneous transition can be labelled with @unbounded only if it:

Is defined at the top-most level of the port state machine in Main;
Is unguarded;
Results in sending precisely one signal event;
Cannot read from any variable that is written to by a non-@unbounded action; and
Does not call any of the state transition functions.

Further, a state machine that has any transitions labelled with @unbounded cannot make any calls to setNextState(Terminated). For example, the following port:

port P {
  function f() : Nil
  outgoing signal sigA()

  machine M {
    @unbounded
    spontaneous = sigA()

    f() = setNextState(Terminated)
  }
}

fails the verification with the following counterexample:

Components that use ports with unbounded spontaneous transitions also have certain restrictions on how they can use them. See Queues section for further details.

Slow Attribute¶

When verifying a component with a required port P, the verification explores all possible interleavings between them. If P has a spontaneous transition, then the verification will consider all scenarios where the spontaneous transition can fire. The verification assumes that a spontaneous transition can happen very quickly and very slowly, which means that it will explore the case where the spontaneous transition occurs so quickly that the component is never able to become idle (and is therefore unresponsive). This may reflect a genuine liveness error, or it may reflect the fact that the assumption that the spontaneous transition may occur so quickly is not correct. In the latter case, this assumption can cause the component to incorrectly fail the responsiveness check. This problem only arises in the multi-threaded runtime, since the single-threaded runtime only allows spontaneous transitions to fire when the component is idle.

To express the fact that a spontaneous transition will not occur too fast, it can be labelled with the attribute @slow. When verifying a component with a required port P, the verification will assume that if infinitely many that has @slow spontaneous transitions can occur in P, then an infinite number of them will occur when the component is idle. This means that the verification will ignore certain infinite loops, for example when verifying whether the component is responsive, the verification will not consider infinite loops where @slow spontaneous transitions always happen when the component is busy.

Consider the following example of a port that can repeatedly send the signal update():

port FastP2 {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal update()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      doSomething() = {}
      spontaneous = update()
    }
  }
}

In state Running, FastP2 can execute the spontaneous transition resulting in the sending of the signal update(). This port can choose to perform an infinite sequence of this spontaneous transition infinitely quickly, which may cause a component using FastP2 to become unresponsive as illustrated in the following example:

@queue(1)
@runtime(.MultiThreaded)
component C {
  val client : Provided<P1>
  val r : Required<FastP2>

  init() = {
    setUnique(r, FastP2.update);
  }

  machine {
    state Idle {
      client.begin() = {
        r.begin();
        setNextState(Running);
      }
    }
    state Running {
      client.doSomething() = r.doSomething()
      r.update() = client.update()
    }
  }
}

Component C uses FastP2 as its required port, and uses the queue control function setUnique to manage the unbounded flow of update() signals it can receive. When it receives an error signal from its required port instance r, the component sends the corresponding signal to its client.

When verifying C, it fails the responsiveness check with the following counterexample:

Even though C’s queue is restricted to only having one instance of update() in its queue, this counterexample illustrates how r can repeatedly send another update() signal immediately after C has taken the current instance out of its queue, and before it has finished processing the corresponding transition. This means that FastC is not able to process any function calls, and is therefore unresponsive.

In this example, it may be reasonable to assume that the underlying implementation corresponding to the spontaneous transition in FastP2 would not repeatedly send update() signals so quickly that it would cause C to become unresponsive in the way illustrated above. The following port is a version of FastP2 where the spontaneous transition is labelled with @slow:

port SlowP2 {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal update()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      doSomething() = {}
      @slow
      spontaneous = update()
    }
  }
}

Component C verifies correctly when using SlowP2 as its required port instead of FastP2. The verification still explores most of the scenarios where the @slow spontaneous is fired for the responsive check. The only counterexample that is ignored is where every @slow spontaneous transition occurs when the component is busy.

The @slow attribute can be used in combination with the other attributes applicable to spontaneous transitions, such as @unreliable and @eventually. The following port extends SlowP2, and provides an example of applying @slow and @eventually on the same spontaneous transition:

port SlowEventuallyP2 {
  function begin() : Nil
  function doSomething() : Nil
  outgoing signal update()
  outgoing signal error()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      doSomething() = {}
      @slow
      spontaneous = nondet {
        @eventually
        update(),
        error(),
      }
    }
  }
}

This port extends SlowP2 by declaring an additional signal called error(), and amending the spontaneous transition in Running so that it results in the nondeterministic choice between sending update() or error(). The spontaneous transition is still labelled with @slow. Further, the first nondet clause, which sends the signal update(), is labelled with the @eventually attribute to denote the fact that this signal must eventually be sent. See Example 1: Component fails to send a signal in the Verification section for a more detailed example of this combination of attributes being used, and the implications it has on components implementing their provided ports.

Note

The recommended approach is not to label spontaneous transitions with the @slow attribute by default, in order to avoid accidentally making assumptions on the underlying implementation that are unnecessary or invalid.

When verifying a component with a required port that has @slow spontaneous transitions, the verification will not consider infinite loops where @slow spontaneous transitions always occur when the component is busy, and assumes that the component will become idle often. When the software implementing the port is not built and verified using Coco, then the user must ensure that the software does satisfy the @slow assumptions specified above, otherwise the verification results will not be valid. This is illustrated in the two example ports FastP2 and SlowP2 above, where the component is responsive when using SlowP2, but fails the responsive check when using FastP2.

An example of where these assumptions are unlikely to hold is where a component does a lot of blocking operations on one of its required ports that take a long time, and prevents the component from becoming idle often. This increases the likelihood that the underlying implementation of any of the required ports with @slow spontaneous transitions will only be able to perform these transitions faster than the duration of the blocking operations, thereby leading to a genuine responsiveness error at runtime. In this case, it would not be safe for such a component to use ports with @slow spontaneous transitions, as the verification would ignore this error.

Components that are more likely to be able to use ports with the @slow attribute safely are those that follow the pattern of only performing non-blocking operations, and receiving the results from these operations via asynchronous notifications. This pattern typically means that the components are idle sufficiently often that it is safe for the verification to assume that if infinitely many @slow spontaneous transitions can occur, then an infinite number of them will occur when the component is idle.

Timer Transition¶

A timer transition specifies the behaviour resulting from a timer, and is only permitted in component state machines.

declarationTimer Transition¶

«timer event» = «expression»

where the expression specifies the actions resulting from the timer event, and must be a simple expression.

eventTimer Event¶

after | periodic («expression»)

where the expression is of type Duration, and specifies the time interval after which the timer event will executed. The expression must be side-effect free.

There are two types of timer events, namely:

after specifies that if the timer event can be executed, then it will do so once after the specified duration has passed.

periodic specifies that the timer event will occur repeatedly each time the specified duration has passed while it is able to do so.

Timer events are never allowed to be guarded.

Consider the following example of a simple component with an after timer transition:

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

  machine {
    state Off {
      client.begin() = setNextState(On)
    }
    state On {
      after(seconds(1)) = client.status()
      client.stop() = setNextState(Off)
    }
  }
}

In state On, either function stop() occurs before the timer elapses changing the state to Off, or the timer transition fires and the signal status() is sent.

In contrast, consider the following example of a component with a periodic timer transition:

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

  machine {
    state Off {
      client.begin() = setNextState(On)
    }
    state On {
      periodic(seconds(1)) = client.status()
      client.stop() = setNextState(Off)
    }
  }
}

In state On, either function stop() is called before the periodic transition fires, or the periodic transition fires one or more times (every second) sending the signal status() each time, and remaining in the same state.

A component state machine can also combine both types of timers:

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

  machine {
    after(seconds(1)) = client.sig1()
    periodic(seconds(1)) = client.sig2()
  }
}

In state Main, the after timer transition can fire once after 1 second, whereas the periodic timer transition can fire repeatedly every second.

The expressions passed as arguments to after and periodic are of type Duration, and must be side-effect free. This means that if the expression is a dynamic timer duration determined by a call to a required port, then the corresponding function declaration in that port must be labelled as being side-effect free, as illustrated by the following example:

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

  machine {
    periodic(source.computeDuration()) = client.sig2()
  }
}

In this example, the duration for the periodic timer in component C is dynamically computed by calling the function computeDuration() on its required port source. For this to be valid, the function declaration for computeDuration() must be labelled with @noSideEffects in the corresponding port declaration as follows:

port Source {
  @noSideEffects
  function computeDuration() : Duration

  machine {
    // ...
  }
}

Verification Assumptions and Limitations¶

Coco performs untimed verification, which means that although it explores all possible interleavings and orderings of transitions (including timer transitions), it does not verify anything about the actual values of the time intervals given as arguments to the after or periodic timer events. As per the syntax definition for timer transition above, these arguments are expressions that evaluate to values of type Duration, which is not a verifiable type. This type is mapped to the corresponding primitives in the generated code, where the actual values can be used in the normal way.

Consider the following example of a component state machine with two timer transitions:

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

  machine {
    after(seconds(1)) = p.sigA()
    after(seconds(10)) = p.sigB()
  }
}

The first timer transition expires after 1 second resulting in the sending of signal sigA(), and the second timer transition expires after 10 seconds resulting in the sending of signal sigB(). During verification, these two timer transitions are indistinguishable, because the time intervals are not verified. The verification will therefore explore both orderings, as illustrated by the following two valid sequences of C1:

Although the values of type Duration are not verifiable, the verification does assume that the time intervals specified in timer transitions do not expire instantly. As a result, the verification treats timer expiry events like slow transitions, and therefore similar assumptions that apply when using the @slow attribute must also hold for timer expiry events. Specifically, if infinitely many timer expiry events can occur in a component, then an infinite number of them will occur when the component is idle. This refers specifically to the occurrence of timer expiry events, not when the corresponding timer transitions fire.

Note

Users are responsible for ensuring that the systems they build in Coco satisfy this assumption, since the verification always assumes that they do, and is not able to detect cases where they do not. The verification ignores certain infinite loops, for example when verifying whether a component is responsive, it will not consider infinite loops where the timer expiry events always occur when the component is busy. If this assumption does not hold, then the verification results are not guaranteed to be valid.

The fact that timers are verified in a non-verified way has some interesting consequences, as illustrated by the following example:

external function sleep(d : Duration) : Nil = {}

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

  machine {
    state Init {
      client.fn() = setNextState(Active.DoOperation)
    }
    state Active {
      client.fn() = {}
      periodic(milliseconds(1)) = setNextState(DoOperation)

      execution state DoOperation {
        sleep(hours(1));
        setNextState(Active);
      }
    }
  }
}

The component C1 passes the verification assertions, but the generated code for C1 leads to a responsiveness error. Following a call on fn(), C1 transitions to the execution state Active.DoOperation, where a new timer interval is started for the periodic timer, and the function sleep(hours(1)) is executed. In the generated code, the timer in Active has a timer interval of 1 second, and is therefore guaranteed to expire before C1 completes the sleep(hours(1)) operation, and moves to Active. Processing expiry timer events takes priority over incoming function calls, and therefore the timer transition will be immediately executed upon entry to this state. This results in C1 moving to the state DoOperation, starting a new timer interval, and repeating the cycle again. C1 is unresponsive, because it never becomes idle, and therefore cannot process any incoming function calls.

This problem arises because the assumption that if infinitely many timer expiry events can occur in a component, then an infinite number of them will occur when the component is idle, does not hold in this example: The timer intervals in the function sleep() and the periodic timer transition is such that C1 is only able to perform the timer expiry events when the component is busy, and is never able to become idle. As a result, the verification results are not valid.

Similar to the patterns discussed in the Slow Attribute section, a pattern where this assumption is likely to be violated is when there are cyclic dependencies between timer transitions and blocking operations, where the timers expire before the operations depending on these timeouts have completed (as illustrated in the example of component C1 above).

Timers with expiry time intervals of zero should also be used with caution. If infinitely many of them can occur in a component state machine, then they will occur instantly thereby preventing the component from becoming idle. Given that they happen instantly, it will not be the case they can also happen infinitely often after the component becomes idle, and therefore breaks the assumption required to guarantee that the verification is valid. Similar caution should be taken when building components with timers that have a non-zero but nonetheless very short time intervals that can occur infinitely often, to ensure that the timers are also able to expire infinitely often when the component is idle.

Note

A component with timers that always expire at a point when the component is not idle is a dangerous case that risks violating the assumptions made by the verification, for example in the event that an infinite number of them can occur.

See also

@slow attribute.

Dispatching Events in a Component State Machine.

Unused Transition¶

declarationUnused Transition¶

unused() = «expression»

The event unused() is a special builtin event, which is used to override the default termination behaviour in components only, and allows termination to be deferred. This may be necessary, for example, when a component can be called to terminate in the middle of performing a series of operations, and instead of immediately terminating by default, the component may need to complete these operations before transitioning to the Terminated state.

If a component state machine has an unused transition declaration, then the verification will verify that following the unused call, the component is guaranteed to eventually terminate. Details and examples of this can be found in the Termination Responsiveness section.

The following component is an example of one that uses unused transitions in an attempt to ensure that its array of required ports finish their actions before it terminates:

port POperation {
  function execute() : Nil
  outgoing signal finished()

  machine {
    state Idle {
      execute() = setNextState(Running)
    }
    state Running {
      spontaneous = {
        finished();
        setNextState(Idle);
      }
    }
  }
}

@queue(2)
@runtime(.MultiThreaded)
component C {
  val client : Provided<POperation>
  val source : Array<Required<POperation>, 2>

  machine {
    state Idle {
      client.execute() = {
        source[0].execute();
        source[1].execute();
        setNextState(Running);
      }
    }
    state Running {
      var shouldTerm : Bool
      var waitingFor : Bounded<0, 2> = .Last

      source[_].finished() = {
        waitingFor = waitingFor - 1;
        if (waitingFor == 0) {
          client.finished();
          setNextState(if (shouldTerm) Idle else Idle);
        }
      }
      unused() = {
        shouldTerm = true;
      }
    }
  }
}

In this example, when execute() is called on C, it calls execute() on each required port in its array, and moves to the state Running. In Running, C waits for the signal finished() from each of them, after which it sends the signal finished() to its client, and returns to the state Idle.

In state Running, the C declares an unused transition that sets the value of shouldTerm to true. This variable is used to determine when C should terminate once it has received the finish() signals from all of its required ports.

The verification checks whether C does eventually terminate following a call to unused(). In this case, it fails with the following counterexample:

This counterexample illustrates how unused() is called when C is in state Running. Following this call, C receives the final finished() signal it was waiting for from its array of required ports, after which it correctly sends finished() to its client, but incorrectly returns to the Idle state instead of Terminated. As a result, C is deadlocked, because it is not able to receive any more function calls (reflecting the fact that it no longer has any clients).

This error is caused by the fact that in state Running, the target state in the setNextState function in the event handler of source[_].finished() is always Idle, regardless of the value of shouldTerm. When this is corrected to be:

setNextState(if (shouldTerm) Terminated else Idle);

then C is guaranteed to eventually terminate following a call to unused().

See also

Termination section for details about Coco’s default termination behaviour.

Termination Responsiveness section for details and examples of the verification performed on components with unused transitions.

Terminated State section.

Eventually Attribute¶

Coco has a special attribute called @eventually, which can be used to label certain transitions and branches in a port state machine to specify that they will eventually occur. There are also two parameterised variants of this attribute. The first, written as eventually(p), where p is an expression of type Bool, means that if p evaluates to true, then the attribute is applied to the corresponding transition or branch, otherwise it has no effect. The second variant extends this with an additional parameter, written as eventually(p, assumption), where assumption is of the special type EventuallyAssumption, and is used in combination with the @satisfiesEventually attribute to allow eventually assumptions to span across multiple transitions that are labelled with the same assumption value.

When a transition T is labelled with @eventually in some state S of a state machine, then the state machine incurs the following obligation upon entering S: if T is offered infinitely often, then T will happen infinitely often (i.e. T will eventually occur). In the simple case where T is labelled with the variants @eventually or @eventually(p), where p evaluates to true, then the obligation is satisfied by the occurrence of T only. In the general case where T is labelled with the variant @eventually(p, assumption), then the obligation incurred upon entry of S is satisfied by the occurrence of any transition labelled by an @eventually or a @satisfiesEventually attribute that has the value assumption as its argument. In contrast, labelling a transition T with @satisfiesEventually(a) does not create an obligation; instead the occurrence of T simply fulfils the obligation incurred by an @eventually attribute with the argument a.

Components with provided ports that use @eventually must satisfy these eventually constraints. Coco verifies this as part of verifying whether a component implements its provided ports correctly. Components with required ports that use @eventually on transitions can rely on them eventually occurring. Examples can be found in the Component Implements Its Provided Ports section.

The @eventually and @satisfiesEventually attributes can be applied to spontaneous transitions, individual clauses of a nondet expression, individual clauses of an offer, and the argument of an optional. In addition, the @satisfiesEventually attribute can also be applied to event transitions for function calls, which allows users to specify properties such as a transition will eventually occur unless a function call has occurred. Unlike spontaneous transitions, ports do not make any assumptions about whether a function is called or not, as its occurrence is entirely dependent upon the calling component.

The @eventually attribute cannot be used in combination with the @unreliable attribute, or anywhere in a component state machine.

The eventually property is intended to be an event-based property: it is intended to be used to specify that a certain event (for example, a signal) will eventually occur, and should therefore be used in conjunction with events. The verification then checks that the component satisfies this property, by checking that the event is guaranteed to eventually occur in the component implementation.

The rest of this section provides an overview of how the different variants of the @eventually attribute can be used in different contexts, together with a series of examples.

See also

The @satisfiesEventually attribute can be used in combination with @eventually to allow the eventually assumptions to span across multiple transitions.

Note

The eventually property is one that applies specifically over infinite traces. This means that it is only meaningful to label a branch or transition with the eventually attribute if there exists at least one infinite path where that eventually branch or transition can fire infinitely often. Consider the following example of a simple port state machine:

port P {
  function begin() : Nil
  outgoing signal done()

  machine {
    begin() = {
      optional @eventually done();
      setNextState(Terminated);
    }
  }
}

Labelling the optional signal in P with the eventually attribute is not a meaningful specification, and does not mean that the signal done() will eventually occur, because there does not exist a path where the eventually branch can be fired infinitely often. Therefore, a component that transitions to the Terminated state when it receives a call on begin() without ever sending this signal will be a valid implementation of P.

On Spontaneous Transitions¶

When a spontaneous transition is labelled with the @eventually attribute, if the spontaneous transition is enabled infinitely often, then it will eventually be executed.

Consider the following example of a simple port P with two spontaneous transitions, neither of which is labelled by the @eventually attribute:

port P1 {
  outgoing signal fail()
  outgoing signal ok()

  machine {
    spontaneous = fail()
    spontaneous = ok()
  }
}

Port P will execute one of the spontaneous transitions, the choice of which is nondeterministic. A component using this port can depend on receiving one of the resulting signals, namely fail() or ok(), but it cannot determine which one it will receive. A component implementing this port must be able to offer at least one of these signals, but it does not have to offer both. So a component that is only able to offer fail() signals, or a component that is only able to offer ok() signals are both valid implementations of this port. See Component Implements Its Provided Ports section for details about the verification checks that are carried out to verify whether a component correctly implements all of its provided ports.

Now consider the same port example, but where one of the spontaneous transitions is labelled with the @eventually attribute:

port P2 {
  outgoing signal fail()
  outgoing signal ok()

  machine {
    spontaneous = fail()
    @eventually
    spontaneous = ok()
  }
}

The spontaneous transition labelled with @eventually is enabled infinitely often, and therefore will eventually occur. In contrast with the previous example, where neither spontaneous transition is labelled with @eventually, a component using this port may rely on the signal ok() eventually being sent, which may occur after an arbitrary but finite number of fail() signals have been sent. Further, a component implementing this port must satisfy the eventually constraints and guarantee that the ok() signal is sent. A component that is only able to send fail() signals, or a component that can send either fail() or ok() signals without guaranteeing to send the ok() signal is not a valid implementation of this port.

A state in a port state machine can have multiple spontaneous transitions labelled with the @eventually attribute:

port P3 {
  outgoing signal fail()
  outgoing signal ok()
  outgoing signal update()

  machine {
    spontaneous = fail()
    @eventually
    spontaneous = ok()
    @eventually
    spontaneous = update()
  }
}

In this case, the signals ok() and update() will both eventually occur.

Note

The difference between a spontaneous event labelled with the @eventually attribute versus without is subtle yet fundamental. When the @eventually attribute is used in a port, then this places a requirement on the component implementing this port that these eventually constraints are satisfied. This is checked by the verification, and examples can be found in the verification section.

On Nondet and Offer Expressions¶

The @eventually attribute can be applied to individual clauses of a nondet or an offer expression.

Consider the following example, where the @eventually attribute is used on the branch of a nondet expression:

port P4 {
  function f1() : Nil
  outgoing signal fail()
  outgoing signal ok()

  machine {
    f1() = nondet {
      fail(),
      @eventually
      ok(),
    }
  }
}

If the function f1() is called infinitely often, then P4 will eventually send signal ok().

The following example is equivalent to the previous example, but applies the @eventually attribute on the branch of an offer:

port P5 {
  function f1() : Nil
  outgoing signal fail()
  outgoing signal ok()

  machine {
    f1() = offer {
      fail(),
      @eventually
      ok(),
    }
  }
}

The following two example states look very similar, but in fact provide different eventually guarantees:

port P6 {
  outgoing signal fail()
  outgoing signal ok()
  outgoing signal update()

  machine {
    spontaneous = fail()
    @eventually
    spontaneous = ok()
    spontaneous = update()
  }
}

port P7 {
  outgoing signal fail()
  outgoing signal ok()
  outgoing signal update()

  machine {
    spontaneous = nondet {
      fail(),
      @eventually
      ok(),
    }
    spontaneous = update()
  }
}

In port P6, the spontaneous transition labelled with the @eventually attribute resulting in the signal ok() is guaranteed to eventually occur. In contrast, in port P7, the first spontaneous transition results in a nondet expression where the branch that performs the signal ok() is labelled with the @eventually attribute. However, the first spontaneous transition is not guaranteed to occur, because there is another spontaneous transition in the same state, and the choice of which one fires is decided nondeterministically. Therefore, the nondet expression in the first spontaneous transition is not guaranteed to be executed, and in turn, this means that the ok() signal is not guaranteed either.

On Optional Expressions¶

The @eventually attribute can be applied to the argument of an optional expression. What this means depends on whether the argument to optional is a nondet expression, or not.

If the optional argument is not a nondet expression, then:

optional @eventually «expression»

is semantically equivalent to:

nondet { @eventually «expression» , {} }

In contrast, if the optional argument is a nondet expression, then:

optional @eventually nondet {
  «nondet clauses»
}

is semantically equivalent to:

nondet {
  «nondet clauses» , {}
}

«nondet clause» := @eventually [if («expression»)] «expression»;

This means that the @eventually attribute is applied to every nondet clause in the nondet expression, with the exception of the added clause {}.

For example, the expression:

optional @eventually nondet { e1, e2, e3, }

is semantically equivalent to:

nondet {
  @eventually e1,
  @eventually e2,
  @eventually e3,
  {}
}

Spanning Multiple Transitions¶

The @eventually attribute on its own allows eventually assumptions to be made on individual transitions and branches. However, it is sometimes necessary to be able to specify that eventually assumptions span across multiple transitions and branches. Coco supports this with the attribute called @satisfiesEventually, which can be used in combination with @eventually to specify that a group of transitions and branches fulfil an eventually assumption. The variant @eventually(p, assumption) is used to specify an eventually constraint with the label assumption (of type EventuallyAssumption), which can then be used to label other transitions or branches to specify that they are part of the same group. If the first argument evaluates to false, then it is equivalent to @eventually(false).

To illustrate the impact of spanning eventually assumptions across multiple transitions, consider the following simple port that has @eventually labelled on a single transition:

port P {
  function begin() : Nil
  function emergencyHalt() : Nil
  outgoing signal finished()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      emergencyHalt() = setNextState(Idle)

      @eventually
      spontaneous = {
        finished();
        setNextState(Idle);
      }
    }
  }
}

This port P specifies that following a call to begin(), the finished() signal will eventually occur regardless of whether a call is made on the emergencyHalt() function. Now consider the following component C with P as its provided port:

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

  machine {
    state Idle {
      client.begin() = {
        setNextState(Running);
      }
    }
    state Running {
      client.emergencyHalt() = {
        setNextState(Idle)
      }

      after(seconds(10)) = {
        client.finished();
        setNextState(Idle)
      }
    }
  }
}

Component C fails to implement P correctly with the following verification counterexample:

This counterexample shows that following a call to begin(), C can perform an unbounded sequence of alternate calls on emergencyHalt() and begin() without ever sending the finished() signal, thereby failing the eventually constraint in P. This failure is correct given its provided port P, because P requires finished() to eventually be sent regardless of whether other functions are called or not. However, there are cases where it would be useful to be able to specify that a signal is guaranteed to eventually be sent unless some other action has occurred instead, for example a call on emergencyHalt().

Using the @satisfiesEventually attribute, port P can be extended to specify that if a call to emergencyHalt() occurs, then the eventually constraint on the spontaneous transition is also satisfied:

port P {
  function begin() : Nil
  function emergencyHalt() : Nil
  outgoing signal finished()

  machine {
    static val kEventuallyFinishes : EventuallyAssumption

    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      @satisfiesEventually(kEventuallyFinishes)
      emergencyHalt() = setNextState(Idle)

      @eventually(true, kEventuallyFinishes)
      spontaneous = {
        finished();
        setNextState(Idle);
      }
    }
  }
}

In this example, the eventually constraint on the spontaneous transition in state Running is parameterised with kEventuallyFinishes. Further, the transition for the function emergencyHalt() in this state is labelled with @satisfiesEventually(kEventuallyFinishes). This groups these transitions under the same eventually constraint, and means that following a call to begin(), the signal finished() will occur, unless a call on emergencyHalt() has occurred. The component C above correctly implements this port.

In addition to labelling transitions for incoming function calls, the @satisfiesEventually attribute can also be used to label transitions and branches that can be labelled with @eventually. Multiple transitions can be labelled with the same @satisfiesEventually, as illustrated in the following example:

port P1 {
  function begin() : Nil
  function emergencyHalt() : Nil
  outgoing signal finished()
  outgoing signal updated()

  machine {
    static val kEventuallyFinishes : EventuallyAssumption

    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      @satisfiesEventually(kEventuallyFinishes)
      emergencyHalt() = setNextState(Idle)

      @eventually(true, kEventuallyFinishes)
      spontaneous = {
        finished();
        setNextState(Idle)
      }

      @satisfiesEventually(kEventuallyFinishes)
      spontaneous = {
        updated();
        setNextState(Idle)
      }
    }
  }
}

This port P1 specifies that following a call to begin(), either the signal finished() or the signal updated() will occur, unless a call on emergencyHalt() has occurred. A component that provides this port has to eventually send at least one of these signals (but is not obliged to send both), unless a call to emergencyHalt() is made. For example, the following component implements P1 correctly, even though it never sends the finished() signal:

@runtime(.MultiThreaded)
component C1 {
  val client : Provided<P1>

  machine {
    state Idle {
      client.begin() = {
        setNextState(Running);
      }
    }
    state Running {
      client.emergencyHalt() = {
        setNextState(Idle)
      }

      after(seconds(10)) = {
        client.updated();
        setNextState(Idle)
      }
    }
  }
}

This example above illustrates the difference between grouping spontaneous transitions (or branches) under the same eventually assumption versus labelling them with their own individual eventually contraint. The component C1 above only has to guarantee sending at least one of the signals sent on the labelled spontaneous transitions (unless a call on emergencyHalt() has occurred). In contrast, if the second spontaneous transition was labelled with a unique @eventually attribute instead, then an implementation would have to guarantee that both signals are eventually sent, and therefore C1 would fail the verification.

Multiple transitions can be labelled by @eventually attributes with the same EventuallyAssumption label, and will be treated as a single group, which means that at least one of them will be guaranteed to eventually occur (unless a transition labelled with @satisfiesEventually has occurred). The following port P2 is a variation of P1, where the second spontaneous transition in state Running is labelled with @eventually(true, kEventuallyFinishes) instead of @satisfiesEventually(kEventuallyFinishes) (as specified in P1 above):

port P2 {
  function begin() : Nil
  function emergencyHalt() : Nil
  outgoing signal finished()
  outgoing signal updated()

  machine {
    static val kEventuallyFinishes : EventuallyAssumption

    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      @satisfiesEventually(kEventuallyFinishes)
      emergencyHalt() = setNextState(Idle)

      @eventually(true, kEventuallyFinishes)
      spontaneous = {
        finished();
        setNextState(Idle)
      }

      @eventually(true, kEventuallyFinishes)
      spontaneous = {
        updated();
        setNextState(Idle)
      }
    }
  }
}

Although this second spontaneous transition is labelled with an @eventually attribute, it shares the same EventuallyAssumption identifier as that of the @eventually on the first spontaneous transition. This means that they belong to the same group, and is therefore equivalent to P1.

Impact on Shared Ports¶

If a component shares a required port with other clients (i.e. by calling the setAccess functions), then this might impact what assumptions it can make about whether the required port is guaranteed to perform certain events, even when they are in transitions or branches labelled with the @eventually attribute.

To illustrate this, consider the following example of a component C with a required port that is not shared:

port P {
  function begin() : Nil
  outgoing signal done()

  machine {
    begin() = done()
  }
}

port Source {
  function check() : Bool

  machine {
    check() = nondet { @eventually true, false }
  }
}

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

  machine {
    var status : Bool

    client.begin() = {
      while (!status) {
        status = source.check();
      }
      client.done()
    }
  }
}

In this example, component C relies on its required port to eventually return true when the function check() is called, in order to break out of the while loop in the begin() transition and return to its client. Its required port, Source, guarantees this by labelling the nondet branch that returns true with the @eventually attribute, and offering this labelled branch infinitely often.

In contrast, consider the following modified version of this component, CShared, where its required port is shared with other clients using the setAccess function:

@runtime(.MultiThreaded)
component CShared {
  val client : Provided<P>
  val source : Required<Source>

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

  machine {
    var status : Bool

    client.begin() = {
      while (!status) {
        status = source.check();
      }
      client.done()
    }
  }
}

The component CShared fails the responsiveness check with the following counterexample:

Although the required port, source, is guaranteed to eventually return true when check() is called, there is no guarantee that it will return true when check() is called by the CShared component. As illustrated in the counterexample, a valid infinite sequence of behaviour is for source to only return true when check() is called by the other clients, and return false when called by CShared. In this scenario, CShared becomes unresponsive, because it is unable to return to its client and process another function call.

Verification Limitations¶

When using the @eventually attribute, the verification may occasionally return a false negative for the assertion that checks whether a component satisfies the eventually constraint specified by its provided ports. This means that the assertion fails the verification when in fact it should have passed the check. This problem can arise when the @eventually attribute is not used in conjunction with an event, as illustrated in the following example:

port P {
  function check() : Nil
  function move() : Nil
  function isMoving() : Bool

  machine {
    check() = {}

    state Idle {
      move() = setNextState(Moving)
      isMoving() = false
    }
    state Moving {
      @eventually
      spontaneous = setNextState(Idle)
      isMoving() = true
    }
  }
}

In state Moving, the spontaneous transition labelled with the eventually attribute performs a state transition to Idle without sending a signal, essentially treating the eventually property as a state-based one. This can cause the verification to fail the eventually check when it should pass, as illustrated by the following example of a component, which is supposed to implement P:

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

  machine {
    client.check() = {}

    state Idle {
      client.move() = setNextState(Moving)
      client.isMoving() = false
    }
    state Moving {
      after(seconds(5)) = setNextState(Idle)
      client.isMoving() = true
    }
  }
}

The implementation of C is very similar to the specification of its provided port P, with the only difference being that the transition from Moving to Idle is implemented using a timer transition, which fires after 5 seconds.

The verification check for the eventually property fails with the following counterexample:

This counterexample illustrates that after calling move(), C can perform an infinite loop of calls on check() thereby failing to satisfy the eventually property specified in P. In fact, C does satisfy the eventually constraint and is performing these calls in the Idle state, but P cannot detect this because i) the transition satisfying the eventually constraint is invisible, and ii) it can perform the same infinite sequence of events in the states before and after the transition (in this case, the infinite sequence of calls on check()).

This is a false verification error, and requires the Coco code to be modified so that either of these two properties i) or ii) above no longer hold.

State Machine Inheritance¶

Many systems have common patterns of behaviour across multiple components, and having to repeat these patterns across many ports can be laborious and error-prone. For example, a system may specify that all of its components follow a standard sequence of initialisation behaviour, while allowing each of them to also perform their own specific behaviour when in some operational mode. Rather than duplicating the initialisation behaviour across all of the components’ ports, Coco provides an elegant way of abstracting these common patterns using state machine inheritance for ports.

If a port P2 inherits another port P1, then the state machine M2 of P2 can inherit the state machine M1 of P1, written as:

@compatible(.MultiThreaded)
port P2 : P1 {
  …
  machine M2 : M1 {
    …
  }
}

The derived port must be labelled with the @compatible attribute to denote the runtime(s) in which the derived port can be used. The verification checks whether the derived port complies with the port it inherits in each of the runtimes specified in @compatible. In this example, P2 must comply with P1 under the multi-threaded runtime only, and therefore cannot be used by components in the single-threaded runtime. For further details and examples about these verification checks, see Implements the Base Port Specification.

State machine inheritance is orthogonal to port inheritance, and allows base port state machines to be extended with additional behaviour. Every top-level state in the derived state machine must have the same name as a top-level state in the base state machine, and no transitions can be declared at the top-most level in Main.

Semantically, when one state machine inherits another, all the functionality of each top-level state of the derived state machine become nested within the corresponding top-level state of the base state machine. Further, all references in the base state machine to top-level states are changed to refer to the corresponding state in the derived state machine.

Consider the following example of a port that specifies a simple pattern of behaviour for the initialisation and monitoring of some component:

port P1 {
  function initialize() : Nil
  function isRunning() : Bool
  outgoing signal hasInitialized()

  machine M1 {
    state Idle {
      initialize() = setNextState(Running)
      isRunning() = false
    }
    state Running {
      entry() = hasInitialized()
      isRunning() = true
    }
  }
}

Now consider the following port P2 that inherits P1 and its state machine, and specifies additional behaviour in the Running state:

@compatible(.MultiThreaded, .SingleThreaded)
port P2 : P1 {
  function status() : Bool
  outgoing signal error()

  machine M2 : M1 {
    state Running {
      status() = nondet {
        true,
        false,
      }
      spontaneous = error()
    }
  }
}

The resulting behaviour of P2 is semantically equivalent to the following:

port Expanded {
  function initialize() : Nil
  function isRunning() : Bool
  function status() : Bool
  outgoing signal hasInitialized()
  outgoing signal error()

  machine {
    state Idle {
      initialize() = setNextState(Running.Running)
      isRunning() = false
    }
    state Running {
      entry() = hasInitialized()
      isRunning() = true

      state Running {
        status() = nondet {
          true,
          false,
        }
        spontaneous = error()
      }
    }
  }
}

Executing a State Machine¶

This section describes the semantics of Coco state machines in terms of how they start, and how they respond to incoming events.

Starting Up¶

Upon startup, the state machine will enter an initial state, which is determined as follows:

If the state machine has no user-defined states, the initial state is Main.
Otherwise, the initial state is the first user-defined state in the state machine.

This behaviour can be overridden by declaring an entry function in Main that calls setNextState passing the desired initial state as the parameter.

If a state machine SM₁ inherits another state machine SM₂, then the initial state of SM₁ is determined by the steps above applied to the state machine resulting from extending SM₂ with the behaviour specified in SM₁, as described in State Machine Inheritance.

If the entered state is an event state, then the state machine becomes idle, and is ready to react to incoming events appropriate to the type of state machine. In contrast, if it is an execution state, then the state machine immediately executes the block of code in that state.

Entering a State¶

When an event state is entered, the following actions are executed:

State parameters, if any, are instantiated by value.
All local variables are initialised according to their declarations.
The entry function is executed.
Every state invariant is evaluated.
If the state machine is a component state machine, for each timer transition in the current state, a corresponding interval timer is started for the specified duration.

When an execution state is entered, the following actions are executed:

State parameters, if any, are instantiated by value.
All state local variables are instantiated, and initialised according to their declarations.

Exiting a State¶

A state is exited only as a result of a state transition function. Upon exit, all unexpired interval timers are cancelled, and the exit function is executed.

Dispatching Events¶

A state machine has monitor semantics; that is, only one thread of control at a time can occupy the state machine and execute its code. A state machine is idle precisely when:

it is in an event state;
there is no event handler being executed;
if it is a component state machine, its queue is empty.

Otherwise, the state machine is busy.

Dispatching Events in a Component State Machine¶

When a component state machine is idle, it will react to incoming events in the following order:

Signals in the component’s queue.
Timer expiry events.
Function calls from the component’s environment via its provided ports, and calls to unused() for the purposes of termination.

When a function call or signal occurs, the state machine executes the handler of a matching enabled event transition. An event matches a transition precisely when the event matches the transition’s trigger event, and the source of the event matches the transition’s event source.

When a component state machine receives an incoming function call or signal in a state S, it will execute the corresponding enabled event transition declared in S. If no such match exists, then the state machine will execute the corresponding match transition declared in the nearest ancestor of S. If no matching transitions exist in any of S’s ancestors up to and including Main, then it will execute the illegal handler for that incoming event.

It is a dynamic error if, in any one state, there are two or more matching enabled event transition for a given incoming function call or signal.

The builtin termination event unused behaves in the same way as function calls, and will execute the corresponding unused transition declared in the nearest ancestor of the current state. It differs from function calls in that it is not declared or visible to a component’s provided port, cannot be guarded, and cannot result in the illegal handler.

When a timer expiry event occurs, the corresponding handler is executed. Upon completion, if the event is a periodic timer, and the transition is still enabled, a new interval timer is started. Timer events occur in deadline order, and within multiple timer events with the same deadline, the events occur in the order in which the corresponding transitions were enabled.

See also

Compound Await and Simple Await sections for details on how a component state machine executes compound await expressions and simple await statements respectively.

Dispatching Events in a Port State Machine¶

When a port state machine is idle in some state S, it will respond to an incoming function call by executing the handler of a matching enabled event transition. In contrast with component state machines, there can be more than one matching enabled transition for an incoming event, in which case one of them will be chosen and executed nondeterministically. If no such match exists, then the state machine will execute the corresponding match transition declared in the nearest ancestor of S. If no matching transitions exist in any of S’s ancestors up to and including Main, then it will execute the illegal handler for that incoming event.

In addition to handling incoming function calls, a port state machine can also nondeterministically decide to execute any enabled spontaneous transition that are declared in the current state or in any of the current state’s ancestors, up to and including Main.

Termination¶

Coco supports automatic termination of systems. In the generated code, each component stores the number of clients connected to any of its provided ports. When this reaches zero, a call on unused() is initiated on the component resulting in a call on setNextState(Terminated), thereby automatically shutting down the component. Termination cascades through the system from top to bottom due to the following actions performed upon entry to the Terminated state:

Unsubscribe from all of its required ports;
Unregister from all of its required ports, which means that they will recursively terminate.
Call purge to delete all of the signals from the its queue.

By default in Coco, a component state machine can be called to terminate at any time when it is idle, which results in the component immediately transitioning to the Terminated state. This is equivalent to explicitly declaring an unused transition that results in the execution of setNextState(Terminated) at the top level of state Main. Therefore, the following component state machine:

component DefaultTermination {
  val client : Provided<P>

  machine M {
    client.f() = {}
  }
}

is equivalent to:

component ExplicitDefaultTermination {
  val client : Provided<P>

  machine M {
    unused() = setNextState(Terminated)
    client.f() = {}
  }
}

The default termination behaviour can be overridden by declaring unused transitions in component state machines, which allows termination to be deferred and custom termination behaviour to be specified. See the Unused Transition section for further details and examples.

As part of the well-formedness checks, the verification will verify whether any runtime errors can occur resulting from a component being called to terminate. This can arise, for example, if an assertion fails in an exit function that gets executed during the state machine’s transition to Terminated, as illustrated in the following example:

port P {
  function begin() : Nil
  outgoing signal done()

  machine {
    state InActive {
      begin() = setNextState(Running)
    }
    state Running {
      spontaneous = {
        done();
        setNextState(InActive);
      }
    }
  }
}

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

  machine {
    var isDone : Bool

    exit() = assert(isDone)

    state InActive {
      entry() = {
        isDone = true;
      }
      client.begin() = {
        source.begin();
        setNextState(Running);
      }
    }
    state Running {
      entry() = {
        isDone = false;
      }
      source.done() = {
        client.done();
        setNextState(InActive);
      }
    }
  }
}

Component C can be called to terminate when it is idle in state Running, resulting in the exit() function in Main being executed as part of the transition to Terminated. In Running the value of isDone is always false (as set by the entry() function), and therefore when the exit() function in Main is executed upon termination, the verification will fail with the following runtime error:

In contrast, if component C is amended to use the following port P2 as its required port:

port P2 {
  function begin() : Nil
  outgoing signal done()

  machine {
    begin() = done()
  }
}

Then C would not have any runtime errors upon termination, because C is only idle when it is in the state InActive, and therefore the value of isDone is always true when executing any calls to terminate.

See also

Unused Transition section for details and examples of how to override the default termination behaviour.

Terminated State section.

Runtimes¶

Coco implements two runtimes, multi-threaded and single-threaded runtimes, which can be specified using the attribute @runtime(r : Runtime), where r can be either Runtime.MultiThreaded or Runtime.SingleThreaded.

Coco also supports the mixing of these two runtimes, where a system can consist of a mix of single-threaded and multi-threaded components.

There are different tradeoffs between using the single-threaded versus the multi-threaded runtime, and the decision of which one to use is dependent upon the requirements of the software being built. The multi-threaded runtime is the most expressive, and often the most intuitive one to use; however, it can suffer from component implementations becoming too complex due to the concurrency allowed, and it can also be expensive for large systems due to each component having their own background thread. In contrast, components developed using the single-threaded runtime are typically easier to build, and are much less resource intensive at runtime. The downside is that it can be difficult to ensure that the environment that the generated code runs in correctly implements the assumptions made by the Coco Platform during the verification.

The advantage of being able to use a hybrid of the two runtimes is that it enables developers to balance these tradeoffs more effectively, instead of having to pick one of them exclusively for the whole system being developed.

Multi-threaded Runtime¶

A multi-threaded component executes signal handlers, timer event handlers, and execution states autonomously and in parallel with its clients under its own internal thread, which is supplied automatically by the Coco multi-threaded runtime. The monitor semantics of Coco components ensure they are thread-safe, namely that client threads and the component’s internal thread are all mutually exclusive.

In the multi-threaded runtime, a component can change state in a way that is visible to its client even while its client is in the middle of executing a transition. This is reflected by the fact that the required ports of some component C can perform spontaneous transitions autonomously, even when C is busy executing an event transition.

The following example illustrates how a required port can spontaneously change state, and the impact this can have on the component using it:

port P1 {
  function callTwice() : Bool

  machine {
    callTwice() = true
  }
}

port P2 {
  function check() : Bool

  machine {
    state Success {
      check() = true
      @unreliable
      spontaneous = setNextState(Failure)
    }
    state Failure {
      check() = false
    }
  }
}

@runtime(.MultiThreaded)
component ImplMT {
  val client : Provided<P1>
  val source : Required<P2>

  machine {
    client.callTwice() = source.check() == source.check()
  }
}

Component ImplMT can perform a single function call callTwice() resulting in calling check() twice on its required port source. If both calls return the same value, then callTwice() returns true, otherwise it returns false. ImplMT has a provided port client, which specifies that callTwice() must always return true. Its required port source has two states, and can perform the function call check() in either of them. If check() is called in Success then it returns true, and if it is called in Failure then it returns false. Further, source can spontaneously move between the two states at anytime (via the spontaneous transitions), which means that ImplMT cannot determine which state source is in at any point, even while it is in the middle of executing callTwice().

The impact of source’s spontaneous state changes on ImplMT is reflected in the following verification error:

This counterexample is one where ImplMT fails to implement its provided port correctly, because ImplMT can perform a sequence of events that leads to callTwice() returning false, which is not allowed. This is caused by the fact that source is able to change state while ImplMT is in the middle of processing callTwice(), resulting in the consecutive check() calls on source returning different values.

Single-threaded Runtime¶

The single-threaded runtime assumes that a component, or a collection of components, executes under a single thread provided by its environment; such a grouping is called a single-threaded stack. The set of provided ports exposed to the environment is called the top boundary, and the set of required ports is called the bottom boundary.

In contrast to the multi-threaded runtime, a component that implements the ports on the bottom boundary of a single-threaded stack is not allowed to change state in a way that is visible to its client while the single-threaded stack is not idle (i.e. all of the components in the stack are idle). This is reflected by the fact that the required ports of a single-threaded component C are blocked from performing any spontaneous transitions while C is busy, and can only perform them when C is idle. This means that a component can make stronger assumptions about what state a component it uses is in than it can under the multi-threaded runtime. In turn, this can simplify the component’s implementation in some cases, because it may not have to consider as many interleavings with its required ports as it would have done under the multi-threaded runtime.

This difference between the runtimes is illustrated in the following example, which is the same as the previous one above with the only exception that it uses the single-threaded runtime:

port P1 {
  function callTwice() : Bool

  machine {
    callTwice() = true
  }
}

port P2 {
  function check() : Bool

  machine {
    state Success {
      check() = true
      @unreliable
      spontaneous = setNextState(Failure)
    }
    state Failure {
      check() = false
    }
  }
}

@runtime(Runtime.SingleThreaded)
component ImplST {
  val client : Provided<P1>
  val source : Required<P2>

  machine {
    client.callTwice() = source.check() == source.check()
  }
}

Component ImplST is labelled with the attribute @runtime(Runtime.SingleThreaded) to denote that it is using the single-threaded runtime. Its provided port client is the top boundary, and its required port source is the bottom boundary of this single-threaded stack.

Unlike component ImplMT in the previous example above (running under the multi-threaded runtime), ImplST passes all of the verification checks, including the check that verifies whether it implements its provided ports, which previously failed. Under the single-threaded runtime, the spontaneous transitions in source cannot occur between the two check() calls because ImplST is in the middle of processing the call callTwice(). This means that ImplST is guaranteed that the two check() calls on source will occur in the same state, and therefore always return the same value.

A single-threaded component does not have an internal thread, and therefore it does not process signal events from its queue independently or concurrently with the environment or any other component in the same single-threaded stack. In contrast to the multi-threaded runtime, when a component is processing a call, it only returns to its client (that made the call) when it has finished processing all of the signals in its queue. It is an invariant of a single-threaded stack that whenever a component in the stack is executing an event handler, the queues of all components it requires directly or indirectly are empty.

Processing the Queue¶

The single-threaded runtime has a special event called drainQueue, which is a command to instruct a component to drain its queue. The drainQueue event is sent upwards in the system, and causes a component to process all of the items in its queue, before recursively draining the queue of the component above it. The drainQueue event only travels upwards as a result of a spontaneous transition finishing at the bottom boundary of the single-threaded stack. Coco automatically inserts and sends this event at the end of each spontaneous transition, regardless of whether a signal is emitted as part of this transition or not. In contrast, when a component calls a function on a required port, it does not receive a drainQueue event from the required port, and instead the component drains its own queue before returning to its caller.

The Coco Platform verifies whether a component and its provided port agree upon when the drainQueue events can occur. This is essential since a component can rely on a drainQueue event being received only at certain points. To illustrate this, consider the following example:

port P {
  function begin() : Nil
  function cancel() : Nil
  outgoing signal sig()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      cancel() = setNextState(Terminated)
      spontaneous = sig()
    }
  }
}

@runtime(Runtime.SingleThreaded)
@queue(1)
component C {
  val client : Provided<P>
  val source : Required<P>

  machine {
    state Idle {
      client.begin() = {
        source.begin();
        setNextState(Running);
      }
    }
    state Running {
      client.cancel() = {
        source.cancel();
        setNextState(Terminated);
      }
      source.sig() = {
        client.sig();
        client.sig();
      }
    }
  }
}

Component C has an instance of port P as its provided port, and as its required port. When using P as its required port, C can rely on the fact that P will perform a drainQueue event upon completion of its spontaneous transition where it sends one signal sig(), in order to avoid its queue of size one from overflowing.

However, when verifying whether component C correctly implements its provided port P, the verification fails with the following counterexample:

In this counterexample, component C is able to send two sig() signals consecutively without performing a drainQueue event after the first one. This is not allowed by its provided port P, which specifies that a drainQueue event must be performed after every signal sig() is sent. This is essential because a component using this port can rely on this property to avoid its queue overflowing, as illustrated in this example where the component C has a queue size of one, and uses P as its required port. If an implementation of P was allowed to send more than one signal to C, then its queue capacity would be exceeded at runtime.

Spontaneous transitions in the single-threaded runtime are not as general purpose as they are in the multi-threaded runtime. Specifically, spontaneous transitions in the single-threaded runtime are intended to correspond to incoming signals over the bottom edge of a component (as illustrated in the example above). When this is not the case, the verification counterexamples found due to a mismatch between the drainQueue events can be more subtle. To illustrate this, consider the following example:

port P {
  function check() : Bool
  function begin() : Nil
  outgoing signal sig()

  machine {
    state Idle {
      begin() = setNextState(Pending)
    }
    state Pending {
      check() = false
      spontaneous = setNextState(Started)
    }
    state Started {
      check() = true
    }
  }
}

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

  machine {
    state Idle {
      client.begin() = setNextState(Started)
    }
    state Started {
      client.check() = true
    }
  }
}

In this example, after executing the begin() function, port P transitions to state Pending, where it can either perform the function check() and return false, or it can fire the spontaneous transition, where it transitions to state Started, and performs the drainQueue event. In Started, P can perform the function check(), which returns true. In contrast, apart from an initial drainQueue event performed upon startup, component C cannot perform any drainQueue events, as it does not have any required ports, and therefore has no way of receiving any signals across its bottom boundary. After it has executed the function begin(), C can perform the function check(), which will only ever return true.

When verifying whether component C correctly implements its provided port P, the verification fails with the following counterexample:

This counterexample illustrates how C can perform a sequence of events that is not permitted by its provided port P. This error is caused by a mismatch between when the drainQueue events occur in P versus C. After executing the function begin(), C can perform the function check() and return true. In contrast, port P is in state Pending after executing begin(), where it can either perform the function check() and return false, or it can perform a spontaneous transition, where it performs the drainQueue event and transitions to state Started. P is only able to perform the function check() that returns true when it is in this state. This means that the sequence of events that C has performed in the counterexample is not permitted by P, because C does not perform a corresponding drainQueue event before executing the check() function which returns true.

Restrictions in the Single-Threaded Runtime¶

When using the single-threaded runtime, the state machines of a component or port have to satisfy the following overarching rule: when a state machine transitions out of an idle state, and before it returns back to an idle state again, all signals emitted by the state machine must be sent to the same recipient. If a function call caused the state machine to move out of the idle state, then the recipient of the signals must be the calling client. In all other cases, the single recipient of the signals is determined by the recipient of the first signal emitted.

For single-threaded components, this rule means that they also cannot call the setAccess functions with PortAccess.Shared or PortAccess.SignalOnly for ports that send signals. A further restriction on single-threaded component state machines is that they cannot have execution states.

Consider the following example of a port that is used by a single-threaded component C1:

port Server {
  port P {
    function begin() : Nil
    outgoing signal ok()
  }
  val left : P
  val right : P

  machine {
    left.begin() = left.ok()
    right.begin() = left.ok()
    spontaneous = {
      left.ok();
      right.ok();
    }
  }
}

For the purposes of this example, let’s assume that C1 has exclusive access to port left only, and no access to port right. When begin() is called on Server by C1 via port left, then the signal ok() is sent to C1, which is allowed. In contrast, when begin() is called by another component via port right, Server sends the signal ok() to C1 via port left, which is not allowed in the single-threaded runtime. A second error is highlighted in the spontaneous transition where it sends signals to two different recipients, one of which is the single-threaded component C1, which is also not allowed.

To illustrate the restrictions imposed on single-threaded component state machines, consider the following example:

@runtime(Runtime.SingleThreaded)
@queue(1)
component C {
  val client1 : Provided<P1>
  val client2 : Provided<P2>
  val source : Required<Server>

  machine {
    client1.begin() = source.run()
    source.ok() = client2.error()
  }
}

port Server {
  function run() : Nil
  outgoing signal ok()

  machine {
    run() = ok()
  }
}

In this example, when component C receives the function call begin() from its provided port client1, it calls run() on its required port Server, which sends the signal ok() to C as a response. This means that C has not yet become idle because its queue is non-empty, and therefore it has to process the signals in its queue. When C processes the signal ok(), it sends the signal error() to its other provided port client2, which is not allowed.

The single-threaded runtime also imposes requirements on how the environment must interact with the stack:

The single-threaded stack is not thread safe, and therefore the environment must not perform concurrent calls to either boundary. All interactions between the stack and the environment are atomic and mutually exclusive.
The environment implementing the bottom boundary cannot change state or perform any actions that are visible to the single-threaded stack when the stack is not idle.
The environment in which the single-threaded stack runs is responsible for calling specific Coco functions to invoke the components in the stack to drain their queues at the right time.

Warning

The Coco Platform assumes that the environment correctly implements these requirements in order for the verification results to be valid, and the generated code to run correctly. If the environment is non-Coco code, then its compliance with these requirements cannot be verified or guaranteed by the Coco Platform.

Mixing Runtimes¶

Coco supports a hybrid between the two runtimes by allows developers to build systems that are composed of a mix of single-threaded and multi-threaded components. This is particularly beneficial for developing large systems that have single-threaded software stacks running within a multi-threaded environment.

To illustrate where the mixing of runtimes may be useful, consider the following example of a port, which models a low level interface of some hardware component:

port MessageSource {
  function hasArrived() : Bool

  machine {
    state Pending {
      hasArrived() = false
      spontaneous = setNextState(Arrived)
    }
    state Arrived {
      hasArrived() = true
    }
  }
}

MessageSource is a simple port, which has the function hasArrived() to indicate whether a message has arrived or not, and returns true or false depending on whether it is in state Pending or Arrived. When it is in the initial state Pending, it can perform a spontaneous transition to state Arrived, and so a component using this port will not know which state it is in when calling hasArrived().

Now consider the following example of a single-threaded component that uses MessageSource as its required port:

@runtime(Runtime.SingleThreaded)
component ImplST {
  val client : Provided<P>
  val source : Required<MessageSource>

  machine {
    client.check() = {
      val arrivedFirst = source.hasArrived();
      val arrivedSecond = source.hasArrived();
      assert(arrivedFirst == arrivedSecond);
    }
  }
}

Upon receiving a client.check() call, the component ImplST makes two consecutive calls to the hasArrived() function on its required port, and then has an assertion stating that the return values from these calls are always the same. When verifying this component under the single-threaded runtime, this assertion always holds, because of the single-threaded assumption that the state of the required ports (and therefore the components implementing them) do not change while the component is executing the client.check() call. This means that the required port will always be in the same state when the two consecutive calls on hasArrived() are made.

The assumption in the single-threaded runtime that the required ports do not change state while a client component is active will not necessarily reflect how the actual hardware underneath will behave. It is much more likely that the hardware component implementing the port MessageSource will receive a signal indicating that a message has arrived, and change state independently from its client. As illustrated in the following example, this can be expressed by specifying that the required port of the single-threaded component in the previous example is multi-threaded:

@runtime(Runtime.SingleThreaded)
component ImplMix {
  val client : Provided<P>
  @runtime(Runtime.MultiThreaded)
  val source : Required<MessageSource>

  machine {
    client.check() = {
      val arrivedFirst = source.hasArrived();
      val arrivedSecond = source.hasArrived();
      assert(arrivedFirst == arrivedSecond);
    }
  }
}

The verification assumptions now differ from those where the required was single-threaded, and reflect the possible interleavings resulting from the multi-threaded port. In this example, the verification finds the following error:

In this counterexample, the multi-threaded port can change state between the two consecutive calls on hasArrived() made by the component ImplMix, reflecting the fact that the required port can run concurrently with its single-threaded client. The verification fails, because the two calls on hasArrived() can return different values.

When building a single-threaded stack of components in a multi-threaded environment, the recommended approach in Coco is to use a multi-threaded encapsulating component comprising single-threaded components. This is illustrated in the following example of a multi-threaded encapsulating component called Stack, which has two single-threaded component instances called top and bottom:

@runtime(Runtime.SingleThreaded)
component TopImpl {
  val client : Provided<Top>
  val source1 : Required<Middle>
  @runtime(Runtime.MultiThreaded)
  val source2 : Required<Bottom>
  …
}

@runtime(Runtime.SingleThreaded)
component MiddleImpl {
  val client : Provided<Middle>
  @runtime(Runtime.MultiThreaded)
  val source1 : Required<Bottom>
  …
}

@runtime(Runtime.MultiThreaded)
component Stack {
  val client : Provided<Top>
  val source1 : Required<Bottom>
  val source2 : Required<Bottom>
  val top : TopImpl
  val middle : MiddleImpl

  init() = {
    connect(client, top.client);
    connect(top.source1, middle.client);
    connect(top.source2, source2);
    connect(middle.source1, source1);
  }
}

For the purposes of this example, the behaviour of the single-threaded components TopImpl and MiddleImpl are ignored, and instead the focus is on the connections declared between the components within the encapsulating component Stack itself. The connections between the components are illustrated in the following diagram:

An encapsulating component Stack defined in this way behaves in precisely the same way as a normal multi-threaded component from the perspective of other components that interact with it; i.e. it has a non-blocking queue, and processing signals takes priority over processing timers, which in turn take priority over processing function calls. However, the semantics of how incoming function calls and signals are handled within the encapsulating component differs when mixing the runtimes. Using the example of the Stack component above, the semantics of how it behaves is broken down into simple steps below.

Let’s start by considering what happens when a function call is made by one of the single-threaded components within the encapsulating component:

These function calls will be handled in precisely the same way as defined under the runtime of the component being called.

Now consider what happens when a function call is made across the top boundary of the encapsulating component on the top most single-threaded component within it:

In this case, the function call has to acquire a lock before the call can be made on top. The dashed line represents the scope of the lock.

The first category of signals to consider are those sent by a single-threaded component in the stack (i.e. within the dashed line):

These signals will be treated in precisely the same way as defined by the runtime of the component receiving the signal.

In contrast, the second category of signals are those sent across the bottom boundary of the Stack component:

In this case, these signals cannot necessarily be processed immediately by the bottom most single-threaded component, middle, since the single-threaded stack may be in the middle of processing something else and therefore not be idle. Further, under the single-threaded runtime, a component would normally process all signals from its queue first before returning to its client. This would not make sense, as these signals coming in from the environment may be unrelated to the events taking place in the single-threaded stack. Therefore, these signals are stored in a separate queue, which is created with the encapsulating component. When the single-threaded stack becomes idle, the encapsulating component uses its own background thread to process the signals in the queue: Each signal is taken from the queue, passed to the queue of the relevant single-threaded component, and run to completion before the next signal in the queue is processed. All function calls are blocked while the queue is non-empty.

Since the multi-threaded encapsulating component has its own background thread, timers can be used within the single-threaded stack of components within it. These timers are then processed by the encapsulating component’s background thread:

Using this approach is strongly recommended when building single-threaded stacks in multi-threaded environments, as it much more straightforward to ensure that the ports and runtime assumptions modelled at the boundary of the single-threaded stack correctly reflect the actual environment that the generated code will integrate into. Further, integrating the generated code into existing code bases is significantly simplified, as the code generator automatically generates all of the necessary locks, and threads.

To ensure that the verification is sound, the following restriction on how signals can be sent by multi-threaded required ports to single-threaded components applies: Signals can only occur on spontaneous transitions that are labelled with the @unbounded attribute. Therefore, the corresponding port and component must obey the rules imposed by the @unbounded attribute.