Alloy：如何定义两个模块之间的关系而没有模块依赖性错误？

Question

以前，我定义了两个简单的签名，以便可以知道此车轮属于哪辆车。

sig Car{
     wheels: some Wheel
     }

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

但是，当我将它们放入不同的模块中时，分析器将给出错误“模块导入中的循环依赖性”。那么，如何在没有模块相关性错误的情况下定义汽车与车轮之间的关系呢？

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

作为错误状态，您尝试从模块C打开模块W，而模块C依次打开模块W，这...

为避免这种情况，我可以直接查看3个解决方案，或者：

1. 在单个模块中定义车轮和汽车（因为这两个概念密切相关）

OR

2. 在第三个模块中定义汽车和车轮之间的关系。

   • 在模块C中，汽车底盘的概念（不带轮子的概念）
   • 在模块W中，定义了车轮的概念
   • 在模块X（打开C和W）中，您可以将汽车的概念定义为由底盘和车轮组成。

OR

3. 只需删除Wheel签名的BelongCar档案，因为您可以轻松地从〜wheels获得此信息...

如果您告诉我们更多有关您的要求的信息，我们可能会为您提供更好的帮助。您为什么想将这两个概念分为两​​个单独的模块？