meta capability

A new meta capability has been added for greater flexibility to efficiently handle some situations.

When the model contains at least one attempt to reference a meta atom, then the model will be automatically augmented with meta atoms as follows:

So, for example, say we have the following model:

  sig A {
      x: Int,
      y: Int,
      z: Int
  }

One common thing you might want to have is an equals predicate:

pred eq[a1, a2 : A] { a1.x=a2.x and a1.y=a2.y and a1.z=a2.z }

The unconvenience with doing it this way is that it gets very long as there are more fields in the sig and if you happen to add a new field in A you have to remember to modify the eq predicate as well.

Using the meta capability this predicate could be written more succinctly (and with no impact on performance) like this:

pred eq[a1, a2 : A] { all f:A$.subfields | a1.(f.value)=a2.(f.value) }

You can also have more a intricate model such as:

sig A { x: Int }
sig B extends A { y: Int->Int }

and the following will still work:

pred eq [b1, b2 : B]  { all f:B$.subfields | b1.(f.value)=b2.(f.value) }

We do some manipulations to make this common idiom work because it's a fairly common one: whenever we see an expression of the kind "all f:GUARD | body" or "some f:GUARD | body" where GUARD's type is a subtype of (sig$+field$), we replicate the body multiple times for each possible meta atom in existence, and bind "f" to each possible meta atom one-at-a-time. We do this in such a way that there's no impact in performance; the cost of writing a frame condition using the meta capability is exactly the same as if you manually enumerate each field.

But this is a one-off case, so always be mindful about the expressions you write since these will still need to type-check.