An Example of Modelling and Evaluation of a Concurrent Program using Coloured Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm