Как мы моделируем случай переключения в Alloy?

Question

У меня есть модель сплава, которая должна иметь некоторые правила, такие как

abstract sig country {}

one sig US extends country {}
one sig UK extends country {}
one sig DE extends country {}
one sig CA extends country {}

abstract sig currencyCode {}

one sig USD extends currencyCode {}
one sig GBP extends currencyCode {}
one sig CAD extends currencyCode {}
one sig EUR extends currencyCode {}

abstract sig location {}

one sig NewYork extends location {}
one sig Vancouver extends location {}
one sig London extends location {}
one sig Munich extends location {}

Поэтому я хочу установить правило, чтобы всякий раз, когда экземпляр выбирал США, он также выбирал доллары США и Нью-Йорк. Если он выберет доллары США, то он выберет США и Нью-Йорк, что означает, что страна, местоположение и валюта будут сгруппированы вместе. Я попытался использовать следующий факт, чтобы сделать это, но это не работает. Каковы недостатки в том, и есть ли способ сделать это?

 fact UKRL {
    all a: itemType.site, 
        b: item.country, 
        c: item.currency, 
        d: startPrice.currencyId, 
        e: item.locationLink |
    (a in UK) <=> (b in UK)  <=>  (c in GBP)  <=>  (d in GBP)  <=>  (e in London)
}

fact DERL {
    all a: itemType.site, 
        b: item.country, 
        c: item.currency, 
        d: startPrice.currencyId, 
        e: item.locationLink |
    (a in DE) <=> (b in DE)  <=>  (c in EUR)  <=>  (d in EUR)  <=>  (e in Munich)
}

Answer 1

Вы недостаточно демонстрируете свою работу, чтобы обеспечить надежное воспроизведение проблемы, поэтому любой ответ будет основан на предположении. Я предполагаю, что вы разрешаете использование нескольких элементов и хотите, чтобы каждый элемент был связан с какой-либо страной, но вы хотите, чтобы разные элементы могли быть связаны с разными странами.

Ваши текущие формулировки фактов UKRL и DERL имеют несколько проблем.

Во-первых, я предполагаю, что вы пытаетесь потребовать, чтобы для любого элемента его страна, валюта и locationLink были согласованы друг с другом (я неофициально использую слово "непротиворечивый"). Но каждый из двух ваших фактов ограничивает не страну, валюту и locationLink одного элемента, а все значения во второй позиции отношений страны, валюты и locationLink. Таким образом, тот факт, что UKRL означает, говоря по-английски: либо (a) у всех itemTypes есть сайт 'UK', и у всех товаров есть страна 'UK', а у всех валют предметов - 'GBP', а у всех идентификаторов валют startPrice - 'GBP', и все ссылки на местоположение элемента - "Лондон", иначе (б) ни одно из них не является правдой.

Задайте себе вопрос: что произойдет, если у меня есть два товара: один со страной Великобритания, валютой CAD и местоположением Лондон, а другой со страной CA, валютой EUR и местоположением Мюнхен? Удовлетворяет ли это факт или нет? Как насчет того, что DERL?

Если вы хотите, чтобы каждый экземпляр вашей модели был настроен для одной страны (со всеми элементами, имеющими одинаковую страну, валюту и ссылку на местоположение), то ваши квантификаторы в порядке, но ваше ограничение не говорит то, что вы хотите сказать, То, что вы хотите сказать: либо все настроено для Великобритании, либо все настроено для Германии, либо все настроено для Канады, либо все настроено для США. Если бы это был я, я бы попробовал определение предиката, который является истинным, если и только если все настроено для Великобритании - очень похоже на ваш факт UKRL, но с использованием AND, а не <=>, и предиката, а не факта. Тогда я бы определил еще три, для других стран. Затем я определил бы окончательный предикат (вы можете сделать это фактом, если хотите, но я обычно нахожу, что определение вещей как предикатов помогает мне легче экспериментировать), в котором говорится, что либо UKpred, либо DEpred, либо CApred, либо USpred должны быть истинными.

Если вы хотите, чтобы разные элементы в одном и том же экземпляре модели могли иметь разные страны, вам нужно дать количественную оценку по элементам, а не по item.country (и т. Д.).

Надеюсь, это поможет.