在合金分析仪中保持相同的索引？答案

【问题标题】：Keep the same index in Alloy Analyzer?在合金分析仪中保持相同的索引？
【发布时间】：2021-09-10 10:32:08
【问题描述】：

我想将机器分配给操作员。每台机器都有一组固定的工作（例如，机器 1 完成工作 2 并工作）。这里有一个简单的输出示例，有 2 个操作员（operator1,operator0）和 3 台机器（machine1_0,machine1_1,machine2）：

问题在于它生成的模型比必要的要多，因为它创建的模型具有相同的“works”，但会更改索引。例如，在一个模型中：

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_x 和 work2_y。

有什么建议吗？谢谢。

代码：

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 model-checking

【解决方案1】：

根据我对您的问题的理解，您希望您的实例中最多有一个 work1、最多一个 work2 和一个 work3。

要达到此效果，您只需将所需的多重性添加到您的签名声明中：

abstract sig Work{}
lone sig work1,work2 ,work3 extends Work{}

【讨论】：