如何在Alloy中将Couple关系表示为Man指向Woman的箭头？

不用重构原模型，只需要两步就能实现你的需求，同时保留原Couple的所有约束：

1. 在原模型中导出配偶关系 #

给原模型加一个fun来定义从Man到Woman的配偶关联，直接复用Couple里的husband和wife字段，不用额外写约束：

abstract sig Person {}

sig Man, Woman extends Person {}
sig Couple {
   husband: disj lone Man,
   wife: dis lone Woman,
}

// 导出Man到Woman的配偶关系
fun spouse: Man -> Woman {
  c: Couple | c.husband -> c.wife
}

run {} for 4

2. 在可视化界面调整显示 #

运行模型后，在Alloy的可视化窗口里：

• 左上角的sig列表里，取消勾选Couple，隐藏这个节点类型
• 在关系列表里，勾选刚定义的spouse，这样就会显示Man指向Woman的箭头，代表二者的配偶关联

为什么这个方案更优 #

原模型里的disj和lone已经帮你保证了核心约束：

• 每个Man最多只能是一个Couple的丈夫
• 每个Woman最多只能是一个Couple的妻子
• 每个Couple最多有一个丈夫和一个妻子

你之前的方案需要手动添加这些约束（比如限制Man的spouse只能是Woman、双向一致性、唯一性等），反而冗余。这个方法完全复用原模型的约束，只做显示层面的调整。

内容的提问来源于stack exchange，提问作者PULKIT AGRAWAL