Моделирование отношений в Event-B

Question

У меня есть вопрос следующим образом:

Класс начальной школы содержит множество детей и множество книг. Напишите модель, которая отслеживает книги, которые прочитали дети. Следует поддерживать связь между детьми и книгами.

Итак, у меня есть свой контекст как так

CONTEXT  
    booksContext
SETS
    STUDENTS
    BOOKS

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

И моя машина выглядит следующим образом:

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

readBooks ∈ student → row выдает ошибку. Очевидно, я моделирую это неправильно. Может ли кто-нибудь помочь мне с этим? Я новичок в мероприятии B, и я действительно не знаю, что делать

Answer 1

Переменная readBooks не может быть одновременно подмножеством BOOKS и общей функцией, потому что BOOKS не является полной функцией от STUDENTS до ℕ.

Фиксированная модель может быть найдена в этом вопросе.

Это выглядит так:

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

где readBooks - это общая функция от набора учащихся до набора книг, которые эти студенты прочитали.