Alloy: Как определить отношения между двумя модулями без ошибки зависимости модуля?

Question

Раньше я определил две простые сигнатуры, чтобы я мог знать, к какому автомобилю принадлежит это колесо.

sig Car{
     wheels: some Wheel
     }

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

Однако, когда я помещаю их в разные модули, анализатор выдаст ошибку «Circular зависимость в импорте модуля ». Итак, как мне определить отношения между автомобилем и колесами без ошибки зависимости модуля?

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

Как указано в сообщении об ошибке, вы пытаетесь открыть модуль W из модуля C, который, в свою очередь, открывает модуль W, который ...

Чтобы избежать этого, я могу напрямую увидеть 3 решения:

1. Определите колесо и автомобиль в одном модуле (поскольку эти две концепции тесно связаны)

OR

определяют отношение между автомобилем и колесами в третьем модуле.

• В модуле C концепция шасси автомобиля (без понятия колес)
• В модуле W определяется понятие колеса
• В модуле X (который открывает C и W) вы можете определить свою концепцию автомобиля как состоящую из шасси и колес.

ИЛИ

Просто опустите поле BelongCar с подписью Wheel, так как вы можете легко получить эту информацию из ~ wheels ...

Мы могли бы помочь вам лучше, если вы расскажете нам больше о своем требования. Какого черта вы хотите разделить эти два понятия на два отдельных модуля?