Alloy建模有序幻灯片演示文稿：单归属约束问题排查

• 核心冲突：你用Int one -> lone Slide定义演示文稿的幻灯片映射，这种结构允许同一个幻灯片被多个演示文稿的Int键关联，即便添加单归属事实，求解器在默认作用域下很难找到同时满足每个演示文稿至少2张幻灯片、所有幻灯片被包含、幻灯片仅属于一个演示文稿的合法实例。
• 语义误解：one -> lone的含义是每个Int对应最多一个幻灯片，但并未限制幻灯片只能被一个Int（或一个演示文稿）关联，加上单归属约束后，映射关系的复杂度超出了求解器在默认小作用域内的求解能力。

1. 基础签名定义 #

用seq替代Int映射，因为seq天然维护有序性，且每个序列属于独立的演示文稿，便于约束单归属：

sig Presentation {
  slides: seq Slide  // 有序幻灯片列表，seq自带顺序属性
}

sig Slide {}

2. 添加核心约束 #

• 幻灯片单归属：确保每张幻灯片仅出现在一个演示文稿的序列中

  fact SingleOwnership {
    all s: Slide | one p: Presentation | s in p.slides.elems
  }
  

• 演示文稿最小幻灯片数：每个演示文稿至少包含2张幻灯片

  fact MinSlidesPerPresentation {
    all p: Presentation | #p.slides >= 2
  }
  

3. 后续重排逻辑的扩展基础 #

seq的特性很适合实现幻灯片重排需求：

• 若要定义重排后的序列是原序列的排列，可使用seq/permutation关系：all p, p': Presentation | p'.slides is permutation of p.slides
• 若要添加位置限制（如某张幻灯片不能在第一个位置），可直接通过序列索引约束：all p: Presentation | p.slides[0] != s0（其中s0是指定幻灯片）

4. 验证实例的Run命令 #

添加合理的作用域限制，帮助求解器快速找到实例：

run {} for 2 Presentation, 4 Slide

内容的提问来源于stack exchange，提问作者Marko Mušnjak