If one wants to transform a model into code, then one should be very careful to guarantee that all actions of the model are atomic. I wonder if anyone has found any algorithms that check the model and prove that all actions are atomic, independent of the level of parallelism, meaning that each action could potentially be executed by a different agent in parallel to all others.
In agda , one can easily construct functions who have types that correspond to each action of a specification. But executing them in parallel will potentially invalidate the specification due to the fact that they might not be atomic.