如何在Alloy 6中定义具备对称性与有序性的电梯楼层集合？

针对你在定义电梯运行用的有序楼层集合时遇到的问题，下面分别给出两种初始方案的改进版本，满足up/down关联对称、支持任意2层以上楼层数量、形成线性有序链的需求。

方案一：基于抽象集合的改进 #

你最初的抽象集合方案问题在于顶层/底层的关系定义错误，且缺少up/down的对称约束。以下是修正后的代码：

abstract sig Floor {}

// 顶层：仅包含下层关联，无上层
one sig TopFloor extends Floor {
    down : lone Floor
} {
    this not in down
}

// 底层：仅包含上层关联，无下层
one sig BottomFloor extends Floor {
    up : lone Floor
} {
    this not in up
}

// 中间楼层：同时拥有上层和下层关联
sig MidFloor extends Floor {
    up : one Floor,
    down : one Floor
} {
    this not in up + down
    up in Floor - BottomFloor  // 上层不能是底层
    down in Floor - TopFloor   // 下层不能是顶层
    up.down = this             // 核心：上层的下层必须是当前楼层
}

// 全局约束保证楼层链的完整性和正确性
fact FloorOrder {
    // 所有楼层都能从底层向上遍历到，也能从顶层向下遍历到
    Floor in BottomFloor.*up
    Floor in TopFloor.*down
    
    // 顶层的下层（如果存在）必须指向顶层
    TopFloor.down.up = TopFloor
    
    // 底层的上层（如果存在）必须指向底层
    BottomFloor.up.down = BottomFloor
    
    // 禁止出现循环结构
    no cycles : set Floor | cycles in cycles.*up
}

// 验证up/down对称性的断言
assert UpDownSymmetry {
    all f : Floor | f.up != none implies f.up.down = f
    all f : Floor | f.down != none implies f.down.up = f
}

// 运行示例：生成3层楼的结构
run {#Floor = 3} for 3

关键改进点 #

• 修正顶层/底层的关联定义：顶层只有down，底层只有up，避免无效的上层/下层关联
• 给中间楼层添加up.down = this约束，直接保证up与down的对称关系
• 通过全局fact确保所有楼层形成单一线性链，无循环、无分支
• 用断言验证对称性是否符合预期

方案二：基于单一集合的改进 #

你之前的单一集合方案缺少up/down的对称约束，导致关联关系不一致。以下是补充约束后的代码：

sig Floor {
    up : lone Floor,
    down : lone Floor
}

one sig bottom, top in Floor {}

fact FloorConstraints {
    // 顶层无上层，底层无下层
    no top.up
    no bottom.down
    
    // 核心对称约束：A的上层是B，当且仅当B的下层是A
    all f, g : Floor | f.up = g iff g.down = f
    
    // 所有楼层都在底层到顶层的遍历链中，保证结构完整
    Floor in bottom.*up
    Floor in top.*down
    
    // 每个楼层最多有一个上层和一个下层，避免分支结构
    all f : Floor | #f.up <= 1 and #f.down <= 1
    
    // 禁止循环
    no cycles : set Floor | cycles in cycles.*up
}

// 验证结构正确性的断言
assert ValidFloorStructure {
    all f : Floor | f.up != none implies f.up.down = f
    all f : Floor | f.down != none implies f.down.up = f
    // 除顶层外，每个楼层必有一个上层；除底层外，每个楼层必有一个下层
    all f : Floor - top | one f.up
    all f : Floor - bottom | one f.down
}

// 运行示例：生成4层楼的结构
run {#Floor = 4} for 4

关键改进点 #

• 添加all f, g : Floor | f.up = g iff g.down = f，直接绑定up和down的对称关系
• 补充约束确保每个楼层（除顶/底）都有且仅有一个上层和下层，避免分支
• 全局fact保证所有楼层形成完整的线性链，无循环
• 用断言验证整个结构的正确性

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