如何在Alloy Analyzer中固定索引避免生成等效重复模型？

我需要将机器分配给操作员，每台机器对应固定的任务集合，例如machine1类机器可执行work1、work2类任务。以下是2名操作员（operator1、operator0）和3台机器（machine1_0、machine1_1、machine2）的简单输出示例。

当前遇到的问题是Alloy会生成大量冗余模型：不同模型的任务分配逻辑完全一致，仅任务的索引标识发生了变化。例如第一个模型中：

machine1_0 -> do -> {work1_1 , work2_2}
machine1_1 -> do -> {work1_0 , work2_1}

另一逻辑完全相同的模型中：

machine1_0 -> do -> {work1_0 , work2_2}
machine1_1 -> do -> {work1_1 , work2_1}

我需要将生成的模型输入到另一款软件处理，因此需要避免这类重复模型生成，要求所有输出模型中，machine1_0始终绑定固定的work1类和work2类任务。

现有代码如下：

sig operator{
    runs: set Machine
}

abstract sig Machine{
    do: set Work
}
fact {all m:Machine | #runs.m = 1}
fact {all m:Machine | disj [m.do , (Machine-m).do ] }
fact{all w:Work | #(do.w) >= 1 }

sig machine1 extends Machine{}{
    #do = 2
    not disj [do , work1]
    not disj [do , work2]
}

sig machine2 extends Machine{}{
    #do = 2
    not disj [do , work2]
    not disj [do , work3]
}

abstract sig Work{}

sig work1 extends Work{}
sig work2 extends Work{}
sig work3 extends Work{}

pred checktime{}

run checktime for exactly 2 operator, exactly 2 machine1, exactly 1 machine2, 6 Work

注：本简单示例中Alloy不会生成重复模型，但当任务、机器、操作员数量上升时会出现该问题。

该问题由Alloy默认保留同类型原子的对称性导致，仅原子索引不同的等价实例会被判定为不同模型输出，主动打破对称性即可解决，两种常用实现方案如下：

方案1：直接固定首个machine1实例的绑定关系 #

新增事实规则，强制第一个machine1实例（即machine1_0）绑定work1、work2类的首个实例，代码修改量最小，直接新增如下fact即可：

fact 固定machine1_0任务绑定 {
    let m0 = machine1.first |
        one w1: work1.first |
        one w2: work2.first |
        m0.do = w1 + w2
}

该方案完全匹配需求，修改后不会再出现仅任务索引交换的冗余实例。

方案2：引入排序模块统一管理绑定 #

如果后续需要扩展更多固定绑定规则，可以导入Alloy内置的排序模块给对应sig全局排序，再统一配置绑定规则：

1. 代码开头导入排序模块：

open util/ordering[work1]
open util/ordering[work2]
open util/ordering[machine1]

2. 新增绑定规则：

fact {
    first[machine1].do = first[work1] + first[work2]
}

两种方案均可直接消除冗余模型，方案1更轻量，适合当前场景使用。

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