Modelling Relation in Event-B

Question

I have a question as follows:

A primary school class contains a number of children and a variety of books. Write a model which keeps track of the books that the children have read. It should maintain a relation hasread between children and books.

So I have my context as so

CONTEXT  
    booksContext
SETS
    STUDENTS
    BOOKS

CONSTANTS
    student
    book
AXIOMS
    axm1: partition(STUDENTS, {student})
    axm2: partition(BOOKS,{book})

And my machine is as follows:

MACHINE
    books
SEES
    booksContext
VARIABLES
    students
    readBooks
INVARIANTS
    students ⊆ STUDENTS
    readBooks ⊆ BOOKS
    readBooks ∈ students → ℕ

readBooks ∈ students → ℕ is trowing up an error. Obviously I am modelling this wrong. Can any body help me with this? I am new to event B and I really don't know what to do

Answer 1

readBooks variable can't be both a subset of BOOKS and a total function because BOOKS isn't a total function from STUDENTS to ℕ.

The fixed model can be found in this question.

It looks like this:

MACHINE
    books
SEES
    booksContext
VARIABLES
    students
    books
    readBooks
INVARIANTS
    students ⊆ STUDENTS
    books ⊆ BOOKS
    readBooks ∈ students → books

where readBooks is a total function from the set of students to the set of books that these students have read.