Alloy:How to define the relations between two modules without the module dependency error?

Question

Previously, I defined two simple signatures so that I can know which car does this wheel belong to.

sig Car{
     wheels: some Wheel
     }

sig Wheel{ 
    BelongCar:one Car,
}{
    BelongCar=this.~@wheels
}

However, when I put them into different modules, the analyzer will give the error "Circular dependency in module import". So how should I define the relations between Car and Wheels without the module dependency error?

\\in C.als
module C
open W

sig Car{
     wheels: some Wheel
     }


\\in W.als
module W
open C
sig Wheel{ 
    BelongCar:one Car,
}{
    BelongCar=this.~@wheels
}

Answer 1

As the error states, you try to open module W from module C which, in turns opens module W, which ...

To avoid this I can directly see 3 solutions, either:

1. Define wheel and car in a single module ( as the two concepts are intimately linked)

OR

2. define the relation between car and wheels in a third module.

   • In module C the concept of a car chassis ( without the notion of wheels )
   • In module W the concept of wheel is defined
   • In module X (which open C and W ), you can define the your concept of Car as being composed of Chassis and Wheels.

OR

3. Simply drop the BelongCar filed of the Wheel signature, as you can easily get this info from ~wheels...

We might be able to help you better if you tell us more about your requirements. Why the heck would you like to divide those two notions into two separate modules ?