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.