CODEWITHSUNDEEP
alloy
Glad
Glad

Reputation: 3

How to represent one-to-one relationship in Alloy?

Assume I have sig A{} sig B{e:A} I want to represent 1-1 mapping between A and B so for each B there is one and only one A correspond to:

{all b:B | one a : A | b.e = a}

Are there some another way to do that, such as using multiplicity?

Upvotes: 0

Views: 787

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

You could write to ensure that each B is related to exactly one A :

 sig B{
   e: one A
 }

Edit:

To ensure that each A is related to exactly one B you can add a signature fact to the signature declaration of A

sig A{
}{
    one this.~e
}

Why this work :

The signature fact under signature A is processed by Alloy as:

fact{
    all a:A | one a.~e
}

in which:

  • e is a field defined in signature B. It hence define a relation of type B -> A.

  • The ~ operator yields the inverse of that relation (so the type becomes A -> B ).

  • The "dot join" between a and that relation (A.A->B) yields all the B elements for which B.e=a.

  • The one keyword is finally used to say that there's only one such B element (for all a).

Upvotes: 3

Related Questions