Lesson 6: Armouring the Valve Controller¶

Step 1: Specifying the Armour port¶

To specify the Armour port, we need to examine ValveController to identify those functions that are always permitted versus those that are sometimes not allowed. Examining ValveController, we can see that:

1. isOpen() and isClosed() are allowed in every state, and can always be passed through.
2. open() and close() are only allowed in Ready, and must be rejected in all other states.
3. setup(…) is only allowed in Initial, and must be rejected in all other states.

We need to define new signatures for those functions that can be rejected, namely open() and close() to return a boolean as follows:

  function open() : Bool
  function close() : Bool

The other signatures are unchanged.

The state machine builds on your existing state machine for ValveController, and extends it to allow all legal calls, and intercept all illegal calls as follows:

  machine {
    var position : ValveDriver.Status = .Unknown

    isOpen() = position == .Opened
    isClosed() = position == .Closed
    open() = false
    close() = false
    setup(_) = false

    state Initial {
      setup(_) = nondet {
        {
          setNextState(Ready);
          return true;
        },
        {
          return false;
        },
      }
    }

    state Ready {
      open() = {
        setNextState(Moving(.Opened));
        return true;
      }
      close() = {
        setNextState(Moving(.Closed));
        return true;
      }
    }

    state Moving(target : ValveDriver.Status) {
      entry() = {
        position = .Unknown;
      }

      spontaneous = setNextState(Ready)

      exit() = {
        position = target;
      }
    }
  }

The complete Coco for this port is in Example_06B/src/Armour.coco.

Step 2: Building the ArmourImpl Component¶

We now need to build the ArmourImpl component, which implements the Armour port, and requires the ValveController port. This component should return true on every allowed function call, and false otherwise.

As is common with armour components, the component state machine is very similar to the state machine in its provided port. This means that we can take the following steps as a shortcut to implement the ArmourImpl component:

• Create a new module called ArmourImpl.coco, and declare a component called ArmourImpl.
• Copy the state machine from the Amour port, and paste it into the ArmourImpl component declaration.
• Modify the ArmourImpl component state machine to convert it into a proper implementation of its provided port, and add the necessary calls to its required port.
• Verify your work after each step, and fix any verification errors that arise.

import unqualified Armour
import unqualified ValveController
import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ArmourImpl {
  val client : Provided<Armour>
  val valve : Required<ValveController>
}

@queue(1)

Step 3: Building the ArmouredValveGroup Encapsulating Component¶

To make it more convenient for a client application using the armoured version of the ValveControllerImpl, we will make a new encapsulating component called ArmouredValveGroup. Clients that want to use the armoured version can then instantiate ArmouredValveGroup while clients that want the unarmoured version can instantiate ValveGroup. The armoured version would typically be used by clients not written in Coco, because their correct use of the ValveControllerImpl cannot be verified by the Coco Platform. In contrast, clients written in Coco would typically use the unarmoured version, because verifying these clients guarantees that they use the ValveControllerImpl correctly.

The new encapsulating component is declared as follows:

import unqualified Armour
import unqualified ArmourImpl
import unqualified TestValveGroup

@runtime(.MultiThreaded)
component ArmouredValveGroup {
  val client : Provided<Armour>

  val armour : ArmourImpl
  val testValve : TestValveGroup

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

The following architecture diagram is a graphical representation of ArmouredValveGroup:

This binds the TestValveGroup encapsulating component, which consists of instances of ValveControllerImpl, ValveDriverImpl and SimulatorImpl, to the ArmourImpl component, thereby forming a testable stack of software components. In turn, this means that a C++ program can then instantiate and access these components in a straightforward way.