Alloy - Lone instance

Question

I am writing a simple Alloy code but I cannot understand how can I say AT MOST one A has associate with p.D (so AT MOST would be One or Zero). So I wrote the below code but the assertion presents no counter-example with an instance of P1 without D. Could you help me how can I define my fact in terms of having AT MOST one instance for p.D where I can see a counter example that p has no connection for its D.

abstract sig A {}
sig A1,A2,A3 extends A{}
abstract sig P {}
sig P1 extends P {D: A}

fact
{
all p: P1 | lone (p.D & A)
}

assert asr 
{no p: P1 | no (p.D & A)}
check asr for 5

user1513683 user1513683 · Accepted Answer · 2013-09-23T05:08:48

Your specification (introduction of sig P1) says that for each p in P1 is always related by d to exactly one a in A. Your fact is redundant ("0 or 1" is implied by "always 1").

You could declare "sig P1 extends P (D : lone A}". (The fact would still be redundant.)

Also note that the "& A"s in your fact and assertion are redundant.

You might have meant the fact to be fact {lone P1.D} which says that all those instances of P1 which are related to an A are related to the same A.

Alloy - Lone instance

1 Answers