Keep the same index in Alloy Analyzer?

Question

I want to allocate a machines to operators. Each machine has a fix set of works (e.g., machine1 does work2 and work). Here a simple output example with 2 operators (operator1,operator0) and 3 machines (machine1_0,machine1_1,machine2):

The problem is that it generates more models than neccesary because it create models with the same "works" but changing the index. For example, in one model:

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

and in other (identical allocation)

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

I need these repeated models to be avoided as I pass this model to a second software.

I want machine1_0 to stick with the same work1_x and work2_y for all output models.

Any suggestions? Thanks.

Code:

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

(Note. For this simple example Alloy do not repeat models but when the number of tasks, machines and operators grow.)

Answer 1

From my understanding of your problem, you would like that there is at most one work1, at most one work2, and at most one work3 in your instances.

To reach this effect, you can simply add the desired multiplicity to your signature declaration:

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