理解合金中的签名-Java 学习之路

我在合金网站上看到签名定义了一套 . 鉴于这个定义，我试图理解下面的合金代码：

enum dooroptype { unlocked, locked, opened}
enum enginetype {on,off}
enum motortype { ismoving, still}
enum key_location { in_car, faralone}

abstract sig state{
  inside,far, near : set Person,
  car_action : motortype,
  engine : enginetype,
  key_position : (Person + key_location),
  door : dooroptype
}

如果签名实际上定义了一个集合，那么为什么我们在签名定义中有这么多参数，因为集合是一元关系？如果我错了，怎么解释这个定义 .

2 回答

2
两个小修正：
- 从技术上讲，enum enginetype {on，off}是简称
```
sig enginetype {}
one sig on, off extends engine type {}
```
所以它宣布3组，其中两组（开和关）是单身 .
- 字段key_position的声明
```
abstract sig state{
  key_position : (Person + key_location)
  }
```
确实可以被视为两个关系的联合（在状态 - >人和状态 - > key_location），但多重约束是任何状态s只有一个s.key_position值，而不是Aviad的公式所暗示的两个值 .
回复于 2024-04-25T20:36:43+08:00
2
我正在采取合金的第一步，但我会尽力回答 . 这就是你在上面的代码中所拥有的：
- dooroptype = set（一元关系），正好有3个原子 .
- enginetype =设置（一元关系）恰好有2个原子 .
- motortype =设置（一元关系）恰好有2个原子 .
- key_location =设置（一元关系）恰好有2个原子 .
- state =具有0个或更多原子的set（一元关系） .
- inside，far和near =二元关系定义为 state -> set Person
- car_action =二元关系定义为 state -> one motortype
- engine =二进制关系定义为 state -> one enginetype
- key_position =两个二元关系 state -> Person 和 state -> key_location 的并集（但具有多重性，将每个状态限制为最多出现一次，因此状态可以与 Person 或 key_location 关联，但不能与两者关联）
- door =二元关系定义为 state -> dooroptype
简而言之，上面定义的所有内容都是关系，有些是一元的，有些是二元的 . 二元关系 inside, far and near 用 set multiplicity定义，而所有其他关系用多重性1定义 .

换句话说，签名是一个集合，关系在签名内定义，但是全局可见 .
回复于 2024-04-25T20:36:43+08:00

理解合金中的签名

2 回答

相关问题