按 Alloy 中的日期获取物品

Question

我被这个正式方法作业问题困住了，我不确定我哪里做错了。

我有两个签名，Item 和 ToDo，它们的定义如下：

sig Item {
    due : Date lone -> Step,
    category : Category lone -> Step
}

one sig ToDo {
    list : (seq Item) -> Step,
    current : Item lone -> Step,
    completed : Item -> Step
}

我必须定义一个函数，将具有给定日期和类别的 Item 插入 ToDo 的列表集中。诀窍是列表集应该按项目的到期日期排序。步骤和日期都有顺序。

我的问题是：如何获取 ToDo.list 中具有特定日期的项目集？我已经有了这个功能：

fun tasksWithDate[d : Date, st : Step, t : set Item]: set Item

我尝试使用以下代码（及其变体）来获取 Item 集：

t.due.st.d

这不起作用，我明白为什么，因为 t.due.st 留下了一组日期。然而，从那时起的其他尝试并没有让我到达那里。我尝试使用括号让它在到达 t 之前评估“due.st”和“d”之间的连接，但这不起作用，我尝试使用方括号来更改顺序，但是那不起作用。我知道我在这里做错了什么，但我不知道是什么。

Answer 1

我提出的解决方案如下：

let r = t -> t.due.st {
    r.d
}

它所做的是创建一组 t 与 t 的到期日期的关系。然后，它与所需日期执行连接，返回包含该日期的所有 t。