setting references with a union

[mantkiew]

The following model works as expected:

abstract X

A : X 
B : X 
C : X

xs ->> X * 
[ xs = A, B, C ] 

However, making X a reference

abstract X -> integer

A : X = 1
B : X = 2
C : X = 3

xs ->> X * 
[ xs = A, B, C ] 

causes the following error in Alloy:

This name is ambiguous due to multiple matches:
field this/c0_X <: ref
field this/c0_xs <: ref

The generated Alloy code is incorrect and irregular:

fact { (c0_xs.@ref) = (((c0_A.@ref) + (c0_B.@ref)) + c0_C) }

The A and B should not have @refs, so only for C is the code generated correctly.

Currently, the only way to fix it is by adding .ref as follows

[ xs = A.ref, B.ref, C.ref ] 

However, the instance produced is incorrect!

=== Instance 1 Begin ===

A = 1
B = 2
C = 3
xs$1 = C
xs$2 = B
xs$3 = A

--- Instance 1 End ---

Changing the xs to

xs ->> integer *

results in the correct instance

=== Instance 2 Begin ===

A = 1
B = 2
C = 3
xs$1 = 3
xs$2 = 2
xs$3 = 1

--- Instance 2 End ---

I suppose this has something to do with the type system.

[mantkiew]

Another way of getting correct output:

abstract X -> integer

A : X = 1
B : X = 2
C : X = 3

xs ->> X *
[ xs.dref.dref = A, B, C ]

desugars correctly to

[c0_xs . dref . dref = c0_A . dref ++ c0_B . dref ++ c0_C . dref]

because by forcing dereferencing twice, the only valid type is TInteger and therefore A, B, and C must also be dereferenced.

[mantkiew]

However, writing

[ xs.dref = A, B, C ]

should not cause A, B to be dereferenced. We get incorrect output today (with Clafer 0.4.1):

[c0_xs . dref = c0_A . dref ++ c0_B . dref ++ c0_C]

whereas we clearly want

[c0_xs . dref = c0_A ++ c0_B ++ c0_C]