ModelWriter/WP3

[Bug] contains relation must be defined as an injective relation

ferhaterata opened this issue · 0 comments

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 }

Here is a possible inconsistency:
image