Incorrect instance

[lpassos]

Version: 0.0.3 Description: instance generated by Alloy does not reflect constraints given by Clafer instance spec.

How to reproduce:

abstract Person
  name
    first : string
    last  : string
  or spokenLanguage
     english
     german
     other : string

ThomasEdison : Person
  [ first = "Thomas"
    last  = "Edison"
    english
    ! german
    other = "french"
  ]

Result: when running alloy on the produced file from clafer translator result in an instance thomasEdison with only english as spokenLanguage. Actually, Alloy produces 2 instances: 1) only english, 2) both english and other=2 (where 2 represents the string "french").

Expected result: thomasEdison instance should have english and "french" as spokenLaguages.There should be only one instance.

[kbak]

It's not necessarily incorrect. It all depends on the semantics we agree on. For now I'm closing the issue, because the model behaves as expected. I sent an email several days ago about semantics of primitive clafers. Feel free to comment and show this example!

[lpassos]

I don't see why the model behaves as expected. The semantics of "or" has long been defined in Clafer as having the same meaning as FODA's or-group cardinality, unless it had changed to something different. As far as I know, an or group defines that at least one subclafer must occur (in the case of ThomasEdison, exactly english and french). I don't see why having 2 instances as result is correct. Could you please clarify on that?

[kbak]

You said that or means at least 1, so 1) only english is correct, 2) both english and other = 2 is correct. The constraint says other = "french", which was translated to universal quantification: all x : other | x.ref = french. Universal quantification doesn't imply that there is an instance of other. Feel free to contribute to https://github.com/gsdlab/clafer/wiki/Experimental:-Attributes

[lpassos]

Hmm. Got it :)