通过约束对Alloy中抽象关键字语义进行编码

Question

我想将抽象关键字语义编码为Alloy中的约束(请耐心，我需要这样做是有原因的!:))。如果我有以下代码:

abstract sig A {}
sig a1 extends A{}
sig a2 extends A{}

我认为它的含义如下(我希望我是对的!):

sig A {}
sig a1 in A{}
sig a2 in A{}
fact {
   A=a1+a2         //A is nothing other than a1 and a2
   a1 & a2 = none  // a1 and a1 are disjoint
}

所以上面的两个签名是相等的(即，在语义上是相等的):

我渴望使用Alloy提供的抽象关键字来简化生活，但是当我使A成为sig O的子集并使用抽象关键字:

时，问题出现了。

sig O{}
abstract sig A in O{}
sig a1 extends A{}
sig a2 extends A{}

以上语法

返回错误!Alloy抱怨:"子集签名不能抽象"，所以我的第一个问题是:为什么Alloy不允许这个?

我没有停下来编码抽象的关键字语义(如上所述)，并得出以下代码:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}
fact {
    A=a1+a2             // A can not be independently instantiated
    a1 & a2 = none      // a1 and a2 are disjoint
}

这工作，一切都很好:)

现在，如果我想将a3添加到Alloy规格中，我需要按如下方式调整规格:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}
sig a3 in A{}
fact {
    A=a1+a2+3           
    a1 & a2 = none  
    a1 & a3 = none
    a2 & a3 = none
}

但是，正如您通过比较上面的两个规范所看到的，如果我想继续这样做，并以类似的方式添加a4到我的规范中，我需要更多地更改事实部分，这仍然很麻烦!实际上ai &Aj =none (for i=1..n)表达式是非单调递增的!例如，添加a4迫使我添加多个约束:

fact {
    A=a1+a2+3 +a4           
    a1 & a2 = none  
    a1 & a3 = none
    a1 & a4 = none
    a2 & a3 = none
    a2 & a4 = none
    a3 & a4 = none
}

所以我的第二个问题:是否有任何解决方法(或可能更简单的方法)来做到这一点?

任何评论都是赞赏的。谢谢:)

Answer 1

关于Q1(为什么Alloy不允许扩展子集签名?):我不知道。

关于Q2(是否有解决方案):最简单的解决方案是使a1…可以是A的子签名(扩展)，并找到另一种方法来建立A与O的关系。在您给出的简单示例中，O没有子类型，因此只需将A in O更改为A extends O即可。

如果O已经被你没有展示给我们的其他签名分区了，那么这个解决方案就不起作用了;在没有更多细节的情况下，很难说什么会起作用。(理想情况下，你需要一个最小的完整的工作示例来说明难度:你给出的示例是最小的，并且说明了一个难度，但它们不能说明为什么a不能是o的扩展)

---

(附录)

在评论中，你说

我在O中使用A而不是A extends O的原因是O中还有另一个签名C，这里没有显示。A和C不一定不相交，所以这就是我认为我必须在中使用而不是extend来定义它们是o的子集的原因。

细节决定成败，但结论不是由前提得出的。如果A和C都扩展O，它们将不相交，但如果一个使用扩展，另一个在中使用，它们不会自动不相交。因此，如果您希望A和C都是O的子集，并且A由几个其他签名划分，则可以这样做(除非存在尚未提到的其他约束)。

sig O {}
abstract sig A extends O {}
sig a1, a2 extends A {}
sig a3, a4 extends A {}
sig C in O {}