CODEWITHSUNDEEP
alloy
qartal
qartal

Reputation: 2064

Creating an object for each relation in Alloy

I have the following def. in Alloy:

sig A {b : set B}
sig B{}
sig Q {s: A , t: B}

I want to add a set of constraints such that for each relation b1:b there exists one and only one Q1:Q where Q1.s and Q1.t refers to the source and target of b1, respectively. For example, if I have an instance which contains A1 and B1 and b1 connects them (i.e., b1: A1->B1), then I also would like to have a Q1 where Q1.s=A1 and Q1.t=B1.

Obviously number (cardinality) of Q is equal to number (cardinality) of b relation.

I managed to write such a constraint as bellow:

t in s.b 
all q1,q2:Q | q1.s=q2.s and q1.t=q2.t => q1=q2
all a1:A,b1:B | a1->b1 in b => some q:Q | q.s=a1 and q.t=b1

I am wondering if anyone has a bit more concise way to express my intentions in terms of an alloy fact. I am open to use Alloy util package if it makes life easier.

Thanks

Upvotes: 0

Views: 232

Answers (2)

qartal
qartal

Reputation: 2064

I would complete the @user1513683 answer by adding two relations s and t to make it the complete answer to the question:

sig A { b : set B }
sig B {}
sig Q { ab : A -> B , s:A, t:B}{ one ab and t=ab[s]}
fact { b = Q.ab and #Q = #b }

Upvotes: 0

user1513683
user1513683

Reputation: 419

sig A { b : set B }
sig B {}
sig Q { ab : A -> B }{ one ab }
fact { b = Q.ab and #Q = #b }

Upvotes: 1

Related Questions