Why does alloy model with but 1 set A return instance of more than 1 A

Question

I am sorry for the title, I tried hard to make it as understandable as possible but I know I failed. Here is the simple model:

sig ETHBusStation {
    next: set ETHBusStation
}

one sig Polyterrasse, HaldenRight, HaldenLeft, Hoengg extends ETHBusStation {}

sig ETHBus {
    station: lone ETHBusStation
}

fact {
    //no (Hoengg - HaldenRight)
    all s: ETHBusStation | ETHBusStation in s.^next and some s.next
    all b1, b2: ETHBus | b1.station != b2.station}

run {} for 2 but 1 ETHBusStation

when I run the analyzer it finds an instance with one of each Polyterrasse, HaldenRight, HaldenLeft, Hoengg but since these are all disjoint subsets of ETHBusStation, how can this be with the but 1 parameter?

I am expecting it to have a single station that links to itself via next.

I am grateful for any hints and tips. If we use in instead of extends it behaves as expected, but then they also don't have to be disjoint which makes sense.

Answer 1

I believe the scope declaration is being overridden by the one sig decl. If it didn't do this, the expected behavior would be to find no instances, since the sig decl claims that exactly four bus stations exist, and the scope says that there is at most one bus station.