2

我有一个问题如下：

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

所以我有我的背景

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 ∈ students → ℕ 出现错误。显然我在建模这个错误。任何机构都可以帮助我吗？我是事件 B 的新手，我真的不知道该怎么做

4

1 回答 1

1

readBooks 变量不能既是 BOOKS 的子集又是总函数，因为 BOOKS 不是从 STUDENTS 到 ℕ 的总函数。

固定模型可以在这个问题中找到。

它看起来像这样：

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

其中 readBooks 是从学生集到这些学生已阅读的书集的总函数。

于 2014-04-12T18:10:30.850 回答