0

我在合金网站上读到签名定义了一个集合。鉴于此定义，我试图理解以下合金代码：

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
}

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

4

2 回答 2

3

我正在Alloy中迈出第一步，但我会尝试回答。这就是您在上面的代码中所拥有的：

  1. dooroptype = 恰好有 3 个原子的集合（一元关系）。
  2. enginetype = set（一元​​关系）正好有 2 个原子。
  3. motortype = 恰好有 2 个原子的集合（一元关系）。
  4. key_location = 设置（一元关系）正好有 2 个原子。
  5. state = 具有 0 个或更多原子的集合（一元关系）。
  6. inside, far and near = 二元关系定义为state -> set Person
  7. car_action = 二元关系定义为state -> one motortype
  8. 引擎 = 二元关系定义为state -> one enginetype
  9. key_position = 两个二元关系的并集state -> Person和state -> key_location（但具有限制每个状态最多出现一次的多重性，因此状态可以与 aPerson或 a相关联key_location，但不能同时与两者相关联）
  10. 门 = 定义为的二元关系state -> dooroptype

简而言之，上面定义的一切都是关系，有些是一元的，有些是二元的。二元关系inside, far and near用set多重性定义，而所有其他关系用多重性定义。

换句话说，签名是一个集合，关系在签名内部定义，但全局可见。

于 2012-11-12T10:09:33.813 回答
2

两个小修正：

  1. 从技术上讲，枚举引擎类型 {on,off} 是

    sig enginetype {}
one sig on, off extends engine type {}

所以它声明了 3 个集合，其中两个（开和关）是单例。

  1. 字段 key_position 的声明

    abstract sig state{
  key_position : (Person + key_location)
  }

确实可以被视为两个关系的联合（通过 state -> Person 和 state -> key_location），但多重性约束是任何 state s 都只有一个 s.key_position 值，而不是 Aviad 公式建议的两个值.

于 2012-11-14T15:13:44.467 回答