Note

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

Lesson 7: Supporting Asynchronous Termination

The ValveControllerImpl component does not currently allow terminate() to be called on it while the valve is moving, as specified by its provided port ValveController. This is because the current implementation is synchronous and allowing terminate() to be called while the valve is moving would block both the ValveControllerImpl and its client. This would arise because ValveControllerImpl would call terminate() on the ValveDriverImpl, which in turn would block both the ValveControllerImpl and its client, because it is in an execution state when the valve is moving. This would not comply with R3.

To allow terminate() to be called while the valve is moving, we need an asynchronous implementation that does not block the client while termination waits for the valve to stop moving. To achieve this, we will start by extending ValveController with an asynchronous terminate() function that can be called in every state, and then modify ValveControllerImpl to implement this accordingly.

Following the usual Coco workflow, we start by extending the ValveController port, and then we will use the verification to determine what other changes are required as a consequence.

Step 1: Modifying ValveController

As the first step, we will make the following changes to ValveController:

  1. Add a new signal called hasTerminated() to mark the end of the termination.
  2. Add a new state called Terminating, which is entered when the client calls terminate(), and exited when termination has finished. Once in this state, no function calls are allowed from the client.
  3. Add a signal send expression when exiting the Terminating state to send the new hasTerminated signal.
  4. Change the terminate() function call transition handlers to transit to this new Terminating state to allow asynchronous termination.

Adding a New Signal

Declare the new signal as follows:

  outgoing signal moveEnded(result : ValveDriver.ValveStatus)

Adding a Terminating State

Declare the new Terminating state so that it is entered whenever a terminate() event occurs as follows:

    state Terminating {
      isOpen() = illegal
      isClosed() = illegal
      terminate() = illegal
      spontaneous = setNextState(Terminated)
      exit() = {
        hasTerminated();
      }
    }

In this state, it is illegal to call the functions isOpen(), isClosed(), or terminate(). The only transition enabled is a spontaneous transition, which models the fact that at some point after entering the state it will spontaneously send a hasTerminated() signal, and terminate. Our intention is for the terminate() function to be the last call the client can make on ValveController.

The reason for all of the functions to be illegal in this state is because the client using this port cannot know whether the port is in the Terminating or Terminated state, due to the spontaneous transition firing nondeterministically changing the state from Terminating to Terminated. After the client has called terminate() but before it has processed the signal hasTerminated() from its queue, it has no way of knowing which of these two states the port is in. Therefore, the client would not be able to make any calls on ValveController following the terminate() function anyway, regardless of whether they were legal or illegal in the Terminating state.

Note

A state in a port state machine that has an enabled spontaneous transition resulting in a state change is referred to as being unstable, because it can nondeterministically fire the spontaneous transition without requiring any external stimulus. From the viewpoint of a client using a port that is in an unstable state, it cannot determine when the spontaneous transition fires, and therefore which state the port is in.

Modifying the terminate() transitions

Currently, there are two transitions declared for the function terminate(), which need to be modified, one in Main, and another in Operational.Moving.

The first one is in Main as follows:

    terminate() = setNextState(Terminated)

In order to allow both synchronous and asynchronous implementations, modify this transition to the following:

    terminate() = nondet {
      setNextState(Terminating),
      {
        hasTerminated();
        setNextState(Terminated);
      },
    }

The second one is in the state Operational.Moving, which says that the terminate() function is illegal in this state (i.e. while the valve is moving) as follows:

        terminate() = illegal

We need to change this so that it remembers that a terminate() call has occurred while moving for two reasons: firstly, to prevent a subsequent terminate() call from the client; and secondly, to enable the termination actions to be carried out when the movement ends. Change this transition to the following:

        var termPending : Bool
        terminate() = offer {
          if (!termPending) {
            termPending = true;
          },
          otherwise illegal,
        }

Modifying the Operational.Moving State

The end of the valve movement is modelled in the Operational.Moving state by a spontaneous transition, which sends a moveEnded() signal to the client, and changes state to Operational.Idle. We need to change this behaviour so that if terminate() has been called while in Operational.Moving state, we also send a hasTerminated() signal (after the moveEnded() signal), and change state to Terminated. The modified transition handler is as follows:

        spontaneous = {
          position = nondet {
            pos,
            ValveDriver.ValveStatus.Unknown,
            @represents("Error")
            ValveDriver.ValveStatus.Error,
          };
          setNextState(if (termPending) Terminated else Stationary);
        }

Finally, we also have to ensure that if a terminate() call occurs while the valve is moving, both the moveEnded() and hasTerminated() signals must be sent. To achieve this, we modify the exit function as follows:

        exit() = {
          moveEnded(position);
          if (termPending) hasTerminated();
        }

After all of these changes, your ValveController 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)
  outgoing signal hasTerminated()

  machine M {
    var position : ValveDriver.ValveStatus = ValveDriver.ValveStatus.Unknown

    isOpen() = position == ValveDriver.ValveStatus.Open
    isClosed() = position == ValveDriver.ValveStatus.Closed
    terminate() = nondet {
      setNextState(Terminating),
      {
        hasTerminated();
        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;
        }
        var termPending : Bool
        terminate() = offer {
          if (!termPending) {
            termPending = true;
          },
          otherwise illegal,
        }
        spontaneous = {
          position = nondet {
            pos,
            ValveDriver.ValveStatus.Unknown,
            @represents("Error")
            ValveDriver.ValveStatus.Error,
          };
          setNextState(if (termPending) Terminated else Stationary);
        }
        exit() = {
          moveEnded(position);
          if (termPending) hasTerminated();
        }
      }
    }
    state Terminating {
      isOpen() = illegal
      isClosed() = illegal
      terminate() = illegal
      spontaneous = setNextState(Terminated)
      exit() = {
        hasTerminated();
      }
    }
  }
}

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

Verifying your Changes (Example_07B)

The verification results show a warning in ArmourImpl, and an error in the assertions for ValveControllerImpl.

Let’s look at the error found in the ValveControllerImpl first.

Note

The general approach after changing a port that works best is to resolve any errors to the component implementing that port, followed by addressing errors in components requiring that port. The reason for this is that changing the component implementing the port can sometimes lead to making further changes to the provided port itself.

Therefore, in this case, we will make sure there is a correct implementation of ValveControllerImpl, which implements ValveController, before addressing the ArmourImpl component, which requires it.

When running the verification, the Coco Platform finds that ValveControllerImpl no longer correctly implements its provided port, and produces the following counterexample:

Missing signal counterexampleclientUserValveControllerImpldriverterminate()terminate()[nondet] τ (index 0)terminate()return nilreturn nilreturn nil The specification expected the component to perform one of the following events: hasTerminated() but the component was only willing to perform: <new function call>

Analysis

In the counterexample, the first (and only) call from the client is a terminate() call. The provided port, ValveController, stipulates that a terminate() must be followed by a hasTerminated() signal, and a state change to the Terminated state. The terminate() call occurred when ValveControllerImpl was in the Uninit state, where the only enabled transition is the one specified in Main. To fix this, we need to modify this transition to send the hasTerminated() signal.

Step 2: Adding Missing hasTerminated() Signal to ValveControllerImpl

To add the missing hasTerminated() signal, we must modify the transition in Main as follows:

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

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

Verifying your Changes (Example_07C)

Verification fails because the ValveControllerImpl does not implement its provided port correctly. The counterexample shown is as follows:

Trace counterexampleclientUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parameterssetup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn truereturn trueclose()close()close()return nilreturn nilreturn nilterminate()terminate()illegal The provided port expected the last function call not to be illegal.

Analysis

Examining the counterexample, we can see that the ValveControllerImpl component is called to move the valve, which in turn calls on the ValveDriverImpl component to carry this out. While the valve is moving (i.e. before the ValveControllerImpl sends the endOfMovement(…) signal), the client calls terminate() on the ValveControllerImpl while it is in Operational.Moving state. In this state, the terminate() call is not permitted even though it is specified as being permitted by the provided port.

Step 3: Extending ValveControllerImpl to Allow terminate() while Moving

Examining the Operational.Moving state in the ValveControllerImpl, we see the following transition:

        client.terminate() = illegal

This defines the terminate() function to be illegal in this state. We cannot simply modify this transition to call terminate() on the ValveControllerImpl, because that will block the client in the case where the valve is moving. Instead, we have to allow the terminate() call, remember that it has occurred, and then complete the termination actions when the valve has finished moving. ValveController also specifies that terminate() must be the last call that can be made on ValveControllerImpl.

When the valve has finished moving, if a terminate() is pending, then ValveControllerImpl must send the the movementEnded(…) signal followed by a hasTerminated() signal.

To implement these changes, modify the terminate() and endOfMovement(...) transition handler in Operational.Moving as follows:

      state Moving {
        var termPending : Bool
        if (!termPending) client.terminate() = {
          termPending = true;
        }

        driver.endOfMovement(result : ValveDriver.ValveStatus) = offer {
          if (termPending) {
            driver.terminate();
            client.hasTerminated();
            setNextState(Terminated);
          },
          otherwise {
            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 transition for terminate() is guarded by the boolean variable termPending:

        var termPending : Bool
        if (!termPending) client.terminate() = {
          termPending = true;
        }

If termPending is false, then the transition is enabled, which in turn sets termPending to true thereby disabling the transition.

The following lines are the modified endOfMovement(…) transition:

        driver.endOfMovement(result : ValveDriver.ValveStatus) = offer {
          if (termPending) {
            driver.terminate();
            client.hasTerminated();
            setNextState(Terminated);
          },
          otherwise {
            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);
          },
        }

If a terminate() call was made while the valve was moving, then ValveControllerImpl must call terminate() on the ValveDriverImpl, send the hasTerminated(…) signal, and change state to Terminated. Otherwise, it behaves as before.

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

Verifying the Changes (Example_07D)

The ValveControllerImpl fails to implement its required port correctly, as illustrated by the following counterexample:

Trace counterexampleclientUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parameterssetup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn truereturn trueopen()open()open()return nilreturn nilreturn nilterminate()terminate()return nilreturn nilterminate()terminate()terminate()return nilhasTerminated() The provided port expected the last function call to be illegal.

Analysis

The counterexample shows that terminate() was called twice on the ValveControllerImpl while the valve was moving. The provided port specifies that this is not allowed but the ValveControllerImpl nevertheless accepts the second call. At first sight, this result is unexpected because we have guarded the terminate() transition in Operational.Moving so that we only accept it once. Once we have seen the terminate() function call in this state, the guard disables the transition, and so a subsequent occurrence while in that state should be illegal.

At least, this is what we intended. It is not, however, what the Coco code says.

In Main, we have an enabled transition for terminate(), whereas the transition for terminate() is disabled in state Operational.Moving. This means that when a terminate() is called for the second time in this state, instead of being rejected as we intended, the call was accepted, executing the handler of the matching enabled transition in Main.

Step 4: Modifying the terminate() Transition

Instead of using a guarded transition in Operational.Moving, we will use an unguarded transition with an offer as follows:

        client.terminate() = offer {
          if (!termPending) {
            termPending = true;
          },
          otherwise illegal,
        }

When termPending is false, the offer is equivalent to the enabled transition:

client.terminate() = {termPending = true;}

When termPending is true, the offer is equivalent to the enabled transition:

client.terminate() = illegal

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

Verifying your Changes (Example_07E)

The ValveControllerImpl fails to implement its provided port correctly, as illustrated by the following counterexample:

Trace counterexampleclientUserValveControllerImpldriversetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parameterssetup(<unavailable>)[nondet] τ Para...eters are validreturn truereturn truereturn trueclose()close()close()return nilreturn nilreturn nilterminate()terminate()[spontaneous] τ[nondet] τ Move...nt completed OK(queued): endOf...eStatus.Closed)return nilreturn nil(dequeued): end...eStatus.Closed)terminate()return nilhasTerminated() The last event performed by the component was not allowed by the provided port, which expected one of: <new function call> moveEnded(ValveStatus.Error) moveEnded(ValveStatus.Unknown) moveEnded(ValveStatus.Closed)

Analysis

In the counterexample, we can see that terminate() is called on ValveControllerImpl while the valve is moving. When the movement is finished, ValveDriverImpl sends an endOfMovement(…) signal, and the ValveControllerImpl responds by sending a hasTerminated(…) signal without sending a moveEnded(…) signal first, as required by its provided port, ValveController.

To fix this, we need to modify ValveControllerImpl to send the moveEnded(…) signal in the case that the terminate() call occurs while the valve is moving.

Step 5: Add the Missing moveEnded(…) Signal to ValveControllerImpl

Add the missing signal to the endOfMovement(…) handler as follows:

        driver.endOfMovement(result : ValveDriver.ValveStatus) = offer {
          if (termPending) {
            driver.terminate();
            client.moveEnded(result);
            client.hasTerminated();
            setNextState(Terminated);
          },
          otherwise {
            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 Coco for this component is in Example_07F/src/ValveControllerImpl.coco.

Verifying your Changes (Example_07F)

All of the assertions for ValveControllerImpl now pass the verification correctly. Now we turn our attention to the warning found in ArmourImpl, the component which requires ValveController.

Analysis

The warning is telling us that ArmourImpl never calls terminate() while the valve is moving. This is because the ArmourImpl component currently intercepts a client’s request to terminate ValveController while the valve is moving, and prevents the call from being passed on. Before we modified ValveController to allow this, the ArmourImpl component was preventing what would have been an illegal call on ValveController. After having modified ValveController to accept such calls, we can modify the ArmourImpl component to allow them.

Step 6: Modifying the ArmourImpl component to allow terminate() while moving

We need to make the following changes to the ArmourImpl component:

  1. Add a new state called Terminating in which all function calls are illegal, and which terminates when it receives confirmation from ValveController that it has terminated.
  2. Delete the terminate() transition from the Busy state; we no longer have to override the terminate() transition in Main.
  3. Modify the terminate() transition in Main to change to the new Terminating state.

Adding the Terminating state

Add a new state called Terminating as follows:

    state Terminating {
      client.isOpen() = illegal
      client.isClosed() = illegal
      client.open() = illegal
      client.close() = illegal
      client.setup(_ : ValveHAL.ValveParameters) = illegal
      client.terminate() = illegal
      valve.hasTerminated() = setNextState(Terminated)

      // ignore trailing moveEnded() signals
      valve.moveEnded(_ : ValveDriver.ValveStatus) = {}
    }

All function calls are intercepted and declared to be illegal in this state.

Delete the Terminate() transition from the Busy state

After deleting the terminate() transition, the Busy state looks like the following:

    state Busy {
      valve.moveEnded(_ : ValveDriver.ValveStatus) = setNextState(Idle)
    }

Modify the terminate() transition in Main

Modify the terminate() transition in Main as follows:

    client.terminate() = {
      valve.terminate();
      setNextState(Terminating);
      true
    }

The complete Coco for this component can be found in Example_07G/src/ArmourImpl.coco.

Verifying your Changes (Example_07G)

The ArmourImpl component fails to respect the queue capacity assertion, with the following counterexample:

Exception counterexampleUserArmourImplvalvesetup(<unavailable>)setup(<unavailable>)[nondet] τ Valid parametersreturn truereturn trueopen()open()return nilreturn trueterminate()terminate()return nil[spontaneous] τ[nondet] τ (index 1)(queued): moveE...Status.Unknown)(queued): hasTerminated()Queue full.

Analysis

The ArmourImpl component has a specified queue size of 1. Prior to the modifications we made in Step 6 above, this was sufficient for two reasons:

  1. Prior to the modifications we made to ValveController in Step 1, it only sent at most one signal in response to a function call. After these modifications, if terminate() is called while the valve is moving, two signals are eventually sent in response.
  2. Prior to the modifications we made to the ArmourImpl component in Step 6, it never called ValveController to terminate while the valve is moving.

To fix this error, the ArmourImpl component’s queue capacity must be increased to 2.

Step 7: Increasing the Queue Size for ArmourImpl

We increase the ArmourImpl component’s queue size as follows:

@queue(2)

The complete Coco for this component is in Example_07H/src/Armour.coco.

Verify the Models (Example_07H)

All ports and components verify correctly.