CODEWITHSUNDEEP
alloy
C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25054

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

I am getting unexpected results in an Alloy model. Consider the following model which describes a few aspects of responses to HTTP requests:

// 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

Because the predicates green and red declare their argument as being of type R200_OK, I expect that these predicates will be true only for atoms in the relation R200_OK, and other Responses (e.g. a Response with rc = rc301) will satisfy neither predicate. This expectation is expressed by assertion A.

To my surprise, however, when asked to check assertion A, the Alloy Analyzer produces what it says is a counterexample, involving a Response which is not in the relation R200_OK. (I first encountered this unexpected behavior in 4.2, build 2012-09-25; the current build of 2014-05-16 behaves the same way.)

Section B.7.3 Declarations of the language reference says "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)." Am I wrong to read this as entailing that the only atoms which should satisfy the predicates red and green are atoms in the relation R200_OK? Or is something else going on?

Upvotes: 1

Views: 441

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

They are checked.

The phenomenon you are pointing out in your question is explained in the Software Abstraction Book page 126.

It's basically written that the type checker will report an error if and only if the type of the argument declared in the predicate and the type of the value given as parameter during invocation are disjoint. In your case, R200_OK and Response are not disjoint, hence the absence of error.

You could rewrite your predicate as follows :

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

To illustrate the type checker's behavior extensively, you can consider the following example

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

I would also like to put under your attention that you use the keyword in rather than extends , in the declaration of your 3 kinds of responses, which implies that :

  • A same response can be of different kind (i.e. a R200_OK response can also be a R302_Found)
  • A Response can also be neither R200_OK nor R302_Found, nor R301_Moved_Permanently.

It might not be what you want to express.

Upvotes: 5

Related Questions