Предикаты и Int в сплаве

Я знаю использование предикатов в сплаве, но я был немного удивлен приведенным ниже описанием:

pred locationConstraint(loc: Int -> Int){
    loc in (Int[0] + Int[1] + Int[2] + Int[3] + Int[4] + Int[5] + Int[6]) -> (Int[2] + Int[3])
 + (Int[2] + Int[3]) -> (Int[0] + Int[1] + Int[2] + Int[3] + Int[4] + Int[5])

}

Может кто-нибудь объяснить мне вышеизложенное.


alloy
person Programmer    schedule 17.11.2012    source источник
comment
Кто бы ни проголосовал за этот вопрос, он может показаться вам глупым вопросом, но SO настолько скудна в информации о Alloy, что каждая мелочь помогает.   -  person Aviad P.    schedule 18.11.2012

Ответы (1)


arrow_upward
1
arrow_downward

Добавьте run {} к вашей модели и введите {x,y:Int | locationConstraint[x->y]} в оценщик, чтобы получить результат:

введите здесь описание изображения

person Aviad P.    schedule 18.11.2012
comment
2 небольших вопроса. Что означает Int[0]? Как вы интерпретируете выражение (Int[0] + Int[1]) -> (Int[2] + Int[3]). Не могли бы вы объяснить вышеизложенное в текстовой форме. Большое спасибо :) - person Programmer; 19.11.2012
comment
Int[0] означает одноэлементный набор атома Int, который представляет нулевое значение. Int[0] + Int[1] представляет собой объединение двух таких одноэлементных множеств, то есть подмножество Int, содержащее атомы 0 и 1. - person Aviad P.; 19.11.2012
comment
На ваш второй вопрос {a+b+c} -> {d+e+f} означает бинарное отношение между множеством {a,b,c} и {d,e,f}, которое содержит все возможные пары, т.е. это декартово произведение двух множеств. Другими словами, это полный двудольный ориентированный граф (см.) двух наборов вершин {a,b,c} и {d,e,f}. - person Aviad P.; 19.11.2012