开发者

Getting an item by its date in Alloy

I'm stuck on this formal methods homework problem and I'm not sure what I'm not getting right.

I have two signatures, Item and ToDo which are defined as so:

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

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

I have to define a function which inserts an Item with a given date and category into the list set of ToDo. The trick is that the list set is supposed to be ordered by the due date of the items. There is ordering on both Step and Date.

My question is: How do I get开发者_如何学Go the set of Items in ToDo.list with a specific date? I've got the function:

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

And I've tried using the following code (and variations thereof) to get the set of Item:

t.due.st.d

This doesn't work, and I understand why because t.due.st leaves a set of dates. However other attempts from that point don't get me there. I've tried using parentheses to get it to evaluate the join between "due.st" and "d" before getting to the t, but that doesn't work and I've tried using square brackets to change the order, but that doesn't work. I know I'm doing something wrong here, but I can't figure out what.


The solution that I came up with is the following:

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

What this is doing is creating a set of relations of t to the due date of t. It then performs a join with the desired date returning all t with that date.

0

上一篇:

下一篇:

精彩评论

暂无评论...
验证码 换一张
取 消

最新问答

问答排行榜