экспресс-эквивалентность между несколькими экземплярами

Question

Предположим, у меня есть значи А в моем модуле, который связан с сиг В.

Представьте теперь, что у нас есть несколько примеров:

A$1 -> B$1 , A$2 -> B$2 

и

A$1 -> B$2 , A$2 -> B$1 

Я хотел бы выразить, что B $ 1 и B $ 2 эквивалентны (при определенных условиях), что только этот экземпляр будет генерироваться A$1 -> B , A$2 -> B.

Одним из решений может быть использование ключевого слова «один» при объявлении sig B, но в моем случае это не сработает, потому что B имеет несколько полей, что делает атомы B не обязательно эквивалентными. Короче говоря, 2 атома эквивалентны, только если у них есть поля одинаковых значений.

В идеале я хотел бы удалить нумерацию для B., но все же иметь возможность иметь несколько атомов B.

Answer 1

Анализатор сплавов не дает вам большого контроля над тем, как генерируются последующие экземпляры (или как сломать симметрии), поэтому вам обычно приходится обойти эти проблемы на уровне модели.

Для примера, может быть, это правильная модель

sig B{} 

one sig BA extends B {} 

sig A { 
    b: one BA 
} 

run { #A=2 } 

Answer 2

Сначала вы сказать, что два экземпляра, которые вы описываете эквивалентны, хотя на поверхностном уровне они появляются, чтобы иметь различные значения для A $ 1 и $ 2 , Затем вы говорите: «2 атома эквивалентны, только если ... их поля имеют одинаковые значения». Если это определение эквивалентности, то ваши два экземпляра не эквивалентны; если ваши два экземпляра эквивалентны, то ваше определение не захватывает то, что вы хотите.

Звучит так, как будто вы имеете в виду (1), что атомы B либо (1a) всегда эквивалентны, либо (1b) эквивалентны при определенных обстоятельствах, и (2) что атомы A эквивалентны, если их поля имеют значения, которые либо идентичны, либо эквивалентны. И как будто вы хотите запретить эквивалентные атомы А. Если это так, то ваши рабочие места:

• Определите предикат, который является истинным для двух элементов B тогда и только тогда, когда они эквивалентны.
• Определить предикат для двух элементов A, которые являются истинными тогда и только тогда, когда они эквивалентны.
• Определите предикат (или факт), который указывает, что два атома А в экземпляре не эквивалентны.

Если ваша проблема заключается в том, что анализатор показывает вам примеры модели, которые не интересны друг от друга, а затем см. Ответ Aleksandar Milicevic.