4.3 Event-B Models

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

4.3.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.

4.3.2 Event-B Archives for the tutorial 1

Archive Rodin ex1-tut1.zip.

Archive Rodin ex2-tut1.zip.

Archive Rodin ex4-tut1.zip.

Archive Rodin ex51-tut1.zip.

Archive Rodin ex52-tut1.zip.

Archive Rodin ex6-tut1.zip.

Archive Rodin ex7-tut1.zip.

Archive Rodin ex8-tut1.zip.

Archive Rodin ex9-tut1.zip.

Archive Rodin mcfsi1-variant1.zip.

Archive Rodin mcfsi1-variant2.zip.

Archive Rodin ex10-1-tut1.zip.

Archive Rodin ex10-2-tut1.zip.

4.3.3 Event-B Archives for the tutorial 2

Exercice 1 Tutorial 2 Nous donnons deux solutions possibles: l’une avec ok et l’autre sans ok.

Archive Rodin fx1-tut2.zip.

Archive Rodin fx1-tut2bis.zip.

Exercice 2 Tutorial 2 Archive Rodin fx2-tut2.zip.

Exercice 3 Tutorial 2 Archive Rodin mcfsi3-ex3.zip.

Exercice 4 Tutorial 2 Archive Rodin fx4-tut2.zip.

Exercice 5 Tutorial 2 Archive Rodin fx5-tut2.zip.

Exercice 6 Tutorial 2 Archive Rodin fx6-tut2.zip.

4.3.4 Event-B Archives for the tutorial 3

Exercice 1 Tutorial 3 Nous donnons deux solutions possibles: l’une avec ok et l’autre sans ok.

Archive Rodin ggx1-tut3.zip.

Exercice 2 Tutorial 3 Archive Rodin ggx2-tut3.zip.