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

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

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)
}

alloy
person user2744486    schedule 13.09.2013    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

У ваших нынешних формулировок фактов у УКРЛ и ДЕРЛ есть пара проблем.

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

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

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

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

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

person C. M. Sperberg-McQueen    schedule 16.09.2013