Alloy - Работа с неограниченными кванторами всеобщности

Question

Доброго дня,

Я испытывал проблемы с сплавом при работе с неограниченными кванторами всеобщности. Как объяснено в книге Дэниела Джексона «Абстракции программного обеспечения» (раздел 5.3 «Неограниченные универсальные квантификаторы»), сплав имеет тонкое ограничение относительно универсальных квантификаторов и проверки утверждений. Сплав производит паразитные контрпримеры в некоторых случаях, например, следующий, чтобы проверить, что множества замкнуты в рамках союза (как показано в вышеупомянутой книге):

sig Set { 
    elements: set Element 
} 
sig Element {} 

assert Closed { 
    all s0, s1: Set | some s2: Set | 
    s2.elements = s0.elements + s1.elements 
} 
check Closed for 3 

Производство контрпример, таких как:

Set = {(S0),(S1)} 
Element = {(E0),(E1)} 
s0 = {(S0)} 
s1 = {(S1)} 
elements = {(S0,E0), (S1,E1)} 

где анализатор не заполнил Set с достаточными значениями (отсутствующий Set atom, S2, содержащий объединение S0 и S1).

Два решения этой общей задачи предлагается затем в книге:

1) Объявление генератора аксиомы, чтобы заставить сплав генерировать все возможные случаи. Например:

fact SetGenerator{ 
    some s: Set | no s.elements 
    all s: Set, e: Element | 
    some s': Set | s'.elements = s.elements + e 
} 

Это решение, однако, приводит к области действия взрыва, а также может привести к несоответствиям.

2) Опустить аксиому генератора и использовать ограниченную универсальную форму для ограничений. То есть ограничивающее выражение количественной переменной не упоминает имена сгенерированных подписей. Однако не каждое утверждение может быть выражено в такой форме.

Мой вопрос: есть ли какие-либо конкретные правила для выбора любого из этих решений? Мне это не ясно из книги.

Спасибо.

Answer 1

Нет, нет конкретного правила (или, по крайней мере, нет, что я придумал). На практике это не возникает очень часто, поэтому я бы рассматривал каждый случай по мере его появления. У вас есть конкретный пример?

Также учтите, что иногда вы можете сформулировать свою проблему с квантором более высокого порядка (т. Е. Квантором по набору или соотношению), и в этом случае вы можете использовать Alloy *, расширение Alloy, которое поддерживает анализ более высокого порядка ,