How do we simulate switch case in Alloy?

Question

I have an Alloy Model which needs to have some rules like

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

So I want to set up a rule, such that whenever the instance pick US, it will also pick USD and NewYork. If it picks USD, then it will pick US and NewYork, which means the country, location and currency will be grouped together. I tried to use the following fact to do this, but it's not working. What's the flaws in the fact and is there anyway to do this?

 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

You don't show enough of your work to allow the problem to be reproduced reliably, so any answer will be based on conjecture. I conjecture that you are allowing multiple items, and you want each item to be associated with some country, but you want it to be possible for different items to be associated with different countries.

Your current formulations of facts UKRL and DERL have a couple of problems.

First, I guess you are trying to require that for any item, its country, currency, and locationLink should be consistent with each other (I use the word 'consistent' informally). But your two facts each constrain not the country, currency, and locationLink of a single item, but of all the values in the second position of the country, currency, and locationLink relations. So the fact UKRL means, put into English: either (a) all itemTypes have site 'UK', and all items have country 'UK', and all item currencies are 'GBP' and all startPrice currency IDs are 'GBP' and all item location links are 'London', or else (b) none of these is true.

Ask yourself: what happens if I have two items, one with country UK, currency CAD, and location London, and one with country CA, currency EUR, and location Munich? Does it satisfy the fact or not? What about the fact DERL?

If you want each instance of your model to be set up for a single country (with all items having the same country, currency, and location link), then your quantifiers are fine, but your constraint is not saying what you want it to say. What you want it to say is: either everything is set up for the UK, or everything is set up for Germany, or everything is set up for Canada, or everything is set up for the U.S. If it were me, I'd try defining a predicate that's true if and only if everything is set up for the UK -- very similar to your fact UKRL, but using AND, not <=>, and a predicate, not a fact. Then I'd define three more, for the other countries. Then I'd define a final predicate (you can make it a fact if you wish, but I generally find defining things as predicates helps me experiment more easily) that says either UKpred or DEpred or CApred or USpred must be true.

If you want different items in the same model instance to be allowed to have different countries, then you need to quantify over items, not over item.country (etc.).

I hope this helps.