abortableLaunch.rho

new rocketFactory in {

  // When a new rocket is setup, a launch capability for each for each operator is passed in
  contract rocketFactory(aliceLaunch, bobLaunch, ack) = {
    new aliceReadyCh, bobReadyCh in {
      // Start out neither ready
      aliceReadyCh!(false)|
      bobReadyCh!(false)|

      contract aliceLaunch(ack) = {
        new aliceAbort in {
          for (_ <- aliceReadyCh) {
            aliceReadyCh!(true)
          }
          |
          contract aliceAbort(ack) = {
            for(_ <- aliceReadyCh) {
              aliceReadyCh!(false)
              |
              ack!(Nil)
            }
          }
          |
          ack!(*aliceAbort)
        }
      }
      |
      Nil // Bob contract goes here
      | ack!(Nil)
    }
  }
  |
  // Make a new rocket to test
  new aliceLaunch, bobLaunch, ack in {
    rocketFactory!(*aliceLaunch, *bobLaunch, *ack)|
    for (_ <- ack){
      Nil // Tests go here
    }
  }
}