Forbid prime in fields and pred/fun parameters/return type

[grayswandyr]

Primes in fields and pred/fun parameters (and return type) should in my view raise syntax errors:

sig S { var s: S' }
pred p[x: S'] {}
fun q[x: S'] : S' { S }
run {}

[dkasak]

What about expressions? Does an expression such as

some s: S' {
    not (s in S)
    S' = S + s
}

Have a well-defined meaning? From testing, it seems to behave strangely and not in the way I expected.

[grayswandyr]

Sure it does.

var sig S {}

run {some s: S' {
    not (s in S)
    S' = S + s
} }

yields, as expected, a trace where you have an element s in state 1, that is not in state 0, and that is the only difference (for S) wrt state 0.

[dkasak]

I've since started using some s: S' - S instead but I've also changed my spec in other ways. And now predictably when changing some s: S' - S back to some s: S' { not (s in S) }, it works equivalently. :( So I must've been doing something else it didn't like.

So disregard the above, I'll report back if I manage to reproduce the odd behaviour.

[grayswandyr]

BTW, I think it's risky to "create" values of a toplevel var sig with such quantifications because you cannot talk about the pool of values you're drawing from. In that case, it's safer to explicitly model it with an ad-hoc sig:

sig Pool {}
var sig S in Pool {}

run {some s: Pool {
    s in Pool - S
    S' = S + s
} }

[dkasak]

Risky in what way? If I want to enforce invariants on the entire pool I can use S, and when talking about the new elements specifically, I can use S' - S. I wonder if I'm missing something.

[grayswandyr]

I just meant it can be confusing to newcomers.

[nmacedo]

Forbidden for 6.2.