The aim of this practical is to gain further experience in writing Event-B specifications, and then analyzing their correctness.
This practical is concerned with constructing a model which tracks student projects and marks. The model should make use of the sets STUDENT, MARK, and PROJECT, and the constant maxmark. The model will use the following variables:
students - this keeps track of the set of students who are signed up for projects
projects – this is a function which relates students to the project they are doing
marks – this is a function which keeps track of the marks students have been awarded for their projects.
Your model should contain within it the following information:
that MARK is the set 0..maxmark
that no two students can do the same projects
that students do not have marks unless they have projects
whether projects and marks are injective, surjective, total, etc.
The model should start in a state in which no students are associated with any projects. It should handle the following events:
drop_student: removes the given student and his/her project from the system.
sign_up: allows the given student to sign up for the given project provided the student has no project and the project is free
assign_project: arbitrarily chooses a free project and assigns it to the given student
query_student: gives the student doing the given project
query_project: gives the project to which the given student has been assigned
enter_mark: assigns the given mark to the given student
query_mark: gives the mark achieved by the given student
top_student: gives the student with the highest mark; if there is more than one such student, then any of these top students can be given
random_project: gives a random project which has been marked