what's the problem in defining multiple constraints?

I'm trying to write a simple (I thought) model in Alloy, but clearly I didn't get the point ...

The problem is very simple ... A graph that models a network of roads.

Obv a car can be on a Road OR on a CrossRoad, but not in both of them. Here there's my code:

//SIGNATURES

sig Cross {
    var cars: set Car,
    roads: some Road
}

sig Road {
    var cars: set Car
}

sig Car {}

//FACTS

fact CrossConstraints {
    (all r : Road |
        #({cr : Cross | r in cr.roads}) = 2)
}

fact CarConstraints {
    (all c : Car |
        no cr1, cr2 : Cross |
            c in cr1.cars and c in cr2.cars)
    (all c : Car |
        no r1, r2 : Road |
            c in r1.cars and c in r2.cars)
    (all c : Car |
        (one r : Road | c in r.cars ) or
        (one cr : Cross | c in cr.cars))
}

fact {
    #Car > 1
}

It all seems good to me, but the analyser doesn't find and instance of my model ... It seems the problem lies in the constraints defined for `` Car ```, which actually seem very reasonable to me.

Any idea? Thanks

Solution

The usual solution to "debug" an inconsistent spec is to comment facts out and see if the spec becomes consistent, which gives hints to what may be an issue.

Here, the CarConstraints fact is too strong indeed. You're saying that:

every car is necessarily somewhere
but a car cannot be in two crosses even if the crosses are actually the same (and similarly for roads)

Here, you rather meant that a car cannot be in two crosses unless they happen to be the same cross. Said otherwise, you want cars (for both Cross and Road to be injective). To state this (for crosses), you have several choices:

(all c : Car |
        no disj cr1, cr2 : Cross |
            c in cr1.cars and c in cr2.cars)

// I prefer this because it doesn't feature negation, which is error-prone

(all c : Car, cr1, cr2 : Cross |
            c in cr1.cars and c in cr2.cars implies cr1 = cr2)

and finally, since this is a structural fact corresponding to a physical reality, you may directly state this in the domain model (and remove the corresponding fact statement at once):

sig Cross {
    var cars: disj set Car,
    roads: some Road
}

(technically, the last one is stronger since it comes with an implicit always in front of it; in any case, your facts should probably come with an always prepended).

Also, cardinality constraints related to the instances you want to witness (CrossConstraints and #Car > 1) should IMO go in a run command rather than be stated as facts. Facts should IMO almost only be used for general truths.