Lesson 4: Making the Valve Controller Asynchronous

Requirement R3 states that the valve controller must be suitable for use by control systems. This means that all function calls on it must be non-blocking, and the valve controller shall always remain responsive to client requests. Our current implementation of the ValveControllerImpl component does not meet this important requirement, because it blocks its client for the duration of the valve movement. In many control system applications, this would not be acceptable.

In this lesson, our objective is to modify ValveControllerImpl to comply with R3 by making the valve movements asynchronous and non-blocking. To achieve this, we will be introducing the following language features:

We will start by extending ValveController, the provided port of ValveControllerImpl, to specify the required asynchronous behaviour, and then extend the ValveControllerImpl component to correctly implement it.

Step 1: Modifying ValveController to be Asynchronous

The provided port, ValveController, of ValveControllerImpl, must be changed to require an asynchronous implementation of the open() and close() function calls. We can think of asynchronous behaviour as being broken down into the following three phases:

Phase 1:The start of the durative action. This is performed synchronously, and starts the asynchronous, durative part of the action. It is typically assumed that this synchronous part is short enough to be regarded by the client as non-blocking.
Phase 2:This is the long duration part of the durative action that is carried out asynchronously to avoid blocking the client.
Phase 3:The end of the durative action. The client is notified that the durative action has finished. In some cases this may include information as to whether or not the durative action completed without errors.

With this in mind, we must change ValveController so that it performs the Phase 1 actions, starting the valve opening or closing, and returns immediately to the calling client, without waiting for the valve movement to finish. We model the Phase 2 actions with a separate state, which has a spontaneous transition representing the end of the valve movement. When the spontaneous transition fires, this represents the start of the Phase 3 actions, and sends a signal to inform the client that the valve movement has finished.

We will extend ValveController by:

  1. Declaring a new signal to represent the valve movement ending.
  2. Modifying the state machine so that the open() and close() functions return immediately.
  3. Adding a new state to represent the case where the valve is moving.
  4. Extending the state machine to send the signal to the client when the movement has ended. This is also sent if the valve is already in the requested position (i.e. it is already open when open() is called, or closed when closed() is called) and therefore does not need to move.

Note

In Coco, the usual way to notify a client when the durative action has finished is to send a signal. A Coco component is never blocked when sending a signal to a client, as the sending action puts the signal event into the client’s queue. Further, a component’s queue must be non-blocking, which is one of the properties that the Coco Platform will verify.

In this tutorial, we are only using the basic functionality of queues, and signals. See Queues and Queue Control for further details.

Declaring a Signal

Declare a new signal in ValveController as follows:

  outgoing signal moveEnded(result : Bool)

This declares a new signal called moveEnded(result : Bool), which will be sent by the ValveControllerImpl component (via this port) to its client to notify that the valve movement has finished. The signal has a parameter result of type Bool, which is used to indicate whether the movement completed successfully or not. When result is true, this represents the case where the move action successfully completed without any errors, and the valve is in the requested position (i.e. open or closed). It is false otherwise.

Modifying the State Machine

Change the port behaviour by replacing the Operational state with two new ones called Ready and Moving. The port is in state Moving when the valve is moving, and new move requests are not allowed. When the valve is not moving, the port is in the Ready state, where it is able to receive requests to move.

Declare the new Ready state as follows:

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

Declare the new Moving state as follows:

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

      spontaneous = {
        optional {
          position = target;
        }
        setNextState(Ready);
      }

      exit() = {
        moveEnded(position != .Unknown);
      }
    }

Moving has a parameter target of type Position, which represents whether the valve is being opened or closed. This state has an entry function, which is executed upon entry to the state, and assigns the variable position with the value .Unknown. It also has an exit function, which is executed when exiting the state, to signal the movement has ended and whether or not the valve reached to requested position. Further details about the semantics of entry functions and exit functions, and the ordering in which they are executed in transitions can be found in the Executing a State Machine section for state machines in the Coco Language Reference.

Note

An event state and an execution state can be parameterised. When a state is declared with parameters, then each instance of that 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 important to understand when using the different flavours of the state transition functions.

The state Moving introduces a special type of transition in Coco, called a spontaneous transition, which can only be used in ports, and is a powerful concept for expressing port behaviour.

Note

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.

The state Moving has the following spontaneous transition:

      spontaneous = {
        optional {
          position = target;
        }
        setNextState(Ready);
      }

The transition’s handler has the following effect:

  1. It evaluates the optional expression, which nondeterministically decides to either perform the expression, or do nothing. If the expression within optional is executed, this represents a successful outcome, and updates the position variable with the value of the state’s parameter. Otherwise, the choice of doing nothing represents an unsuccessful outcome, and the position variable remains unchanged with the value .Unknown, as set by the entry function.
  2. It sets the next state to Ready.

Your final port state machine in ValveController should be as follows:

  machine {
    enum Position {
      case Opened
      case Closed
      case Unknown
    }

    var position : Position = .Unknown

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

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

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

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

      spontaneous = {
        optional {
          position = target;
        }
        setNextState(Ready);
      }

      exit() = {
        moveEnded(position != .Unknown);
      }
    }
  }

The complete Coco for this port can be found in Example_04B/src/ValveController.coco.

Simulating ValveController (Example_04B)

Use the Coco simulator to explore your port state machine, and build at least two scenarios that execute the different options resulting from the spontaneous transition in Moving.

To launch the simulator, right-click on your ValveController port declaration in the Assertions view, and select simulator Simulate in the popup menu. For a reminder on how to use the simulator, see Coco Simulator, or the introductory steps we took in Step 5: Simulating your Ports and Components in Lesson 1.

Verifying your Changes (Example_04B)

Following the Coco approach of making small, incremental changes followed by verification, our next step is to verify all ports and components that have been modified or might be affected by the modifications. Since the ValveControllerImpl component has ValveController as its provided port, then any changes made to ValveController will require this component to be reverified too. The Assertions view in the Coco Platform will highlight which assertions in your project need to be reverified.

When running the verification on our project, we find that the ValveControllerImpl fails to correctly implement its provided port, and shows the following counterexample:

client client User User ValveControllerImpl ValveControllerImpl hal hal setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] true [nondet 0] true return true return true return true return true return true return true close() close() close() close() move(Moves.Close) move(Moves.Close) return nil return nil return nil return nil return nil return nil Initial Initial Main Initial Initial Ready Initial Main Main Unknown Main Ready Unknown Moving(Position.Closed) Closed Closed Main Closed Main Moving(Position.Closed) Closed The specification expected the component to perform one of the following events: moveEnded(false) moveEnded(true) but the component was only willing to perform: <new function call> Missing signal counterexample

Analysis

This error arises because ValveController port now requires that every valve movement is followed by a moveEnded(…) signal, whereas the ValveControllerImpl component has not been extended with this behaviour yet.

To fix this, we need to extend the ValveControllerImpl component with this additional behaviour by sending the moveEnded(…) signal at the end of every valve movement.

Step 2: Extending ValveControllerImpl with Signals

Adding Transitions for Missing Signals

In our current state machine of the ValveControllerImpl component, the valve movement is executed synchronously in the entry functions in states Opened and Closed. This seems like a reasonable place to add the missing signals.

Amend the entry function in the Opened state as follows:

      entry() = {
        hal.move(.Open);
        client.moveEnded(true);
      }

Likewise, make the corresponding amendments in the Closed state as follows:

      entry() = {
        hal.move(.Close);
        client.moveEnded(true);
      }

Your component state machine should look like the following:

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

    state Initial {
      client.setup(settings : ValveParameters) = if (hal.setParameters(settings)) {
        setNextState(Unknown);
        return true;
      } else {
        return false;
      }
    }

    // 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);
        client.moveEnded(true);
      }
      client.isOpen() = true
      client.open() = {}
      client.close() = setNextState(Closed)
    }

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

The complete Coco for this component can be found in Example_04C/src/ValveControllerImpl.coco.

Verifying your Changes (Example_04C)

The Coco Platform finds a verification error where the ValveControllerImpl fails to implement its provided port correctly, and produces the following counterexample:

client client User User ValveControllerImpl ValveControllerImpl hal hal setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] true [nondet 0] true return true return true return true return true return true return true open() open() open() open() move(Moves.Open) move(Moves.Open) return nil return nil moveEnded(true) moveEnded(true) Initial Initial Main Initial Initial Ready Initial Main Main Unknown Main Ready Unknown Moving(Position.Opened) Opened Opened Main Opened Main Opened The last event performed by the component was not allowed by the provided port, which expected one of: return nil Trace counterexample

Analysis

The counterexample shows the moveEnded(…) being sent by the ValveControllerImpl when its port, ValveController, was expecting the open() function to return immediately. In effect, ValveController expected ValveControllerImpl to perform the open() function asynchronously, in which case the moveEnded(…) signal would occur after open() returned. Instead, ValveControllerImpl is still executing valve movements synchronously and sends the moveEnded(…) signal before open() returned.

This arises because the ValveControllerImpl sends the signal in the entry function in the Opened and Closed states, which are executed before returning to the calling client. To fix this error, we must modify our ValveControllerImpl component by implementing the valve movements asynchronously, as required by the ValveController port, and to satisfy requirement R3.

Note

When an event handler has called one of the state transition functions that causes the current state to be exited, then when it returns to its caller, it performs the follows actions in order:

  1. The current state’s exit function is executed.
  2. The target state’s entry function is executed, and the state machine changes to the target state. If the state change causes multiple nested states to be exited or entered, then all of their corresponding exit functions, and entry functions are executed.
  3. Control returns to the calling client.

Step 3: Making ValveControllerImpl Asynchronous

The current ValveHAL port for the ValveHALBase software only allows synchronous behaviour, which means that we will need to modify the ValveControllerImpl so that it can transform this synchronous behaviour into asynchronous behaviour.

The approach we will take is to define a new execution state in which the blocking move(…) function is called on ValveHAL. Execution states execute concurrently with respect to the component’s client, and therefore the blocking move(…) function call will not block the client. When the valve movement is finished, the execution state will change to either Opened or Closed, according to the movement requested by the client.

Note

An execution state executes in parallel with the client under a component internal thread. It does not have any stack frames in common with the client, and it cannot access variables within the client’s stack. The body of an execution state is a block expression, which starts executing as soon as the state is entered, and ends when it has executed all of its statements. If it does not have a call on one of the state transition functions, then the state machine will remain in the execution state, and the component will be permanently unresponsive to calls made by its client. The Coco Platform checks whether a component can become unresponsive as part of its verification.

To implement these changes, we will:

  1. Add an execution state for the valve movement.
  2. Update all of the handlers for the open() and close() event transitions to change to the execution state instead of invoking the move command on ValveHAL.
  3. Delete the entry function in the Opened and Closed states, as this functionality will now be specified in the new Moving state.

Adding an Execution State

We declare a new execution state as follows:

    execution state Moving(target : ValveHAL.Moves) {
      hal.move(target);
      setNextState(match (target) {
        .Open => Opened,
        .Close => Closed,
      });
      client.moveEnded(true);
    }

The state Moving has a parameter target of type Moves (declared in ValveHAL), which represents the move operation being carried out. The state’s body is a block expression that is executed to completion when the state is entered. Upon completion, the state machine will transition to the state specified in the setNextState function.

Let’s take a closer look at each part of the block expression, starting with the first statement:

      hal.move(target);

This statement calls move(target) on its required port hal. This blocks ValveControllerImpl, but it does not block its client, because the actions performed within an execution state are executed concurrently with respect to the client.

The second statement in the block expression is a call to the setNextState function:

      setNextState(match (target) {
        .Open => Opened,
        .Close => Closed,
      });

This sets the target state that the state machine will transition to upon completion of the block expression. The argument passed to this function is a match expression.

Note

A match expression is similar to a switch statement in C-like languages. It has an expression, the value of which is compared against a list of possible matching patterns, and then evaluates the expression of the first pattern that correctly matches the value.

The final statement in the block expression is:

      client.moveEnded(true);

This sends the signal moveEnded(true) to its client to notify that the move has finished.

Note

The move(…) function defined on the ValveHAL port does not provide any information as to whether or not the valve movement succeeded. ValveControllerImpl therefore assumes the move(…) function always succeeds and the moveEnded(…) signal is always sent with true as its value.

Edit your ValveControllerImpl component so that the state machine looks like the following:

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

    state Initial {
      client.setup(settings : ValveParameters) = if (hal.setParameters(settings)) {
        setNextState(Unknown);
        return true;
      } else {
        return false;
      }
    }

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

    state Opened {
      client.isOpen() = true
      client.open() = {}
      client.close() = setNextState(Moving(.Close))
    }

    state Closed {
      client.isClosed() = true
      client.open() = setNextState(Moving(.Open))
      client.close() = {}
    }

    // Valve is Moving
    execution state Moving(target : ValveHAL.Moves) {
      hal.move(target);
      setNextState(match (target) {
        .Open => Opened,
        .Close => Closed,
      });
      client.moveEnded(true);
    }
  }

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

Verifying your Changes (Example_04D)

The Coco Platform finds a verification error where the ValveControllerImpl fails to implement its provided port correctly, and produces the following counterexample:

client client User User ValveControllerImpl ValveControllerImpl hal hal setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] true [nondet 0] true return true return true return true return true return true return true open() open() open() open() return nil return nil return nil return nil [spontaneous] o…tion = target;} [spontaneous] optional {position = target;} [nondet 0] position = target [nondet 0] position = target move(Moves.Open) move(Moves.Open) return nil return nil moveEnded(true) moveEnded(true) moveEnded(true) moveEnded(true) open() open() open() open() return nil return nil return nil return nil Initial Initial Main Initial Initial Ready Initial Main Main Unknown Main Ready Unknown Moving(Position.Opened) Moving(Moves.Open) Moving(Position.Opened) Moving(Moves.Open) Moving(Position.Opened) Ready Moving(Moves.Open) Main Opened Main Ready Opened Moving(Position.Opened) Opened Moving(Position.Opened) Opened The specification expected the component to perform one of the following events: moveEnded(false) moveEnded(true) but the component was only willing to perform: <new function call> Missing signal counterexample

Analysis

In the counterexample we can see two calls on the ValveControllerImpl to open(). The first open() call returns immediately to its client. ValveControllerImpl enters the execution state called Moving, while the client continues executing without being blocked. In parallel with the executing client, ValveControllerImpl calls the blocking move(…) function on the ValveHAL port. When the movement finishes and the move(…) function returns to ValveControllerImpl a moveEnded(true) signal is sent. When the second open() function call occurs, the valve is known to be open already, and therefore it is not necessary to call the blocking function move(…) on ValveHAL. ValveControllerImpl just returns immediately to the client, but without sending the moveEnded(true) signal.

We must change the ValveControllerImpl so that the moveEnded(…) signal is always sent, whether or not the valve is actually moved.

Step 4: Adding the Missing Signals to ValveControllerImpl

We must modify ValveControllerImpl to send the moveEnded(…) signal when open() is called in state Opened as follows:

      client.open() = client.moveEnded(true)

After making this change, your Opened state should look like the following:

    state Opened {
      client.isOpen() = true
      client.open() = client.moveEnded(true)
      client.close() = setNextState(Moving(.Close))
    }

The corresponding changes need to be made when close() is called in the Closed state, after which your Closed state should look like the following:

    state Closed {
      client.isClosed() = true
      client.open() = setNextState(Moving(.Open))
      client.close() = client.moveEnded(true)
    }

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

Verifying your Changes (Example_04E)

The Coco Platform finds a verification error where the ValveControllerImpl fails to implement its provided port correctly, and produces the following counterexample:

client client User User ValveControllerImpl ValveControllerImpl hal hal setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) setup(<unavailable>) [nondet ] ValidParameters [nondet ] ValidParameters setParameters(<unavailable>) setParameters(<unavailable>) [nondet 0] true [nondet 0] true return true return true return true return true return true return true close() close() close() close() return nil return nil return nil return nil [spontaneous] o…tion = target;} [spontaneous] optional {position = target;} [nondet 0] position = target [nondet 0] position = target move(Moves.Close) move(Moves.Close) return nil return nil moveEnded(true) moveEnded(true) moveEnded(true) moveEnded(true) close() close() close() close() moveEnded(true) moveEnded(true) Initial Initial Main Initial Initial Ready Initial Main Main Unknown Main Ready Unknown Moving(Position.Closed) Moving(Moves.Close) Moving(Position.Closed) Moving(Moves.Close) Moving(Position.Closed) Ready Moving(Moves.Close) Main Closed Main Ready Closed Moving(Position.Closed) Closed Closed The last event performed by the component was not allowed by the provided port, which expected one of: return nil Trace counterexample

Analysis

In the counterexample we can see two consecutive calls on the ValveControllerImpl to open() or close(). The first call returns immediately to its client, and ValveControllerImpl enters the execution state called Moving, while the client continues executing without being blocked. When the movement finishes, a moveEnded(true) signal is sent.

When open() or close() is called, of course, the valve might already be in the requested position, in which case, it seems reasonable that the ValveControllerImpl component would choose to send the moveEnded(true) signal and return immediately. In the counterexample, we can see this behaviour. When the second open() or close() call occurs, the valve is known to be in the required position already, and therefore it is not necessary to enter the Moving state and call the blocking move(…) function on ValveHAL. Instead, ValveControllerImpl just immediately sends the moveEnded(true) signal and returns to its client.

The port should allow this behaviour, but currently it does not. It specifies that the moveEnded(true) signal must be sent after the open() or close() function returns. We need to modify the port to allow the signal to be sent both before or after the function returns.

Note

The Coco Platform will present (one of) the shortest counterexample that leads to an error. When there are several errors with the same path length, the counterexample displayed may vary between releases. In this example, there are two errors, namely one where close() is called when the valve is already closed, and another one where open() is called when the valve is already open. The example presented above is of the latter error when we verified Example_04D (while writing the tutorial!). However, when you run the verification you may find that the Coco Platform presents a counterexample for the first error instead. The errors both have the same cause, and the solution we present below corrects both of them.

Step 5: Extending ValveController to Allow Synchronous Implementation

In the Ready state, the open() and close() transitions always change state to Moving, and return to the client as follows:

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

Therefore, the moveEnded(…) signal is always sent after returning to the client. We must change this to:

    state Ready {
      open() = nondet {
        {
          position = .Opened;
          moveEnded(true);
        },
        {
          setNextState(Moving(.Opened))
        },
      }
      close() = nondet {
        {
          position = .Closed;
          moveEnded(true);
        },
        {
          setNextState(Moving(.Closed))
        },
      }
    }

In both cases, if the valve is already in the requested position, then the moveEnded(…) signal is sent immediately, before returning to the caller, and the state remains unchanged. Otherwise, the state changes to the Moving state and the signal will be sent when the movement has finished, after returning to the caller.

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

Verifying your Changes (Example_05A)

All of the ports and components now verify correctly.