Получение предмета по дате в Alloy - PullRequest
Новая
       47

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

0 голосов
/ 01 ноября 2010

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

У меня есть две подписи, 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, но это не работает, и я попытался использовать квадратные скобки, чтобы изменить порядок, но не работает Я знаю, что делаю что-то не так, но не могу понять, что.

1 Ответ

1 голос
/ 01 ноября 2010

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

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

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

...