Verification¶

Runtime Errors¶

The Coco Platform verifies whether a port is free from a range of runtime errors including:

• Calls to abort.
• Calls to assert with a false argument (either as a state invariant, or as a direct call to assert).
• The absence of a matching clause in any match expression.
• The absence of at least one of the guards evaluating to true in any nondet expression.
• Any Bounded overflows.
• Any Array out of bounds.
• Reading or loading an invalid value (i.e. a value that has not been written to yet).

Responsiveness¶

A port is responsive precisely when it always eventually allows another function call to be made. In other words, every handler must eventually terminate.

One common cause for failing this check is forgetting to transition out of an execution state correctly:

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

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    execution state Running {
      status();
      setNextState(Running);
    }
  }
}

Once port P enters the execution state Running, it remains in this state forever because there are no calls on a state transition function that lead to an event state where function calls are allowed again.

This is illustrated in the following counterexample:

Illegal-Legal Overlap¶

In any state of a port state machine, an event cannot have two corresponding enabled event transitions where one of them has a legal event handler, and the other results in the illegal handler. For example, the following snippet of Coco violates this property:

state S {
  f() = illegal
  f() = { return false; }
}

In state S, function f() is declared to be both illegal, and legal where it returns false.

Empty Spontaneous Transitions¶

A port state machine is not allowed to perform an infinite sequence of empty spontaneous transitions, where an empty spontaneous transition is one that does not send any signals, or alter the state.

Consider the following examples of ports that fail this verification check:

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

  machine {
    f() = {}
    spontaneous = {}
  }
}

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

  machine {
    state S1 {
      spontaneous = setNextState(S1)
    }
  }
}

P1 and P2 can each perform an infinite sequence of empty spontaneous transitions without sending any signals or altering the state.

The failure of this verification check is commonly caused by expressions in the spontaneous transition body that have erroneous guards, as illustrated by the following example:

port P3 {
  function begin(x : Bool) : Nil
  outgoing signal status(x : Bool)

  machine {
    state S1 {
      begin(x : Bool) = setNextState(S2(x))
    }
    state S2(allowed : Bool) {
      spontaneous = nondet {
        {
          status(true)
        },
        {
          if (allowed) status(false)
        },
      }
    }
  }
}

When P2 fires the spontaneous transition in state S2, it can nondeterministically choose between sending the signal status(true), or if the value of allowed is true, sending the signal status(false). However, allowed is never assigned the value true, which means that the second clause of the nondet expression is always empty. P2 can choose to perform an infinite sequence of the empty nondet clause, as illustrated by the following counterexample:

Reachability¶

When verifying ports, reachability information is computed to identify states or transitions that can never be reached. A state S is reachable in a state machine M precisely when there exists a sequence of events from the initial state of M to an instance of S. A transition T is reachable in a state machine M precisely when there exists a path from the initial state of M to a state where T can be executed.

Consider the following example of a simple port P:

port P {
  function begin() : Nil
  function doSomething() : Nil
  function stop() : Nil
  outgoing signal error()
  outgoing signal finished()

  machine {
    state Initial {
      begin() = setNextState(Active)
    }

    state Active {
      var isOk : Bool

      if (isOk) doSomething() = {
      }
      if (!isOk) doSomething() = error()
      if (isOk) stop() = setNextState(Stopping)
      spontaneous = {
        error();
        isOk = false;
      }
    }

    state Stopping {
      spontaneous = finished()
    }
  }
}

Port P fails the verification with a warning that it has unreachable states or transitions. When double-clicking on the reachability assertion, a structured tabular view of the results is displayed in the Counterexamples view, and the corresponding code for P is highlighted to reflect the reachability information:

Starting with the structured tabular view, the states are listed in the first column, and are indented to reflect the state hierarchy. The top two rows list the function calls that can be called on components or ports, and in the case of components only, the signals that they can receive. For every event and state pair in the table, either the entry is blank, indicating that no transition is declared for this event in this state, or it has one of the following icons:

Icon	Meaning
	All the transitions declared for this event are reachable in this state.
	There are multiple transitions declared for this event in this state, but only some of them are reachable.
	All the transitions declared for this event are unreachable in this state.

In port P above, there is an example of each of these: in the state Initial, the transition for the function begin() is reachable (denoted by ), whereas the transition declared for stop() in the state Active is unreachable (denoted by ). Further, there are multiple transitions declared for the function doSomething() in Active, some of which are reachable and some are not (denoted by ). The reachability status of states is also displayed, where the red cells with the state identifiers displayed in italics denote unreachable states, and the green cells denote reachable ones.

The code highlighting in the Coco Editor provides another view of the reachability results. In the case where there are both reachable and unreachable transitions declared for an event in the same state (denoted by in the structured view), the code highlighting identifies precisely which ones are reachable and which ones are not. This is illustrated in the example above with the transitions for the function doSomething() in the state Active.

To remove the highlighting in the Coco Editor, click on the large grey X in the top right hand corner of the Counterexamples view.

The Coco Platform also displays reachability warnings as a state machine diagram. For the example above, this results in the following diagram:

By default, unreachable states and transitions are flagged as warnings (instead of errors). These warnings can be suppressed using the attribute @ignoreWarning(.Unreachable). If all unreachable states and transitions are labelled with this attribute, then the assertion will pass the verification.

Dead States¶

A dead state is one where: i) every event transition is either disabled or results in the illegal handler, and ii) there are no enabled spontaneous transitions that are guaranteed to fire. The verification will find any dead states that are reachable from the initial state of the port state machine, with the exception of the built-in Terminated state, which is not considered to be a dead state.

Consider the following example:

function inRange(n : Int, l : Int, u : Int) : Bool = n >= l && n <= u

port P {
  function f() : Nil

  machine {
    var count : Int = 5
    state S {
      if (inRange(count, 0, 5)) f() = {
        count = -1;
      }
    }
  }
}

In state S, port P can perform the function f(), resulting in count being set to -1. The state machine remains in state S, but now the guard evaluates to false. This means that f() is illegal, and therefore the state machine has reached a dead state.

By default, dead states are flagged as warnings rather than as errors. These warnings can be suppressed using the attribute ignoreWarning(.DeadState):

function inRange(n : Int, l : Int, u : Int) : Bool = n >= l && n <= u

port P {
  function f() : Nil

  machine {
    var count : Int = 5
    @ignoreWarning(Warning.DeadState)
    state S {
      if (inRange(count, 0, 5)) f() = {
        count = -1;
      }
    }
  }
}

This makes the verification engine ignore the dead state previously found, and this check now passes.

Structural Determinism¶

A component state machine is structurally deterministic precisely when, in every state, there is precisely one matching enabled event transition that can be executed for every event.

Consider the following example:

machine M {
  var counter : Int = 0

  state S {
    if (counter <= 0) f() = { ok(); }
    if (counter >= 0) f() = { fail(); }
  }
}

This state machine violates this property, since in the case where counter is set to 0 in state S, there are two enabled event transitions for f() due to the overlapping guards. This nondeterministic behaviour is not allowed in component state machines and is therefore caught as a well-formedness error.

Using Required Ports Correctly¶

This property checks whether a component uses its required ports correctly, namely:

• A component only makes function calls on its required ports when it is permitted to do so, and
• A component is able to handle all of the return values, and signals it receives from its required ports.

The following example illustrates the case where a component makes a function call on a required port when it is not permitted to do so:

port P {
  function begin() : Nil
  function stop() : Nil

  machine {
    state Idle {
      begin() = setNextState(Active)
    }
    state Active {
      stop() = setNextState(Idle)
    }
  }
}

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

  machine {
    state Idle {
      client.begin() = {
        source.begin();
        setNextState(Active);
      }
    }
    state Active {
      client.begin() = source.begin()
      client.stop() = {
        source.stop();
        setNextState(Idle);
      }
    }
  }
}

C has the required port source, which allows the functions begin() and stop() to be called alternatively, starting with begin(). However, the component C can call begin() consecutively, which is not allowed:

The following example illustrates the case where a component receives a signal from a required port that it is not able to handle:

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

  machine {
    @unreliable
    spontaneous = error()

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

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

  machine {
    state Idle {
      client.begin() = {
        source.begin();
        setNextState(Active);
      }
    }
    state Active {
      source.done() = {
        client.done();
        setNextState(Idle);
      }
      source.error() = client.error()
    }
  }
}

Component C is only able to handle signals coming from its required port source in state S2; any signals it receives in state S1 are illegal since there are no transitions defined for them. However, source is able to spontaneously send signals in its initial state, and therefore cause an error in C, as illustrated in the following counterexample:

Similarly, components must also be able to handle all return values they receive from their required ports. In the event where they are not able to do so, this will be caught by this verification check.

Queue Capacity¶

This property checks whether a component’s required ports can send signals that exceed its queue capacity. For example, if a component specifies @queue(2), and a required port is able to spontaneously post 3 signals into the its queue, then this check will fail.

Responsiveness for Components with Clients¶

A component with clients is responsive precisely when: if a client attempts to make a function call on a component, it will eventually be able to do so. This implies that every handler will eventually terminate, and the component will infinitely often be in a state where its queue is empty.

A component is assumed to have clients unless a call to unused() is made on it, indicating that it no longer has any clients connected to it.

The following example illustrates how a component with clients can become unresponsive:

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

  machine {
    f() = sig()
  }
}

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

  machine {
    state Start {
      client.f() = source.f()
      source.sig() = source.f()
    }
  }
}

Component C fails the responsiveness check because when it calls f() on its required port, the required port sends signal sig() to C before the function returns. When processing this signal, C calls f() again on its required port, and the cycle repeats itself continuously, thereby preventing further function calls to be made on C:

Consider the case where C is extended so that it emits a visible signal to its environment when it receives the signal from its required port:

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

  machine {
    f() = sig()
  }
}

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

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

C still fails this responsiveness check for the same reason as the previous example: Although it is able to send signals across its provided port, it can still perform an unbounded sequence of events without offering function calls to its client:

Termination Responsiveness¶

A component is responsive only when following a call to unused(), it eventually enters the Terminated state. By definition, a call on unused() means that the component no longer has any clients connected to it, and therefore will not receive any function calls again.

The following example illustrates how a component can fail the responsive check because it does not guarantee termination following a call to unused():

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();
          if (shouldTerm) {
            waitingFor = .Last;
            source[0].execute();
            source[1].execute();
          } else {
            setNextState(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 if the variable shouldTerm is false.

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 the responsiveness check with the following counterexample:

The counterexample illustrates how C can perform an infinite sequence of events without terminating following a call on unused() in state Running. Following this call, C receives both finished() signals from its required ports, and then calls execute() again on both of them again when shouldTerm is true, instead of terminating as expected. This error can be resolved by replacing the event handler for source[_].finished() in Running to:

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

Reachability¶

When verifying components, reachability information is computed to flag states or transitions that can never be reached in the component state machine and in all of the required port state machines that it is connected to. See Reachability for the definitions of a reachable state and transition.

Example 1: Component fails to send a signal¶

Consider the following example of component that fails to send a signal when it is required to do so by its provided port:

port P0 {
  function begin() : Nil
  outgoing signal ready()

  machine {
    state Idle {
      begin() = setNextState(Starting)
    }
    state Starting {
      spontaneous = {
        ready();
        setNextState(Idle);
      }
    }
  }
}

port P1 {
  function begin() : Nil
  outgoing signal ok()
  outgoing signal fail()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      @slow
      spontaneous = nondet {
        {
          ok();
          setNextState(Idle);
        },
        {
          fail();
          setNextState(Idle);
        },
      }
    }
  }
}

@queue(2)
@runtime(.MultiThreaded)
component C {
  val client : Provided<P0>
  val source : Required<P1>

  machine {
    state Idle {
      client.begin() = {
        source.begin();
        setNextState(Running);
      }
    }
    state Running {
      source.ok() = {
        client.ready();
        setNextState(Idle);
      }
      source.fail() = {
        source.begin();
        setNextState(Running);
      }
    }
  }
}

Component C has the instance client as its provided port, and must therefore implement the behaviour specified by P0. However, the verification finds the following error:

P0 specifies that after function begin() is called, C must send the signal ready(). As illustrated in the counterexample above, C can perform an unbounded sequence of events with its required port without sending ready. This error is caused by the fact that the required port source can nondeterministically choose to repeatedly send the signal fail(), which in turn causes C to call begin() on source again, and repeat the cycle.

In many cases, it may be reasonable to assume that the required port will eventually send the signal ok() to indicate that it has successfully completed the action. In this case, P1 can be amended to include the @eventually attribute on the corresponding spontaneous transition as follows:

port P1 {
  function begin() : Nil
  outgoing signal ok()
  outgoing signal fail()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      @slow
      spontaneous = nondet {
        @eventually
        {
          ok();
          setNextState(Idle);
        },
        {
          fail();
          setNextState(Idle);
        },
      }
    }
  }
}

With this amendment, the component C above now correctly implements its provided port.

Example 2: Component fails to satisfy the eventually constraint¶

This check also verifies whether the component satisfies the eventually constraint specified by its provided port. Consider the following example:

port P0 {
  function check() : Nil
  outgoing signal ready()
  outgoing signal busy()

  machine {
    check() = nondet {
      @eventually
      ready(),
      busy(),
    }
  }
}

port P1 {
  function check() : Bool

  machine {
    check() = true
  }
}

port P2 {
  function check() : Bool

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

@queue(1)
@runtime(.MultiThreaded)
component C {
  val client : Provided<P0>
  val source1 : Required<P1>
  val source2 : Required<P2>

  machine {
    state Idle {
      client.check() = {
        if (source1.check() && source2.check()) {
          client.ready();
        } else client.busy();
      }
    }
  }
}

Component C has client as its provided port, which specifies that upon calling check() an arbitrary but finite number of times, C must eventually send the signal ready().

When verifying whether C implements its provided port correctly, the following counterexample is found illustrating how C violates the eventually constraint:

The cause of this error is that the required port source2 can nondeterministically decide to always return false, thereby causing C to repeatedly send the signal busy() without ever sending the signal ready() as required by its provided port.

Example 3: Component returns a value that is not allowed¶

When verifying whether a component implements it provided port correctly, the verification will also find errors where the component returns values that are not allowed by its provided port. Consider the following example:

external type Data

@derive(Default)
struct DataPacket {
  var haveData : Bool
  var data : Slot<Data>
}

port P {
  function getData() : DataPacket

  machine {
    getData() = {
      var packet : DataPacket;
      nondet {
        {
          packet.haveData = false;
          packet.data = .Invalid;
        },
        {
          packet.haveData = true;
          packet.data = .Valid;
        },
      }
      return packet;
    }
  }
}

Port P specifies the valid combinations of fields in a DataPacket. If the field haveData is true, then the field data (of type Slot<Data>) must contain a valid value. If the field haveData is false, then the field data must not contain a valid value.

Consider the following component C that is intended to implement this port:

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

  machine {
    client.getData() = {
      var packet : DataPacket;
      makeDataPacket(&packet);
      return packet;
    }
  }
}

Component C implements the getData() transition by calling the external function makeDataPacket(…) to complete the field data, which is declared as follows:

external function makeDataPacket(d : &out DataPacket) : Nil = {
  d.haveData = nondet {
    true,
    false,
  };
}

The verification fails because C does not implement its provided port P correctly. The Coco Platform produces the following counterexample:

The verification fails because in component C, the function getData() can return a DataPacket in which the field haveData is true and the field data has no valid value. This is not allowed by its provided port P, which specifies that getData() must return a DataPacket where haveData is true and data is valid, or haveData is false and data is invalid. This error in the component arises because the external function makeDataPacket(…) does not ensure the data field is valid.

Example 4: Component fails to implement either of its two provided ports¶

This example consists of a component with two provided ports, but fails to implement either of them. Consider the following two ports, which will be used as the provided ports for the component below.

port P1 {
  function begin() : Nil
  outgoing signal ok()
  outgoing signal fail()

  machine {
    state Idle {
      begin() = setNextState(Running)
    }
    state Running {
      spontaneous = {
        nondet {
          ok(),
          fail(),
        };
        setNextState(Idle);
      }
    }
  }
}

port P2 {
  function change() : Nil

  machine {
    change() = {}
  }
}

Port P1 allows the function begin() to be called in the Idle state, which causes the state machine to transition to state Running. In Running, the port will spontaneously send either the signal ok() or fail(), and return to Idle. Port P2 simply allows the function change() to be called repeatedly in the same state.

Now consider the following component, which has instances of P1 and P2 as its provided ports, and therefore has to implement both of them independently of one another:

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

  machine {
    state Idle {
      client1.begin() = setNextState(Running)
    }
    state Running {
      after(milliseconds(1)) = {
        client1.ok();
        setNextState(Idle);
      }
      client2.change() = setNextState(Idle)
    }
  }
}

The component state machine starts in state Idle, where the function begin() can be called via its provided port client1 causing the state machine to transition to state Running. In Running, the component can either fire the timer transition, or it can receive a call on the function change() via its other provided port client2 and transition back to state Idle.

When the verification is run, the assertions verifying whether the component implements its provided ports fail in both cases.

The following counterexample illustrates the case where the component fails to implement its provided port client1:

After performing the function call begin(), the component must send either the signal ok() or fail() according to P1. However, before the component can perform the timer transition to send signal ok(), it receives the call change() via its other provided port client2, and transitions back to Idle where it cannot send any signals.

The following counterexample illustrates the case where the component fails to implement its provided port client2:

When it is in the Idle state, the component is not able to accept a call on change(), which it must be able to offer in all states according to its provided port P2.

Example 5: Spontaneous transitions that are not assumed to eventually occur¶

During verification, Coco is able to make certain optimizations in the case where it is able to statically determine whether a spontaneous transition in a port that is being used by a component results in visible behaviour (i.e. the sending of a signal). Specifically, in this case it 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 send signals directly within the transition itself, Coco is able to apply this optimization. However, in the cases where spontaneous transitions do not send any signals or send them indirectly, Coco is not always able to do so for all of the verification assertions, and in some cases may require users to label the spontaneous transitions with @eventually. Examples of how spontaneous transitions can send signals directly versus indirectly can be found in Optimizing How Spontaneous Transitions Are Handled.

The following example is of a component that is dependent upon eventually receiving a signal in order to implement its provided port, but where the signal is sent indirectly resulting from the occurrence of a spontaneous transition:

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() = {}
    }
  }
}

port SendUpdates {
  outgoing signal update()

  machine {
    @slow
    spontaneous = update()
  }
}

@queue(2)
@runtime(.MultiThreaded)
component Impl {
  val client : Provided<SignalInEntry>
  val source1 : Required<SignalInEntry>
  val source2 : Required<SendUpdates>

  init() = { setUnique(source2, SendUpdates.update); }

  machine {
    source2.update() = {}

    state Init {
      client.begin() = {
        source1.begin();
        setNextState(Starting);
      }
    }
    state Starting {
      source1.ready() = {
        client.ready();
        setNextState(Running);
      }
    }
    state Running {
      client.doSomething() = source1.doSomething()
    }
  }
}

The component Impl has two required ports, SignalInEntry and SendUpdates, and has to implement SignalInEntry as its provided port. When verifying whether the component implements it provided port, the verification fails with the following counterexample:

When the component has executed the function begin(), its provided port specifies that it must send the signal ready(), whereas the component can perform an unbounded sequence of behaviour without sending the signal instead. The component sends the signal ready() to its client only when it receives the corresponding signal from its required port SignalInEntry. This means that the component is dependent upon SignalInEntry eventually sending the ready() signal in order to satisfy its provided port specification.

Following the sequence of actions in the counterexample, the SignalInEntry port is in state Starting, where it can only perform a spontaneous transition, which results in a state change to Running and the sending of the signal ready() in its entry function. Further, the component can also receive an unbounded sequence of update() signals from its other required port SendUpdates, which it simply ignores.

This is an example of where Coco is not able to statically determine whether the spontaneous transition in SignalInEntry results in the sending of a signal or not. It therefore cannot assume that the spontaneous transition will eventually occur when verifying a component that uses SignalInEntry as its required port, because in the event that a spontaneous transition does not result in any visible behaviour, then this assumption would be unsound when verifying certain classes of properties.

To solve this, SignalInEntry can either be modified to follow the recommended pattern where the signal is sent directly within the spontaneous transition itself, instead of in the entry function of Running:

    state Starting {
      spontaneous = {
        ready();
        setNextState(Running);
      }
    }

Alternatively, the the spontaneous transition can be labelled with the @eventually attribute:

    state Starting {
      @eventually
      spontaneous = setNextState(Running)
    }

In the event that a spontaneous transition does not result any visible behaviour, or the signal is being sent indirectly due a genuine need to factor out common code, then labelling the spontaneous transition with @eventually is the way to resolve this. When doing so, users must be confident that this is the intended behaviour, particularly when specifying ports for external components.