Alloy 参数声明中的子集签名 - 是否未检查？

Question

我在 Alloy 模型中得到了意想不到的结果。考虑以下模型，它描述了对 HTTP 请求的响应的几个方面：

// Code:  an HTTP return code
abstract sig Code {}
one sig rc200, rc301, rc302 extends Code {}

// State:  the current state of a resource
sig State {}

// subsets of State: some resources are green, some red
// (also:  some neither, some both)
sig Green in State {}
sig Red in State {}

// Response:  a return code + state pair
sig Response {
  rc : one Code,
  entity_body : lone State
}

// some subclasses of Response
sig R200_OK in Response {}{ rc = rc200 }
sig R301_Moved_Permanently in Response {}{ rc = rc301 }
sig R302_Found in Response {}{ rc = rc302 }

// a Response is red/green if its entity body is Red/Green
pred green[ R : R200_OK ] { R.entity_body in Green }
pred red[ R : R200_OK ]{ R.entity_body in Red }

assert A {
  all R : Response | green[R] implies R.rc = rc200
}
check A for 3

因为谓词 green 和 red 将它们的参数声明为 R200_OK 类型，我希望这些谓词仅对关系 [=14= 中的原子为真]，其他响应（例如 rc = rc301 的响应）将不满足任何谓词。这种期望由断言 A.

表达

然而，令我惊讶的是，当要求检查断言 A 时，Alloy 分析器产生了它所说的反例，涉及不在关系 R200_OK 中的响应。（我第一次遇到这种意外行为是在 4.2 版本 2012-09-25；当前版本 2014-05-16 的行为方式相同。）

第 B.7.3 节语言参考声明说 "A declaration introduces one or more variables, and constrains their values and type. ... The relation denoted by each variable (on the left) is constrained to be a subset of the relation denoted by the bounding expression (on the right)." 我是否错误地将其理解为应该满足谓词 red 和 green 的唯一原子是原子在关系 R200_OK 中？还是有其他事情发生？

Answer 1

已检查。

您在问题中指出的现象在软件抽象书籍第 126 页中有解释。

基本上写的是，当且仅当谓词中声明的参数类型与调用期间作为参数给出的值的类型不相交时，类型检查器才会报告错误。在您的情况下，R200_OK 和 Response 不相交，因此没有错误。

您可以按如下方式重写谓词：

pred green[ R : Response ] {R in R200_OK and R.entity_body in Green }

为了广泛地说明类型检查器的行为，您可以考虑以下示例

sig A,B extends C{}
sig C{ c: set univ}
pred testExtend[a:A]{
    a.c!= none
}

run {testExtend[A]} // works as expected
run {testExtend[B]} // error as A and B are disjoint
run {testExtend[C]} // no error as A and C are not disjoint

sig D,E in F{}
sig F{ f: set univ}
pred testIn[d:D]{
    d.f!= none
}

run {testIn[D]} // works as expected
run {testIn[E]} // no error as E and D are not disjoint
run {testIn[F]} // no error as E and F are not disjoint

我还想提醒您，您在 3 的声明中使用关键字 in 而不是 extends各种反应，这意味着：

相同的响应可以是不同的类型（即 R200_OK 响应也可以是 R302_Found）
响应也可以既不是R200_OK也不是R302_Found，也不是R301_Moved_Permanently。

可能不是你想表达的意思

Alloy 参数声明中的子集签名 - 是否未检查？

Subset signatures in Alloy argument declarations - are they not checked?

alloy