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:

• For each user-defined sig X, we add a meta atom “X$”; and for each field Y in a user defined sig X, we add a meta atom “X$Y”.
• Given the meta atom “X$” representing some user signature; “X$.fields” represents the meta atoms for its immediate fields and “X$.subfields” the meta atoms for it and all descendants’ fields.
• Given the meta atom “X$Y” representing some field; “X$Y.value” represents the actual field value in the real world.
• An atom “sig$” is added that represents the union of all meta atoms that represent signatures as well as a “field$” atom representing the union of all meta atoms that represent fields.

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 inconvenience 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.