Я новичок в Alloy, и я все еще довольно смущен. Я относительно уверен в математических отношениях, но не уверен, как перевести их в Alloy.Представление математических отношений в сплаве
Скажем, у меня есть следующее определение (математической) связи
rel = {(x, y) | x \in S1, y \in S2}
Является ли следующий фрагмент сплава правильное представление «отн»?
sig S2 {}
sig S1 {rel: S2}
Как бы я ограничил это отношение нерефлексивным и переходным?
Да, ваша модель определяет rel как связь между наборами S1 и S2. Для того, чтобы ограничить отношения вы могли бы написать что-то вроде этого:
fact antireflexive { no iden & rel }
То есть, нет никакого элемента отображается в себя в rel
И
fact transitive { rel = ^rel }
Это означает, что rel равно его транзитивного замыкания и поэтому транзитивным.
Сначала определите типы:
sig S1, S2 {}
Затем вы можете определить rel отношения со следующими эквивалентными синтаксисами
let rel = { x : univ, y : univ | x in S1 and y in S2 }
let rel = { x : S1, y : S2 }
let rel = S1 -> S2
посмотрев на свой фрагменте снова я заметил, что вы сдержали ваше отношение так что он сопоставляет каждый элемент в S1 точно одному элементу в S2, если вы хотите, чтобы это было неограниченное отношение, вы должны написать 'rel: set S2' –
Спасибо за ответ. Это помогает –