Friday, 13 September 2013

How do we simulate switch case in Alloy?

How do we simulate switch case in Alloy?

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

No comments:

Post a Comment