Блог

Я хочу выделить машины операторам. Каждая машина имеет фиксированный набор работ (например, машина 1 выполняет работу 2 и работает). Вот простой пример вывода с 2 операторами (operator1,operator0) и 3 машинами (machine1_0,machine1_1,machine2):

Проблема в том, что он генерирует больше моделей, чем необходимо, потому что он создает модели с той же «работой s», но с изменением индекса. Например, в одной модели:

 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
 

(Примечание. Для этого простого примера мы не повторяем модели, но когда количество задач, машин и операторов растет.)

Исходя из моего понимания вашей проблемы, вы хотели бы, чтобы в ваших экземплярах было не более одной работы1, не более одной работы2 и не более одной работы3.

Чтобы достичь этого эффекта, вы можете просто добавить желаемую кратность в свою декларацию подписи:

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