Lesson 2: Adding Query Functions

In this lesson, we will be extending the ValveController port and ValveControllerImpl component to satisfy requirement R2, namely that the valve controller must enable clients to query the valve position. We will also be demonstrating how to use the Coco Platform verification to support incremental development, and highlighting the importance of ensuring that port is specified at the right level of abstraction.

This lesson introduces the following new Coco constructs:

To implement requirement R2, we need to extend the ValveControllerImpl component with query functions, which will allow its clients to determine the current state of the valve. We will make these changes as follows:

  1. Extend the ValveControllerImpl component’s provided port, ValveController, with the new query function declarations, and extend the port state machine to specify when these functions are allowed and their required behaviour when called.
  2. Re-verify ValveController and ValveControllerImpl, and identify the necessary changes that are required to make sure that the ValveControllerImpl component correctly implements this new functionality specified in ValveController.
  3. Extend the ValveControllerImpl component accordingly, and re-verify all ports and components that have been modified.

Note

The Coco Platform supports the verification being run locally on a user’s machine, or via the remote verification server. In both cases, the verification results are cached to avoid semantically unchanged Coco modules being re-verified unnecessarily. When using the remote verification, this means that the latest results are available to all members of your project team.

The Coco Assertions window in the Coco perspective shows the current verification status of every port and component in your project as they are modified and verified.

Step 1: Extending ValveController

The first step is to extend the ValveController port, which is the provided port of the ValveControllerImpl component.

Declaring the Query Functions

Add the following new function interface declarations to ValveController:

  function isOpen() : Bool
  function isClosed() : Bool

Extending the Port State Machine

Extend the ValveController port state machine by adding the following new event transitions to the Main state to specify when the new query functions can be called, and what values they return as follows:

    isOpen() = nondet {
      true,
      false,
    }
    isClosed() = nondet {
      true,
      false,
    }

Both query functions can nondeterministically return true or false.

Note

The syntax used in the nondet clauses above, namely:

    isOpen() = nondet {
      true,
      false,
    }

is equivalent to the following form, where the nondet clauses have explicit return statements:

    isOpen() = nondet {
      {
        return true;
      },
      {
        return false;
      },
    }

These event transitions are unguarded and defined in Main only. This means that they can be called in any of the user defined states defined in Main, and the corresponding event transitions declared above will be executed. A client using this port cannot determine which value will be returned, and must therefore be able to handle either of them whenever it calls one of the query functions.

Note

An event transition can be guarded by a Boolean expression. A transition is said to be enabled precisely when it is declared in an active state, and it is either unguarded or its guard evaluates to true. Except when a state machine is in the state Terminated, Main is always an active state. Therefore, an unguarded transition declared in Main is always enabled, unless it is overridden by an enabled transition for the same event in a child state. For details on how enabled transitions are selected in state machines, see the semantics section in the Coco Language Reference.

Declaring transitions in Main is one way of factoring out common behaviour. It can be used to simplify state machines, and make them more maintainable and robust against subsequent changes. This will be discussed and illustrated further in later lessons.

The complete Coco code for this port declaration can be found in Example_02B/src/ValveController.coco.

Verifying your Changes (Example_02B)

When the new ValveController port, and the existing ValveControllerImpl component are verified, the Coco Platform finds an error with one of the assertions for ValveControllerImpl, and presents the following counterexample:

client client User User ValveControllerImpl ValveControllerImpl hal hal isOpen() isOpen() isOpen() isOpen() illegal illegal Initial Initial Main Initial Initial Initial The provided port expected the last function call not to be illegal. Trace counterexample

Analysis

The verification of the ValveControllerImpl component fails, because it has not yet been extended with the new query functionality, and therefore specifies that all function calls on isOpen() and isClosed() are illegal. This is not a correct implementation of the new ValveController port, which specifies that these query functions must be allowed in every state. Therefore, ValveControllerImpl must be extended to implement these query functions.

Note

When extending or modifying the functionality offered by a component, it is often more efficient to modify the component’s provided port first, and then use the verification to identify the minimal changes required to the component so that it correctly implements it. In real applications, a port is typically much smaller and simpler than the corresponding component that implements it, and is often easier for project stakeholders to understand the changes being made. This makes the process of extending or modifying implementations more efficient.

Step 2: Extending ValveControllerImpl

The modifications that must be made to the component declaration are similar to those made to ValveController.

Extend the state machine in your ValveControllerImpl component as follows:

  machine {
    client.isOpen() = false
    client.isClosed() = false

    state Initial {
      client.setup() = setNextState(Unknown)
    }

    // Valve position unknown until the first move request is received
    state Unknown {
      client.open() = setNextState(Opened)
      client.close() = setNextState(Closed)
    }

    state Opened {
      entry() = hal.move(.Open)
      // Deliberate error
      client.isOpen() = false
      client.open() = {}
      client.close() = setNextState(Closed)
    }

    state Closed {
      entry() = hal.move(.Close)
      client.isClosed() = true
      client.open() = setNextState(Opened)
      client.close() = {}
    }
  }

A deliberate copy/paste error has been inserted in the Opened state, namely isOpened() erroneously returns false instead of true. This is to illustrate a problem with the current ValveController port specification discussed below.

The complete Coco code for this component declaration can be found in Example_02C/src/ValveControllerImpl.coco.

Verifying your Changes (Example_02C)

The ValveControllerImpl component verifies correctly. Given the deliberate error inserted in its component state machine above, why was this error not found?

Analysis

The current port declaration for ValveController specifies that the two query functions must be available in every state, and return either true or false nondeterministically. This specification is too weak, because it specifies that the query function can always return either value regardless of the actual position of the valve. Therefore, a component that always returned false irrespective of the valve’s position would be a valid implementation of this specification, as illustrated in this example. This is obviously not our intention.

Step 3: Strengthening ValveController

The specification of ValveController has to be strengthened with the following requirements:

  • Both query functions will return false until the valve position is known.
  • If the most recent function called is open(), then isOpen() must return true, and isClosed() must return false.
  • Likewise, if the most recent function called is close(), then isOpen() must return false, and isClosed() must return true.

This requires extending your ValveController port to capture the underlying state of the valve on the assumption that after calling open() or close() the valve will be in the requested position.

Add the following new enum declaration to your ValveController port:

    enum Position {
      case Opened
      case Closed
      case Unknown
    }

Add the following variable declaration inside the state machine declaration:

    var position : Position = .Unknown

This declares a new variable position of type ValvePosition with the initial value .Unknown.

Note

A variable of an enum type has a default value of the first member of the enum; a variable of type ValvePosition has a default value of .Opened. In this case, we want it to be initialised to .Unknown, hence the explicit initialisation.

Modify the event transitions in Main for the two query functions, so that they return the value according to the most recent function call that moves the valve:

    isOpen() = position == .Opened
    isClosed() = position == .Closed

Modify the state Operational in your state machine as follows:

    state Operational {
      open() = {
        position = .Opened;
      }
      close() = {
        position = .Closed;
      }
    }

Verifying your Changes (Example_02D)

When the amended ValveController port, and the existing ValveControllerImpl component are verified, the Coco Platform finds the following error:

client client User User ValveControllerImpl ValveControllerImpl hal hal setup() setup() setup() setup() return nil return nil return nil return nil open() open() open() open() move(Moves.Open) move(Moves.Open) return nil return nil return nil return nil return nil return nil isOpen() isOpen() isOpen() isOpen() return false return false Initial Initial Main Operational Unknown Operational Unknown Operational Opened Opened Main Opened Main Operational Opened Operational Opened Opened The last event performed by the component was not allowed by the provided port, which expected one of: return true Trace counterexample

Analysis

The verification fails because ValveControllerImpl does not implement its provided port ValveController correctly. As expected, this is caused by the fact that when ValveControllerImpl is in the Opened state, the function isOpened() returns false instead of true.

The solution is to correct the deliberate error that was inserted in ValveControllerImpl to specify that isOpened() always returns true when it is in the state Opened. When the component is re-verified, all of the assertions pass.

The complete Coco code for this component declaration can be found in Example_03A/src/ValveControllerImpl.coco.