language+verification: Dealing with infinity/fairness
In process algebra, any loop of hidden events is a livelock. In reality these loops often occur in the context of some non-deterministic choice to continue or break out of the loop. If one could rely on fairness, there would not be a livelock as such. However at the level of a non-deterministic choice, fairness cannot be represented. We want to solve this for Dezyne.