3.4 Event-B Models

The Event-B models related to the tutoriuals are given in the next list:

3.4.1 Event-B Archives for the lectures

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.

3.4.2 Event-B Archives for the tutorial 1

Archive Rodin mcfsi1-ex1-tut1.zip.

Archive Rodin mcfsi1-ex2-tut1.zip.

Archive Rodin mcfsi1-simple.zip.

Archive Rodin mcfsi1-variant1.zip.

Archive Rodin mcfsi1-variant2.zip.

Archive Rodin mcfsi1-summation.zip.

Archive Rodin mcfsi1-ressource-pb1.zip.

Archive Rodin mcfsi1-ressource-pb2.zip.

Archive Rodin mcfsi1-invariantsafety.zip.

Archive Rodin mcfsi1-ex8.zip.

Archive Rodin ex8-tut1.zip.

Archive Rodin mcfsi1-ex9.zip.

3.4.3 Event-B Archives for the tutorial 2

Archive Rodin alg-maxtwonumbers.zp.

Archive Rodin alg-ex1.zp.

Archive Rodin alg-ex2.zp.

Archive Rodin alg-ex3.zp.

Archive Rodin alg-ex4.zp.

Archive Rodin alg-simple.zip.

3.4.4 Event-B Archives for the tutorial 3

Archive Rodin mcfsi3-ex1-plugin.zip.

Archive Rodin mcfsi3-ex2.zip.

Archive Rodin mcfsi3-ex2.zip.

Fichier power2.c.

Fichier power2.h.

Archive Rodin mcfsi3-ex3.zip.

Archive Rodin mcfsi3-ex4.zip.

Archive Rodin mcfsi3-ex5.zip.

3.4.5 Event-B Archives for the tutorial 4

Archive Rodin mcfsi4-ex1.zip.

Archive Rodin mcfsi4-ex2.zip.

Archive Rodin mcfsi4-ex3.zip.

Archive Rodin mcfsi4-ex4.zip.

3.4.6 Event-B Archives

Archive Rodin mrg1.zip.

Archive Rodin abacus.zip.