为何Alloy Analyzer会重复生成相同的解决方案？

示例 #

运行以下Alloy模型时，明明只存在一种可行解决方案，但工具却多次重复生成它。有没有办法避免重复输出？

open util/integer

abstract sig Robot {
    capability: set Capability,
}

abstract sig Capability {
    do: set AtomicTask
}

abstract sig AtomicTask {
    x: one Int,
    y: one Int
}

fact{all rt: Capability | #capability.rt=1} //所有出现的Capability必须分配给一个机器人
fact{all r: Robot | #r.capability.do>0} //所有出现的Robot必须分配任务
fact{all rt: Capability | #rt.do>0} //所有出现的Capability必须分配任务
fact{all r:Robot | #r<=1} //每个Robot最多出现一次

// ----------------机器人：

sig r2 extends Robot{}
{disj[capability ,  Capability-r2at2-r2at3-r2at4]}
fact{#r2<=1}

// ----------------能力：

sig r2at2 extends Capability{}
{all d:do | d in at2}
sig r2at3 extends Capability{}
{all d:do | d in at3}
sig r2at4 extends Capability{}
{all d:do | d in at4}

fact{#r2at2<=1
#r2at3<=1
#r2at4<=1
} //机器人能力最多出现一次（如果机器人存在且能力已分配任务）

// ----------------原子任务：

abstract sig at2,at4,at3 extends AtomicTask {}
fact{all a:at2 | #do.a=1}   //所需机器人数量
fact{all a:at4 | #do.a=1}   //所需机器人数量
fact{all a:at3 | #do.a=1}   //所需机器人数量
sig at4_1 extends at4{} {x=10 y=5}
sig at3_2 extends at3{} {x=10 y=5}
sig at2_3 extends at2{} {x=10 y=5}
fact{#at4_1=1
#at3_2=1
#at2_3=1
}

// ----------------谓词：

pred TaskAllocation{
}

// ----------------约束：

 fact {all at: at4| one d: do.at | d in r2.capability}
 fact {all at: at3| one d: do.at | d in r2.capability}
 fact {all at: at2| one d: do.at | d in r2.capability}

// ----------------运行命令：

run TaskAllocation for
7 Int, 3 Capability, exactly 3 AtomicTask, 1 Robot

文本格式的输出结果如下：

---INSTANCE---
---INSTANCE---
integers={-64, -63, -62, -61, -60, -59, -58, -57, -56, -55, -54, -53, -52, -51, -50, -49, -48, -47, -46, -45, -44, -43, -42, -41, -40, -39, -38, -37, -36, -35, -34, -33, -32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63}
univ={-1, -10, -11, -12, -13, -14, -15, -16, -17, -18, -19, -2, -20, -21, -22, -23, -24, -25, -26, -27, -28, -29, -3, -30, -31, -32, -33, -34, -35, -36, -37, -38, -39, -4, -40, -41, -42, -43, -44, -45, -46, -47, -48, -49, -5, -50, -51, -52, -53, -54, -55, -56, -57, -58, -59, -6, -60, -61, -62, -63, -64, -7, -8, -9, 0, 1, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 2, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 3, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 4, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 5, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 6, 60, 61, 62, 63, 7, 8, 9, at2_3$0, at3_2$0, at4_1$0, r2$0, r2at2$0, r2at3$0, r2at4$0}
Int={-1, -10, -11, -12, -13, -14, -15, -16, -17, -18, -19, -2, -20, -21, -22, -23, -24, -25, -26, -27, -28, -29, -3, -30, -31, -32, -33, -34, -35, -36, -37, -38, -39, -4, -40, -41, -42, -43, -44, -45, -46, -47, -48, -49, -5, -50, -51, -52, -53, -54, -55, -56, -57, -58, -59, -6, -60, -61, -62, -63, -64, -7, -8, -9, 0, 1, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 2, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 3, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 4, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 5, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 6, 60, 61, 62, 63, 7, 8, 9}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/Robot={r2$0}
this/Robot<:capability={r2$0->r2at2$0, r2$0->r2at3$0, r2$0->r2at4$0}
this/r2={r2$0}
this/Capability={r2at2$0, r2at3$0, r2at4$0}
this/Capability<:do={r2at2$0->at2_3$0, r2at3$0->at3_2$0, r2at4$0->at4_1$0}
this/r2at2={r2at2$0}
this/r2at3={r2at3$0}
this/r2at4={r2at4$0}
this/AtomicTask={at2_3$0, at3_2$0, at4_1$0}
this/AtomicTask<:x={at2_3$0->10, at3_2$0->10, at4_1$0->10}
this/AtomicTask<:y={at2_3$0->5, at3_2$0->5, at4_1$0->5}
this/at2={at2_3$0}
this/at2_3={at2_3$0}
this/at4={at4_1$0}
this/at4_1={at4_1$0}
this/at3={at3_2$0}
this/at3_2={at3_2$0}

原因分析 #

Alloy Analyzer默认会生成所有满足约束的实例，包括结构完全相同的同构实例——这些实例只是元素的内部标识符（比如r2$0）不同，但实际逻辑结构完全一致。你的模型已经通过exactly和#sig=1等约束固定了唯一的逻辑解，但工具默认不会自动过滤同构实例，所以会重复输出看起来一样的结果。

解决方法 #

• 开启同构实例过滤：在Alloy Analyzer的运行窗口中，找到"Options"选项，勾选"Suppress isomorphic instances"（抑制同构实例）。这样工具会自动识别并跳过结构相同的实例，只输出唯一的逻辑解。
• 确认模型约束的严谨性：你的模型已经通过#at4_1=1、exactly 3 AtomicTask等约束固定了每个元素的实例数量，确保了逻辑上只有唯一解，所以开启过滤后就能解决重复问题。

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