Получение предмета по дате в Alloy

Я застрял на этой проблеме с домашним заданием по формальным методам, и я не уверен, что я не понимаю правильно.

У меня есть две подписи, 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
}

Мне нужно определить функцию, которая вставляет элемент с заданной датой и категорией в набор списков ToDo. Хитрость заключается в том, что набор списка должен быть упорядочен по дате выполнения элементов. Есть упорядочение как по Шагу, так и по Дате.

Мой вопрос: как мне получить набор элементов в ToDo.list с определенной датой? У меня есть функция:

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

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

t.due.st.d

Это не работает, и я понимаю почему, потому что t.due.st оставляет набор дат. Однако другие попытки с этого момента не приводят меня туда. Я пытался использовать круглые скобки, чтобы заставить его оценить соединение между «due.st» и «d», прежде чем перейти к t, но это не работает, и я попытался использовать квадратные скобки, чтобы изменить порядок, но это не работает. Я знаю, что я делаю что-то не так здесь, но я не могу понять, что.


formal-methods alloy
person mnuzzo    schedule 01.11.2010    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Решение, которое я придумал, следующее:

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

Это создает набор отношений t к сроку t. Затем он выполняет соединение с желаемой датой, возвращая все t с этой датой.

person mnuzzo    schedule 01.11.2010