首页 文章

通过约束在Alloy中编码抽象关键字语义

提问于
浏览
0

我想将 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 回答

  • 2

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

    在Q2(有一个解决方法):最简单的解决方法是使a1 ...成为A的子签名(扩展),并找到另一种方法来 Build A和O的关系 . 在你给出的简单例子中,O没有子类型,所以只需将 A in O 更改为 A extends O 即可 .

    如果O已经被您未显示的其他签名分区,则该解决方法不起作用;如果没有更多细节,就不可能说出什么会有用 . (理想情况下,您需要一个最小的完整工作示例来说明难度:您给出的示例很少,并说明了一个难点,但它们没有说明为什么A不能作为O的扩展 . )


    [附录]

    在评论中,你说

    [我在O中使用A代替A扩展O]的原因是O中有另一个签名C,此处未显示 . A和C不一定是不相交的,所以这就是我认为我必须使用而不是扩展将它们定义为O的子集的原因 .

    魔鬼在细节中,但结论并未遵循所述的前提 . 如果A和C都扩展为O,它们将是不相交的,但如果使用 extend 而另一个使用 in 则它们不会自动脱节 . 因此,如果您希望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 {}
    

相关问题