0

我有一个合金模型，它需要有一些规则，比如

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

所以我想设置一个规则，这样每当实例选择美国时，它也会选择美元和纽约。如果它选择 USD，那么它将选择 US 和 NewYork，这意味着国家、地点和货币将被组合在一起。我试图使用以下事实来做到这一点，但它不起作用。事实有什么缺陷，有什么办法吗？

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

1 回答 1

0

您没有展示足够的工作来可靠地重现问题，因此任何答案都将基于猜想。我猜想您允许多个项目，并且您希望每个项目与某个国家/地区相关联，但您希望不同的项目可以与不同的国家/地区相关联。

您当前对事实 UKRL 和 DERL 的表述有几个问题。

首先，我猜您试图要求任何项目的国家、货币和 locationLink 应该彼此一致（我非正式地使用“一致”这个词）。但是您的两个事实都不是限制单个项目的国家、货币和 locationLink，而是限制国家、货币和 locationLink 关系的第二个位置的所有值。因此，UKRL 的意思是，用英语表示：（a）所有 itemTypes 都有站点“UK”，所有项目都有国家“UK”，所有项目货币都是“GBP”，所有 startPrice 货币 ID 都是“GBP”并且所有项目位置链接是“伦敦”，否则 (b) 这些都不是真的。

问问自己：如果我有两件商品，一件带有国家/地区、货币 CAD 和位置伦敦，一件带有国家/地区、货币欧元和位置慕尼黑，会发生什么？是否满足事实？那么DERL的事实呢？

如果您希望为单个国家/地区设置模型的每个实例（所有项目都具有相同的国家、货币和位置链接），那么您的量词很好，但您的约束并没有说出您想要它说的内容. 你想说的是：要么一切都为英国设置，要么一切都为德国设置，要么一切都为加拿大设置，或者一切都为美国设置如果是我，我会尝试定义一个谓词，当且仅当所有内容都为英国设置时才为真 - 与您的事实 UKRL 非常相似，但使用 AND，而不是 <=>，并且使用谓词，而不是事实。然后我会为其他国家定义另外三个。然后我会定义一个最终谓词（如果你愿意，你可以让它成为事实，

如果您希望允许同一模型实例中的不同项目具有不同的国家/地区，那么您需要对项目进行量化，而不是对 item.country （等）进行量化。

我希望这有帮助。

于 2013-09-16T00:59:07.363 回答