1

我有一个问题如下：

一个小学班级包含许多孩子和各种书籍。编写一个模型来记录孩子们读过的书。它应该保持儿童和书籍之间的关系hasread。它还应该处理以下事件：

记录：添加给定孩子已阅读给定书籍的事实

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) = ∅
4

1 回答 1

1

rbook只是一本书，但你使用 is 就好像它是一个函数。你的意思是readBooks(name) = {}？如果是，则声明仍将是“学生从未读过书吗？”。

第一个问题可能在 的定义中readBooks。您将其建模为从学生到书籍的总功能。这意味着每个学生都读过一本书。这可能不是你想要表达的。要声明每个学生都阅读了任意数量的书籍，您可以将学生映射到书籍集：

readBooks : students --> POW(books)

守卫会rbook /: readBooks(name)。

我个人更喜欢这种情况下的关系，它们通常更容易处理。如果学生 s 读过书 b s|->b，则这里有一对：readBooks

readBooks : students <-> books

在那种情况下，守卫将是name|->rbook /: readBooks。

于 2014-05-07T18:29:35.253 回答