[Bug] contains relation must be defined as an injective relation
ferhaterata opened this issue · 0 comments
ferhaterata commented
Make necessary changes in Alloy and SMT files
In predicate calculus style:
∀a, a' ∈ A | ∀b ∈ B | (a, b) ∈ R ∧ (a' , b) ∈ R → a = a'
In Alloy Navigational style:
contains : Requirement lone → Requirement
fact {all a: Requirement | lone contains.a }
or
fact {all a: Requirement | lone a.~contains }