Кодирование семантики абстрактных ключевых слов в Alloy с помощью ограничений

Я хотел бы закодировать семантику ключевого слова abstract как ограничение в Alloy (проявите терпение, мне нужно сделать это не просто так! :) ). если у меня есть следующий код:

abstract sig A {}
sig a1 extends A{}
sig a2 extends A{}

Я думаю, что его смысл будет следующим (надеюсь, я прав!):

sig A {}
sig a1 in A{}
sig a2 in A{}

fact {
   A=a1+a2         //A is nothing other than a1 and a2
   a1 & a2 = none  // a1 and a1 are disjoint
}

поэтому две приведенные выше подписи равны (т. е. будут семантически равными):

Я очень хочу использовать ключевое слово Abstract, которое Alloy предоставляет, чтобы упростить жизнь, но проблема возникает, когда я делаю A подмножеством sig O и использую ключевое слово abstract:

sig O{}
abstract sig A in O{}
sig a1 extends A{}
sig a2 extends A{}

приведенный выше синтаксис возвращает ошибку! Alloy жалуется: «Подпись подмножества не может быть абстрактной», поэтому мой первый вопрос: Почему Alloy не допускает этого?

Я не останавливаюсь и не кодирую семантику абстрактного ключевого слова (как объяснялось выше) и прихожу к следующему коду:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}

fact {
    A=a1+a2             // A can not be independently instantiated
    a1 & a2 = none      // a1 and a2 are disjoint
}

И это работает, и все в порядке :)

Теперь, если я хочу добавить a3 к моей спецификации Alloy, мне нужно настроить мою спецификацию следующим образом:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}
sig a3 in A{}

fact {
    A=a1+a2+3           
    a1 & a2 = none  
    a1 & a3 = none
    a2 & a3 = none
}

Но, как вы видите, сравнивая две приведенные выше спецификации, если я хочу продолжить это и добавить a4 аналогичным образом к моей спецификации, мне нужно еще больше изменить фактическую часть, а это по-прежнему создает проблемы! На самом деле количество выражений ai & aj =none (для i=1..n) возрастает немонотонно! т. е. добавление a4 вынуждает меня добавить более одного ограничения:

fact {
    A=a1+a2+3 +a4           
    a1 & a2 = none  
    a1 & a3 = none
    a1 & a4 = none
    a2 & a3 = none
    a2 & a4 = none
    a3 & a4 = none

}

Итак, мой второй вопрос: Есть ли обходной путь (или, возможно, более простой способ) для этого?

Любой комментарий приветствуется. Спасибо :)


encoding abstract alloy
person qartal    schedule 21.08.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

По вопросу 1 (почему Alloy не позволяет расширять подписи подмножеств?): я не знаю.

В Q2 (есть ли обходной путь): самый простой обходной путь - сделать a1 ... an субсигнатурой (расширением) A и найти другой способ установить отношение A и O. В простых примерах, которые вы привели, O не имеет подтипов, поэтому сработает простая замена A in O на A extends O.

Если O уже разделен другими сигнатурами, которые вы нам не показали, то этот обходной путь не работает; невозможно сказать, что будет работать без более подробной информации. (В идеале вам нужен минимальный полный рабочий пример для иллюстрации трудности: приведенные вами примеры минимальны и иллюстрируют одну трудность, но они не иллюстрируют, почему A не может быть расширением O.)

[Дополнение]

В комментарии вы говорите

Причина [по которой я использовал A в O вместо A extends O] заключается в том, что в O есть другая подпись C, которая здесь не показана. A и C не обязательно не пересекаются, поэтому я думаю, что должен использовать in вместо extend при определении их как подмножества O.

Дьявол кроется в деталях, но вывод не следует из изложенных посылок. Если A и C оба расширяют O, они будут непересекающимися, но если один использует extend, а другой использует in, они не становятся непересекающимися автоматически. Поэтому, если вы хотите, чтобы каждый из A и C был подмножеством O, а A был разделен несколькими другими сигнатурами, это можно сделать (если нет других ограничений, которые еще не упомянуты).

sig O {}
abstract sig A extends O {}
sig a1, a2 extends A {}
sig a3, a4 extends A {}
sig C in O {}
person C. M. Sperberg-McQueen    schedule 21.08.2014
comment
Спасибо за ваш комментарий. Вы правы, есть причина, по которой я использовал A in O вместо A extends O! Причина в том, что есть еще одна подпись C в O, которая здесь не показана. A и C не обязательно не пересекаются, поэтому я думаю, что должен использовать in вместо extend при определении их как подмножества O. - person qartal; 22.08.2014