我想将 abstract 关键字语义编码为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提供的Abstract关键字来简化生活,但是当我将A作为sig O的子集并使用 abstract 关键字时,问题就出现了:
sig O{}
abstract sig A in O{}
sig a1 extends A{}
sig a2 extends A{}
上面的语法返回错误!合金抱怨:"Subset signature cannot be abstract.",所以我的第一个问题是: Why Alloy does not allow this?
我不停止并编码抽象关键字语义(如上所述),并得到以下代码:
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
}
这工作,一切都很好:)
现在,如果我想在我的Alloy规范中添加a3,我需要调整我的规范如下:
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(对于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
}
所以我的第二个问题: Is there any workaround (or probably simpler way) to do this?
任何评论表示赞赏 . 谢谢 :)
1 回答
在Q1(为什么Alloy不允许扩展子集签名?):我不知道 .
在Q2(有一个解决方法):最简单的解决方法是使a1 ...成为A的子签名(扩展),并找到另一种方法来 Build A和O的关系 . 在你给出的简单例子中,O没有子类型,所以只需将
A in O
更改为A extends O
即可 .如果O已经被您未显示的其他签名分区,则该解决方法不起作用;如果没有更多细节,就不可能说出什么会有用 . (理想情况下,您需要一个最小的完整工作示例来说明难度:您给出的示例很少,并说明了一个难点,但它们没有说明为什么A不能作为O的扩展 . )
[附录]
在评论中,你说
魔鬼在细节中,但结论并未遵循所述的前提 . 如果A和C都扩展为O,它们将是不相交的,但如果使用 extend 而另一个使用 in 则它们不会自动脱节 . 因此,如果您希望A和C各自是O的子集,并且A要由其他几个签名进行分区,则可以这样做(除非还有其他约束尚未提及) .