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.
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.