Implementing Generalised Alt

In this talk I will describe the design and implementation of a generalised alt operator for the Communicating Scala Objects library.  The alt operator provides a choice between communications on different channels.  The generalisation removes previous restrictions on the use of alts — but the cost of the generalisation is a much more difficult implementation.  In order to support the design, and greatly increase confidence in its correctness, I built CSP models corresponding to the designs, and used the FDR model checker to analyse them; I will describe this analysis, and discuss the relationship with the final code.