Note

You are not reading the most recent version of this documentation. 1.4.7 is the latest version available.

Lesson 5: Increasing Concurrency

In the previous lesson, we modified ValveControllerImpl in an attempt to prevent it blocking its client while the valve is moving in order to comply with requirement R3. Our solution only partly meets this goal. To illustrate where our current solution fails, consider the following Coco snippet of a component implementation of a client using our ValveControllerImpl component:

    state Empty {
      api.startFillingTank() = {
        valve.open();
        setNextState(Filling);
      }
    }
    state Filling {
      api.isValveMoving() = !(valve.isOpen() || valve.isClosed())
    }

In state Filling, the client could be blocked when executing the transition for isValveMoving(), depending on whether or not the valve finished moving when isValveMoving() was called. This is because while the valve is moving, the ValveControllerImpl is in an execution state. If the client attempts a call on ValveControllerImpl while it is in an execution state, the client will become blocked until the ValveControllerImpl enters an event state.

The current implementation of the ValveControllerImpl therefore does not guarantee that isOpen() and isClosed() are always non-blocking, and so requirement R3 is not met.

In this lesson, we will build a solution in which the required non-blocking property of the valve controller is always preserved, and the client can always remain responsive.

We will be introducing the following new language features:

  • Component queues and handling incoming signals from required ports.
  • The built-in variable nextState.

Extending the Architecture

We could make the ValveHALBase component more complex to solve the asynchronies there. However, this goes against our objective of keeping ValveHALBase as a simple, handwritten component that makes the hardware/software interface accessible to the Coco components. Instead, we are going to define a new level of abstraction called the ValveDriverImpl with the goal of making a uniform interface defined by the ValveDriver port, which hides as many differences between different hardware valve types as possible.

The revised architecture is as follows:

ValveGroup valve : ValveControllerImpl driver : ValveDriverImpl client : ValveController client : ValveController client : ValveDriver hal : ValveHAL hal driver ValveHALBase Application client : ValveHAL valve ENC

In addition to the existing ValveControllerImpl component, we have now introduced the following two new components:

  1. ValveDriverImpl is a driver module which abstracts away valve-specific characteristics behind a common interface. The existence of this component, and its provided port are invisible to the client application.
  2. ValveGroup is an encapsulating component which consists of a ValveControllerImpl and a ValveDriverImpl, and implements ValveController as its provided port. It appears as a single opaque component to other components using it, which it interacts with via its provided port client.

We will abstract away from the details of whether or not the physical valve movement is synchronous or asynchronous, and the way in which the end of the valve movement is determined. This satisfies the requirement R4, and allows a single implementation of the ValveControllerImpl to work with more valve types, each of which potentially has its own, type-specific driver.

Step 1: Creating the ValveDriver Port

We start by creating a new module called ValveDriver as follows:

import unqualified ValveHAL

port ValveDriver {
  enum ValveStatus {
    case Unknown
    case Open
    case Closed
    case Moving
    case Error
  }

  function setup(prms : ValveHAL.ValveParameters) : Bool
  function open() : Nil
  function close() : Nil
  function terminate() : Nil

  outgoing signal endOfMovement(result : ValveStatus)

  machine M {
    /// Initial position unknown
    var valveStatus : ValveStatus = ValveStatus.Unknown

    terminate() = setNextState(Terminated)

    state Initial {
      setup(_ : ValveHAL.ValveParameters) = nondet {
        @represents("Parameters are valid")
        {
          setNextState(Ready);
          true
        },
        @represents("Parameters are not valid")
        false,
      }
    }

    state Ready {
      open() = setNextState(Moving(ValveStatus.Open))
      close() = setNextState(Moving(ValveStatus.Closed))
    }

    state Moving(vs : ValveStatus) {
      spontaneous = {
        valveStatus = nondet {
          @represents("Movement completed OK")
          vs,
          @represents("Movement failed")
          ValveStatus.Error,
        };
        endOfMovement(valveStatus);
        setNextState(Ready);
      }
    }
  }
}

We are not introducing any new Coco constructs in this port, so it should be clear to anyone who has worked through the previous lessons.

The complete Coco for this port is in Example_05B/src/ValveDriver.coco.

Step 2: Creating the ValveDriverImpl Component

Our next step is to create a component to implement a virtual valve. It will behave asynchronously, and report error conditions, irrespective of whether or not the underlying hardware has these properties. We have designed this example to implement asynchronous movement on hardware that behaves synchronously, while modifying the ValveControllerImpl so that it remains responsive during the valve movement.

Our complete component for ValveDriverImpl is as follows:

import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveDriverImpl {
  val client : Provided<ValveDriver>
  val hal : Required<ValveHAL>

  machine M {
    client.terminate() = setNextState(Terminated)

    state Initial {
      client.setup(vParms : ValveHAL.ValveParameters) = if (hal.setParameters(vParms)) {
        setNextState(Ready);
        true
      } else false
    }

    state Ready {
      client.open() = setNextState(Moving(ValveHAL.Cmd.Open))
      client.close() = setNextState(Moving(ValveHAL.Cmd.Close))
    }
    /// Asynchronously execute the synchronous valve movement
    execution state Moving(cmd : ValveHAL.Cmd) {
      hal.move(cmd);
      // signal end of movement - this valve has no errors
      client.endOfMovement(match (cmd) {
        ValveHAL.Cmd.Open => ValveDriver.ValveStatus.Open,
        ValveHAL.Cmd.Close => ValveDriver.ValveStatus.Closed,
      });
      // Ready for next move
      setNextState(Ready);
    }
  }
}

We have not used any new constructs in this component, so it should be clear to anyone who has worked through the previous lessons.

Similar to the previous implementation of the ValveControllerImpl, this component cannot respond to its client, the ValveControllerImpl, until the execution state has finished, and the state machine has changed to an event state. This means that for ValveControllerImpl to remain responsive to its client, it must not interact with ValveDriverImpl while the valve is moving.

The complete Coco for this component is in Example_05B/src/ValveDriver.coco.

Step 3: Modifying ValveControllerImpl to use ValveDriver

We now need to modify the ValveControllerImpl component to use the ValveDriverImpl component, instead of directly accessing the ValveHALBase. We will:

  1. Replace the current required port instance hal with a new instance of ValveDriver, called driver, and change all references of hal to driver throughout the state machine.
  2. Replace the execution state with an event state, which will handle the endOfMovement(…) signal from ValveDriver.
  3. Change the transition for the terminate() function so that when it is called, it will call terminate() on ValveDriver.

While making these changes, we will also take the opportunity to refactor ValveControllerImpl. The modified version looks like the following:

import unqualified ValveController
import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveControllerImpl {
  val client : Provided<ValveController>
  val driver : Required<ValveDriver>

  machine M {
    client.isOpen() = false
    client.isClosed() = false
    client.terminate() = setNextState(Terminated)

    state Uninit {
      client.setup(vParms : ValveHAL.ValveParameters) = if (driver.setup(vParms)) {
        setNextState(Operational.Stationary.Unknown);
        true
      } else false
    }

    state Operational {
      state Stationary {
        client.open() = {
          driver.open();
          setNextState(Moving)
        }
        client.close() = {
          driver.close();
          setNextState(Moving)
        }
        // Valve position unknown until first command received
        state Unknown {}

        state Opened {
          client.isOpen() = true
          client.open() = client.moveEnded(true)
        }

        state Closed {
          client.isClosed() = true
          client.close() = client.moveEnded(true)
        }
      }

      state Moving {
        driver.endOfMovement(result : ValveDriver.ValveStatus) = {
          setNextState(match (result) {
            ValveDriver.ValveStatus.Open => Stationary.Opened,
            ValveDriver.ValveStatus.Closed => Stationary.Closed,
            _ => abort(),
          });
          client.moveEnded(true);
        }
      }
    }
  }
}

In the refactored state machine, a new composite state called Operational is introduced to encapsulate all the states except for the uninitialised state Uninit.

Verifying your Changes (Example_05B)

The verification fails because the ValveControllerImpl is no longer well-formed and produces the following counterexample:

Exception counterexampleUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn trueopen()open()return nil[spontaneous] τ[nondet] τ Movement failed(queued): endOf...veStatus.Error)Queue full.

Analysis

The counterexample shows the required port driver is sending a signal to ValveControllerImpl, but its queue is full. This is because we have not declared a queue for the ValveControllerImpl component yet, and therefore it cannot receive any of the signals sent to it by its required port.

Step 4: Adding a Queue to ValveControllerImpl

We need to extend the ValveControllerImpl component with a queue that is big enough to store all of the signals that can be sent by its required ports before they have to be processed. In this case, a queue length of size 1 suffices.

We add a queue by labelling the ValveControllerImpl component declaration with the following @queue attribute:

@queue(1)

The modified Coco for this component is in Example_05C/src/ValveControllerImpl.coco.

Verifying the Models (Example_05C)

During verification, the Coco Platform finds an error where ValveControllerImpl calls abort(), which is not allowed:

Exception counterexampleUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn trueopen()open()return nil[spontaneous] τ[nondet] τ Movement failedreturn nil(queued): endOf...veStatus.Error)(dequeued): end...veStatus.Error)A call to abort() was made.

Analysis

This counterexample illustrates how the last event performed by ValveControllerImpl before the abort() call is to dequeue an endOfMovement(ValveStatus.Error) in state Moving. Examining the corresponding transition in Moving, we see:

        driver.endOfMovement(result : ValveDriver.ValveStatus) = {
          setNextState(match (result) {
            ValveDriver.ValveStatus.Open => Stationary.Opened,
            ValveDriver.ValveStatus.Closed => Stationary.Closed,
            _ => abort(),
          });

A match expression, matching on the result parameter in the endOfMovement(…) signal, is used to determine the next state based on the result of the movement. The type of result is ValveStatus, which is an enum with five values, but the match expression only provides logic for two of them, and an abort() for all the others.

Step 5: Adding Missing Match Cases to ValveControllerImpl

The solution to this error is to amend the match statement by adding the missing cases as follows:

        driver.endOfMovement(result : ValveDriver.ValveStatus) = {
          setNextState(match (result) {
            ValveDriver.ValveStatus.Open => Stationary.Opened,
            ValveDriver.ValveStatus.Closed => Stationary.Closed,
            ValveDriver.ValveStatus.Error => Stationary.Unknown,
            ValveDriver.ValveStatus.Unknown => Stationary.Unknown,
            ValveDriver.ValveStatus.Moving => abort(),
          });

In the case of an error, we do not know the position of the valve. For completeness, we will also add the missing cases for ValveDriver.ValveStatus.Unknown and ValveDriver.ValveStatus.Moving.

The complete Coco for this component is in Example_05D/src/ValveControllerImpl.coco.

Verifying your Changes (Example_05D)

The verification finds an error where ValveControllerImpl is not using its required port correctly. Specifically, ValveControllerImpl is not able to handle the endOfMovement(VAlveStatus.Open) signal that is sent by driver:

Trace counterexampleclientUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parameterssetup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn truereturn trueopen()open()[nondet] τ (index 1)open()return nilreturn nilreturn nilterminate()terminate()return nil The last event performed by the component was not allowed by the provided port, which expected one of: moveEnded(false)

Analysis

ValveController allows terminate() to be called while the valve is moving, and specifies that in this case ValveControllerImpl must move directly to the Terminated state, where all events are illegal. However, the counterexample illustrates the scenario where the ValveControllerImpl receives a signal from its required port after it has terminated, which it cannot handle.

Step 6: Modifying ValveController and ValveControllerImpl

There is not currently any requirement that the ValveControllerImpl should be able to handle a terminate() call while the valve is moving. Further, as we have discussed above, while the valve is moving, ValveDriverImpl is in an execution state, which means that any calls made on it will be blocked. If ValveControllerImpl is trying to make a call on ValveDriverImpl in response to a call made on ValveControllerImpl by its client, then both ValveControllerImpl and its client could end up being blocked.

To fix this error, we will change the ValveController port to prohibit terminate() from being called while the valve is moving.

Start by modifying your ValveController port to reflect this change, by adding the following transition for terminate() in state Moving as follows:

        terminate() = illegal

This will override the terminate() transition declared in Main when ValveController is in the Moving state.

Now modify your ValveControllerImpl component to match it.

The complete Coco for this component is in Example_05E/src/ValveController.coco.

Verifying your Changes (Example_05E)

The verification fails because the ValveControllerImpl does not implement its provided port correctly. In addition, there is a warning that the terminate() function on ValveDriver is never called.

We will start by analysing the first error:

Trace counterexampleclientUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parameterssetup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn truereturn trueopen()open()[nondet] τ (index 1)open()return nil[spontaneous] τ[nondet] τ Movement failed(queued): endOf...veStatus.Error)return nilreturn nil[spontaneous] τ[nondet] τ (index 0)(dequeued): end...veStatus.Error)moveEnded(true)moveEnded(true)isOpen()isOpen()return false The last event performed by the component was not allowed by the provided port, which expected one of: return true

Analysis

The counterexample shows the client calling open() on the ValveControllerImpl to open the valve, and in turn, ValveControllerImpl calls open() on its required port driver. driver sends an endOfMovement(ValveStatus.Error) signal to the ValveControllerImpl indicating that the move has failed, which in turn should send a moveEnded(false) signal to its client. Instead, it erroneously sends a moveEnded(true) specifying that the move completed without errors. As a result, the provided port, ValveController, expects ValveControllerImpl to be in state Opened when in fact, it is in state Unknown. Consequently, the isOpen() returns false when the provided port was expecting it to return true.

The second error is in fact a warning to highlight the fact that terminate() is never called on ValveDriverImpl. This occurs because we forgot to modify the terminate() transition in ValveControllerImpl to make the call.

Step 7: Modifying ValveControllerImpl

To resolve the error shown in the counterexample above, we will modify the Moving state in ValveControllerImpl to send the correct signals:

      state Moving {
        client.terminate() = illegal

        driver.endOfMovement(result : ValveDriver.ValveStatus) = {
          setNextState(match (result) {
            ValveDriver.ValveStatus.Open => Stationary.Opened,
            ValveDriver.ValveStatus.Closed => Stationary.Closed,
            ValveDriver.ValveStatus.Error => Stationary.Unknown,
            ValveDriver.ValveStatus.Unknown => Stationary.Unknown,
            ValveDriver.ValveStatus.Moving => abort(),
          });
          client.moveEnded(nextState != Stationary.Unknown);
        }
      }

Note

The builtin variable nextState : State is an immutable copy of the parameter in the most recent call to one of the state transition functions. Its value can only be changed indirectly by calling one of these state transition functions, such as setNextState.

This nextState variable is used in the following statement:

          client.moveEnded(nextState != Stationary.Unknown);

ValveControllerImpl sends the moveEnded() signal with an expression as its argument that refers to the value of nextState. If the value of nextState is Stationary.Unknown, then this means that ValveControllerImpl has received one of the error conditions from the ValveDriverImpl, and sends the signal moveEnded(false). In all other cases, it sends the signal moveEnded(true).

To resolve the warning that terminate() is never called on ValveDriverImpl we must add the missing call. Change the line:

    client.terminate() = setNextState(Terminated)

to:

    client.terminate() = {
      driver.terminate();
      setNextState(Terminated);
    }

The complete Coco for this component is in Example_05F/src/ValveControllerImpl.coco.

Verifying your Changes (Example_05F)

The project now verifies correctly.

Step 8: Extending ValveControllerImpl to Preserve Signal Data

When the valve completes a movement, the ValveDriverImpl component sends an endOfMovement(…) signal that is declared with the following signature:

  outgoing signal endOfMovement(result : ValveStatus)

In contrast, when the ValveControllerImpl component sends a signal to its client to indicate the completion of the valve movement, it does so with a signal declared as follows:

  outgoing signal moveEnded(result : Bool)

This loses information that would probably be useful to its client. We will therefore change the moveEnded() signature to match the corresponding signal sent by ValveDriverImpl by:

  1. Modifying the ValveController port to change the signal signature.
  2. Modifying the ValveControllerImpl component to solve any static type errors caused by changing its provided port.
  3. Reverifying the project, and fixing any other issues resulting from the changes.

Modifying ValveController

We will take the following steps to modify ValveController:

  1. Import the declarations from ValveDriver.
  2. Modify the signature in the signal declaration.
  3. Adapt the transition handlers that send this signal to handle the new signature.
  4. Modify the transition that sends this signal in state Moving with the new arguments.
  5. Delete the enum ValvePosition.

Your modified ValveController port should look like the following:

import unqualified ValveDriver
import unqualified ValveHAL

port ValveController {
  function setup(prms : ValveHAL.ValveParameters) : Bool
  function open() : Nil
  function close() : Nil
  function isOpen() : Bool
  function isClosed() : Bool
  function terminate() : Nil

  outgoing signal moveEnded(result : ValveDriver.ValveStatus)

  machine M {
    var position : ValveDriver.ValveStatus = ValveDriver.ValveStatus.Unknown
    isOpen() = position == ValveDriver.ValveStatus.Open
    isClosed() = position == ValveDriver.ValveStatus.Closed
    terminate() = setNextState(Terminated)

    state Uninitialised {
      setup(_ : ValveHAL.ValveParameters) = nondet {
        @represents("Invalid parameters")
        false,
        @represents("Valid parameters")
        {
          setNextState(Operational.Stationary);
          true
        },
      }
    }
    state Operational {
      state Stationary {
        open() = offer {
          if (position == ValveDriver.ValveStatus.Open) moveEnded(position),
          otherwise setNextState(Moving(ValveDriver.ValveStatus.Open)),
        }
        close() = offer {
          if (position == ValveDriver.ValveStatus.Closed) moveEnded(position),
          otherwise setNextState(Moving(ValveDriver.ValveStatus.Closed)),
        }
      }
      state Moving(pos : ValveDriver.ValveStatus) {
        entry() = {
          position = ValveDriver.ValveStatus.Unknown;
        }
        terminate() = illegal

        spontaneous = {
          position = nondet {
            pos,
            ValveDriver.ValveStatus.Unknown,
            @represents("Error")
            ValveDriver.ValveStatus.Error,
          };
          setNextState(Stationary);
        }
        exit() = {
          moveEnded(position);
        }
      }
    }
  }
}

Let’s step through each change in turn.

The following line imports ValveDriver:

import unqualified ValveDriver

This brings the declaration of ValveStatus into scope. The following line is the amended signal declaration:

  outgoing signal moveEnded(result : ValveDriver.ValveStatus)

The following lines are changed to use the values of ValveStatus:

    var position : ValveDriver.ValveStatus = ValveDriver.ValveStatus.Unknown
    isOpen() = position == ValveDriver.ValveStatus.Open
    isClosed() = position == ValveDriver.ValveStatus.Closed

The following lines are also changed to use ValveStatus defined in ValveDriver:

        open() = offer {
          if (position == ValveDriver.ValveStatus.Open) moveEnded(position),
          otherwise setNextState(Moving(ValveDriver.ValveStatus.Open)),
        }
        close() = offer {
          if (position == ValveDriver.ValveStatus.Closed) moveEnded(position),
          otherwise setNextState(Moving(ValveDriver.ValveStatus.Closed)),
        }

The parameter of state Moving is modified as follows:

      state Moving(pos : ValveDriver.ValveStatus) {

Finally, the spontaneous transition handler is changed as follows:

          position = nondet {
            pos,
            ValveDriver.ValveStatus.Unknown,
            @represents("Error")
            ValveDriver.ValveStatus.Error,
          };

The complete Coco for this port is in Example_06A/src/ValveController.coco.

Modifying ValveControllerImpl

Your ValveControllerImpl component will now have type errors caused by the changes we have made to the signal declaration in its provided port ValveController.

To fix this, edit your component so that the state machine looks like the following:

  machine M {
    client.isOpen() = false
    client.isClosed() = false
    client.terminate() = {
      driver.terminate();
      setNextState(Terminated);
    }

    state Uninit {
      client.setup(vParms : ValveHAL.ValveParameters) = if (driver.setup(vParms)) {
        setNextState(Operational.Stationary.Unknown);
        true
      } else false
    }

    state Operational {
      state Stationary {
        client.open() = {
          driver.open();
          setNextState(Moving)
        }
        client.close() = {
          driver.close();
          setNextState(Moving)
        }
        // Valve position unknown until first command received
        state Unknown {}

        state Opened {
          client.isOpen() = true
          client.open() = client.moveEnded(ValveDriver.ValveStatus.Open)
        }

        state Closed {
          client.isClosed() = true
          client.close() = client.moveEnded(ValveDriver.ValveStatus.Closed)
        }
      }

      state Moving {
        client.terminate() = illegal

        driver.endOfMovement(result : ValveDriver.ValveStatus) = {
          setNextState(match (result) {
            ValveDriver.ValveStatus.Open => Stationary.Opened,
            ValveDriver.ValveStatus.Closed => Stationary.Closed,
            ValveDriver.ValveStatus.Error => Stationary.Unknown,
            ValveDriver.ValveStatus.Unknown => Stationary.Unknown,
            ValveDriver.ValveStatus.Moving => abort(),
          });
          client.moveEnded(result);
        }
      }
    }
  }

The complete Coco for this component is in Example_06A/src/ValveControllerImpl.coco.

Step 9: Building an Encapsulating Component ValveGroup

As defined in the new architecture at the start of this lesson, some of the functionality of the ValveControllerImpl has been moved into a new component called ValveDriverImpl. The fact that we have divided the ValveControllerImpl into two components and how they are connected together at runtime, is private knowledge that should be hidden from the client. We should be free to refactor the ValveControllerImpl into as many components as we like in order to implement the specified behaviour, without having any impact on the client.

We will create a new encapsulating component called ValveGroup, which consists of an instance of ValveControllerImpl and an instance of ValveDriverImpl, and connects them together:

ValveGroup valve : ValveControllerImpl driver : ValveDriverImpl client : ValveController client : ValveController client : ValveDriver hal : ValveHAL hal driver ENC

Once we have done this, we will modify the TestValveGroup to instantiate the new ValveGroup component instead of ValveControllerImpl.

Creating ValveGroup

We start by declaring a new component called ValveGroup as follows:

import unqualified ValveController
import unqualified ValveControllerImpl
import unqualified ValveDriver
import unqualified ValveDriverImpl
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveGroup {
  val client : Provided<ValveController>
  val hal : Required<ValveHAL>

  val valve : ValveControllerImpl
  val driver : ValveDriverImpl
  init() = {
    connect(client, valve.client);
    connect(valve.driver, driver.client);
    connect(driver.hal, hal);
  }
}

The following lines declare instances of its provided and required ports:

  val client : Provided<ValveController>
  val hal : Required<ValveHAL>

The following lines declare the instances valve and driver of the components ValveControllerImpl and ValveDriverImpl respectively:

  val valve : ValveControllerImpl
  val driver : ValveDriverImpl

The following constructor specifies how the component instances are connected together:

  init() = {
    connect(client, valve.client);
    connect(valve.driver, driver.client);
    connect(driver.hal, hal);
  }

Modifying TestValveGroup to use ValveGroup

Our next step is to make the following changes to TestValveGroup:

  1. Import the declaration from ValveGroup instead of ValveControllerImpl.
  2. Instantiate ValveGroup instead of ValveControllerImpl.

Our modified TestValveGroup is as follows:

import unqualified SimulatorImpl
import unqualified ValveController
import unqualified ValveGroup
import unqualified ValveHAL

@runtime(.MultiThreaded)
component TestValveGroup {
  val client : Provided<ValveController>

  val valve : ValveGroup
  val hal : SimulatorImpl

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

The following architecture diagram is a graphical representation of our updated TestValveGroup:

TestValveGroup valve : ValveGroup hal : SimulatorImpl client : ValveController client : ValveController client : PValveHAL hal ENC ENC

Verifying your Changes (Example_06A)

Your project should now pass the verification without any errors.