The Event-B models related to the tutoriuals are given in the next list:
Archive Rodin for explaining differences between Event-B invariant and Eveny-B theorem.
Archive Rodin for the management of school.
Archive Rodin for clock modelling.
Archive Rodin for modelling the design of the factorial function.