Структуры связанных данных: ограничение операции ссылки - PullRequest
Новая
       5

Структуры связанных данных: ограничение операции ссылки

2 голосов
/ 29 сентября 2019

У меня есть модель (см. Ниже) с двумя подписями: Data и Node. Я определил некоторые предикаты, которые характеризуют жителей Узла, а именно: Orphan, Terminal и Isolated.

Что я хочу сделать - но еще не достиг - это определить предикат Link, который моделирует связывание двух узлов так, что один узел становится преемником (succ) другого. Кроме того, я хотел бы ограничить операцию так, чтобы ссылки могли быть сделаны только для Isolated узлов. Кроме того, я хотел бы, чтобы ограничение - если это возможно - каким-то образом было внутренним по отношению к предикату Link .

Вот моя последняя попытка: 

sig Data {}

sig Node {
    data: Data,
    succ: lone Node
}

// Node characterisation
pred Isolated (n: Node) { Orphan[n] and Terminal[n] }

pred Orphan (n: Node) { no m: Node | m.succ = n }

pred Terminal (n: Node) { no n.succ }


/*
 * Link
 * 
 * May only Link n to an m, when:
 *  - n differs from m
 *  - m is an Isolated Node (DOES NOT WORK)
 *
 * After the operation: 
 *  - m is the succcessor of n
 */
pred Link (n,m: Node) {
    n != m
    Isolated[m] /* Not satisfiable */
    m = succ[n]
}

pred LinkFeasible { some n,m: Node | Link[n,m] }

run LinkFeasible

Включение конъюнкта Isolated[m] делает модель неудовлетворительной. Я думаю, что понимаю почему: не может быть Node, который одновременно является Isolated и наследником другого. Я включаю его только в надежде, что это может раскрыть мои намерения.

Мой вопрос: как мне определить предикат Link, чтобы связать два узла так, чтобы с ним могли быть связаны только Isolated узлы?

1 Ответ

1 голос
/ 30 сентября 2019

Проблема в том, что вы хотите, чтобы Link был операцией , которая изменяет значение succ. Чтобы смоделировать изменения в Alloy, вам нужно добавить упорядоченную подпись, которая представляет различные состояния вашей системы. Таким образом, ваша подпись будет выглядеть примерно так: 

open util/ordering[time]

sig Time {}
sig Data {}

sig Node {
    data: Data,
    succ: Node lone -> Time
}

Но это также меняет все ваши предикаты. Вы не можете сказать, что узел изолирован или является терминалом, вы можете только сказать, что узел изолирован в момент времени T.

Если у вас есть Программные абстракции , это все покрытов разделе 6.1. Я не знаком с какими-либо хорошими руководствами по моделированию времени в Alloy за пределами этой книги.

...