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,我希望这些谓词仅对于关系中的原子是真的R200_OK,而其他响应(例如,响应rc = rc301)将既不满足谓词也不满足谓词.这种期望由断言A表示.

然而,令我惊讶的是,当被要求检查断言A时,合金分析仪产生它所说的反例,涉及一个不在R200_OK关系中的响应.(我在4.2中首次遇到这种意外行为,构建2012-09-25; 2014-05-16的当前版本的行为方式相同.)

B.7.3节语言参考的声明说:"声明引入一个或多个变量,并约束它们的值和类型....每个变量表示的关系(左侧)被约束为表示的关系的子集通过边界表达式(在右边)." 我错误地将其视为需要满足谓词的唯一原子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种反应的声明中使用关键字而不是扩展,这意味着:

• 相同的响应可以是不同类型的(即R200_OK响应也可以是R302_Found)
• 响应也既不是R200_OK也不是R302_Found,也不是R301_Moved_Permanently.

它可能不是你想要表达的.