为什么在箭头表达式中使用字段时会有所不同

Question

以下签名描述照片管理应用程序的状态：

sig ApplicationState {
catalogs: set Catalog,
catalogState: catalogs -> one CatalogState
}

签名当然会创建一个集合。在这种情况下，它会创建一组ApplicationStates:

ApplicationState0
ApplicationState1
...

目录是一个字段。它将每个ApplicationState映射到一组Catalog值：

ApplicationState0, Catalog0
ApplicationState0, Catalog1
ApplicationState1, Catalog0
...

catalogState也是一个字段。它将每个ApplicationState映射到一个关系。关系是：

catalogs -> one CatalogState

这种关系表示：将目录的每个值映射到一个CatalogState值。我们已经看到了目录，我将在这里重复：

ApplicationState0, Catalog0
ApplicationState0, Catalog1
ApplicationState1, Catalog0
...

因此，关系是将这些元组中的每一个映射到一个CatalogState，就像这样：

ApplicationState0, Catalog0, CatalogState0
ApplicationState0, Catalog1, CatalogState0
ApplicationState1, Catalog0, CatalogState0
...

好的，回到编目状态。前面我们说过它将每个ApplicationState映射到一个关系，我们刚刚看到了这个关系是什么。所以，我相信catalogState表示arity=4的关系，就像这样：

ApplicationState0, ApplicationState0, Catalog0, CatalogState0
ApplicationState0, ApplicationState0, Catalog1, CatalogState0
ApplicationState0, ApplicationState1, Catalog0, CatalogState0
...

但是，当我运行Alloy Evaluator时，它说catalogState是一个三元关系。我从这个例子中得到的结论是：

1. 通常字段名表示一个关系。

2. 箭头表达式中使用的字段名并不表示关系。相反，它表示关系的第2列(关系的范围)。

是这样吗？这在《软件摘要》一书中有何解释？

Answer 1

软件摘要第4.2.2节(第二版第97页)开始

关系被声明为签名的字段。

我认为，这至少解决了你的部分问题。(我认为浏览"字段"和关系的索引条目并阅读它们指向的每一节可能会有所帮助。)

你说

箭头表达式中使用的字段名并不表示关系。相反，它表示关系的第2列(关系的范围)。

这听起来可能有些迂腐，但不是：字段名总是表示关系。然而，在签名声明的上下文中，它们隐式地以this.为前缀，这将删除关系的第一列。在声明catalogState: catalogs -> one CatalogState中，对catalogs的引用实际上是对ApplicationState和Catalog上的二进制关系的引用。然而，在这种情况下，它被静默地扩展为this.catalogs，它计算为一组Catalog个体。关键字this在软件摘要的第4.2.2节中介绍。

在您的示例中，声明上的基数约束也可能是一个复杂的因素；我不想在这里解释它们的影响。我只想说，当我遇到基数约束的问题时，我经常发现，非常仔细地阅读附录B中语言参考的相关部分，通常就足以让我理解发生了什么