Event B Total Function

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. It should also handle the following events:

record: adds the fact that the given child has read the given book

newbook: outputs a book that the given child has not already read

books_query: outputs the number of books the given child has read

Here is my model so far

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
    books
    readBooks
INVARIANTS
    students ⊆ STUDENTS
    books ⊆ BOOKS
    readBooks ∈ students → books

I have an event where I want mark a book as read for a given student. It takes in two parameters: the name of the student and the name of the book.

EVENTS
  record

  ANY
    rbook
    name
  grd1: rbook ∈ books
  grd2: name ∈ students

Now for the guards. I want to say

"If the student has not read the book already"

I had this but t doesn't work and I don't know what to do now. Can anyone help me

grd3: rbook(name) = ∅

Answer 1

rbook is just one book, but you are using is as if it was a function. Do you mean readBooks(name) = {}? If yes, the statement would still be "Has the student never read a book?".

The first problem is probably in the definition of readBooks. You modelled it as a total function from students to books. That means that every student has read exactly one book. That is probably not what you wanted to express. To state that every student has read an arbitrary number of books you can map students to sets of books:

readBooks : students --> POW(books)

The the guard would be rbook /: readBooks(name).

Personally I would prefer relations in such a case, they are usually easier to cope with. Here a pair s|->b would be in readBooks if student s has read book b:

readBooks : students <-> books

In that case the guard would be name|->rbook /: readBooks.