Why do Alloy Analyzer generates the same solution multiple times?
As a dummy example, consider the next Alloy model. If you run code in the Alloy Analyzer it generates a solution (just one solution is possible) but generated multiple times. Is there a way to avoid repeating the same output?
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} //all Capability appearing must be assigned to a robot
fact{all r: Robot | #r.capability.do>0} //all Robots appearing must have assigned tasks
fact{all rt: Capability | #rt.do>0} // all capability appearing must have assigned tasks
fact{all r:Robot | #r<=1} // all robots appears max. once
// ----------------ROBOTS:
sig r2 extends Robot{}
{disj[capability , Capability-r2at2-r2at3-r2at4]}
fact{#r2<=1}
// ----------------CAPABILITIES:
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
} // robot capabilities appear once (if robot appears, and if capab. tasks assigned)
// ----------------ATOMIC TASKS:
abstract sig at2,at4,at3 extends AtomicTask {}
fact{all a:at2 | #do.a=1} // number of robots needed
fact{all a:at4 | #do.a=1} // number of robots needed
fact{all a:at3 | #do.a=1} // number of robots needed
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
}
// ----------------PREDICATE:
pred TaskAllocation{
}
// ----------------CONSTRAINTS:
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 COMMAND:
run TaskAllocation for
7 Int, 3 Capability, exactly 3 AtomicTask, 1 Robot
The result shown in text format is:
---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}
I rewrote your example because some parts, in particular those related to multiplicities (one, lone), weren't very idiomatic; and also because I suspected this had an impact on your problem. This is likely because adding multiplicities gives more information about your model than the use of additional constraints featuring the cardinality operator. Seems this was the way to go as this indeed removes the issue:
open util/integer
abstract sig Robot {
capability: set Capability,
}
abstract sig Capability {
do: some AtomicTask // all capability appearing must have assigned tasks
}
abstract sig AtomicTask {
x: one Int,
y: one Int
}
fact {
capability in Robot one -> Capability //all Capability appearing must be assigned to a robot
capability.do in Robot -> some AtomicTask //all Robots appearing must have assigned tasks
}
// ----------------ROBOTS:
lone sig r2 extends Robot{}
{disj[capability , Capability-r2at2-r2at3-r2at4]}
// ----------------CAPABILITIES:
lone sig r2at2 extends Capability{}// robot capabilities appear once (if robot appears, and if capab. tasks assigned)
{all d:do | d in at2}
lone sig r2at3 extends Capability{}
{all d:do | d in at3}
lone sig r2at4 extends Capability{}
{all d:do | d in at4}
// ----------------ATOMIC TASKS:
abstract sig at2,at4,at3 extends AtomicTask {}
fact{all a:at2 | one do.a } // number of robots needed
fact{all a:at4 | one do.a } // number of robots needed
fact{all a:at3 | one do.a } // number of robots needed
one sig at4_1 extends at4{} {x=10 y=5}
one sig at3_2 extends at3{} {x=10 y=5}
one sig at2_3 extends at2{} {x=10 y=5}
// ----------------PREDICATE:
pred TaskAllocation{
}
// ----------------CONSTRAINTS:
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 COMMAND:
run TaskAllocation for
7 Int, 3 Capability, exactly 3 AtomicTask, 1 Robot