Loss of keyword "all" in Alloy

1

I’m used to writing models in Alloy that have each “step” in a predicate and then require that all steps satisfy the predicate. Now that the keyword “all” is no longer supported, it seems that it is difficult to quantify over variables passed to a predicate as in:

sig A {}

pred allsteps {
some s:A ,sPrime:A | step [a,aPrime]
}

pred step[a,aPrime:A] {
a = aPrime
}

Any hints on how to quantify over arguments passed to predicates in the new Alloy? I want to keep the structure of the separation of concerns in the predicates.

2

Sorry, I don’t see what you mean… Can you expand on this?

3

Wondering what you mean by “all” not being supported…

1 Like
4

I see that I posted the wrong code for my question. Sorry! Here is the error message that we are getting.
Screenshot from 2021-10-27 11-47-19
I interpreted this error message to mean the ``all’’ keyword is no longer supported as a quantifier. If that’s not the case, what does the error message mean?

5

The following code generates the error message above in Alloy 6:

sig Snapshot{}
pred path{
	all s,s_next | operation[s,s_next]
}

We figured out that we needed to add types, but the error message was not very helpful!

6

I seem to recall it was possible to use all as a relation qualifier, like one, some and no currently, in old versions of Alloy (before Alloy 4). So there was probably a time where writing all r not followed by : became syntactically incorrect, hence the error message.

1 Like
7

Yes, that’s exactly right. My recollection is that I was being rather fanatical about consistency in the language design, so indeed it seemed that if you could write no expr and some expr, you should be able to write all expr too, but then we realized it was a terrible idea!

8

I was bit by the same error message when I wrote (following a tutorial), something like all x' :.

Turns out the apostrophe has become illegal to use, but the error message told me I couldn’t use all…

9

Interesting. We should perhaps remove these error messages (there are two occurrences in the Alloy grammar specifications). This would still yield an error, but at least a “nominal” one rather than ad-hoc one (which gives a misleading message like the one you had).