Testcase:positive/tmp_DefaultGlobal.cfr

[RaoMukkamala]

Checks

1. test case is ok ? Yes
2. Compiles ? Yes
3. De-sugars correctly ? No
4. Compiles in Alloy ? Yes
5. Instances checked in alloy? Yes.

a
  b ?
    c ?
  [c] // globally c in the context of b
This should desugars to: [globally (this . c0_b => this . c0_b . c0_c) ].
But it actually desugars to: [some this . c0_b . c0_c]

I tested by adding an assertion: assert[never (a.b && not a.b.c) ] and I found a counter example where in the
Time 0: root -> c0_a -> c0_b2 ->c0_c0 plus some orphan instances of b and c.
Time 1: root -> c0_a -> c0_b2 plus some orphan instances of b and c. (which is a voilation)

[mantkiew]

Actually, adding the globally by default is not implemented in the desugarer. I guess, we have to revisit what the proper desugaring should be. What you have

[globally (this . c0_b => this . c0_b . c0_c) ]

only works for clafers with card max 1. And it is even incorrect. Should be:

[globally (some this . c0_b => some this . c0_b . c0_c) ]

In general, we need to quantify over each instance of b like this

[globally (all x : this . c0_b | some x.c0_c) ]

Also, wanted to reiterate that the insertion of quantifiers actually happens in the type system, not in the desugarer.

[wasowski]

I can't study this in detail now (drowning in overwork), but let me just mention that this case is covered in the ECOOP draft. We have identified some problems in the draft, but globally seems allright.:

A 2..5
   B ∗ 
      [ φ( "this" ) ]
   [ G(all b : this.B | φ( b/this ) ) ]
[ G( all a : this.A | G(all b : a.B | b =>φ( b/this ) )) ]

(from page 10)