Событие B Общая функция

Question

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

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

запись: добавляет тот факт, что данный ребенок прочитал данную книгу

newbook: выводит книгу, которую данный ребенок еще не прочитал

books_query: выводит количество книг, которые прочитал данный ребенок

Вот моя модель пока

CONTEXT  
    booksContext
SETS
    STUDENTS
    BOOKS

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

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

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

У меня есть событие, на котором я хочу отметить книгу как прочитанную для данного ученика. Он принимает два параметра: имя ученика и название книги.

EVENTS
  record

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

Теперь для охранников. я хочу сказать

"If the student has not read the book already"

У меня было это, но т не работает, и я не знаю, что делать сейчас. Может кто-нибудь мне помочь

grd3: rbook(name) = ∅

Answer 1

rbook это всего лишь одна книга, но вы используете, как если бы это была функция. Ты имеешь ввиду readBooks(name) = {}? Если да, то утверждение все равно будет "Неужели студент никогда не читал книгу?".

Первая проблема, вероятно, заключается в определении readBooks, Вы смоделировали это как общую функцию от студентов к книгам. Это означает, что каждый студент прочитал ровно одну книгу. Это, вероятно, не то, что вы хотели выразить. Чтобы указать, что каждый студент прочитал произвольное количество книг, вы можете сопоставить студентов наборам книг:

readBooks : students --> POW(books)

Охранник будет rbook /: readBooks(name),

Лично я бы предпочел отношения в таком случае, с ними обычно легче справиться. Здесь пара s|->b будет в readBooks если студент s прочитал книгу b:

readBooks : students <-> books

В этом случае охранник будет name|->rbook /: readBooks,