Сплав — единственный экземпляр

Я пишу простой код Alloy, но я не могу понять, как я могу сказать, что МАКСИМАЛЬНО один A связан с pD (так что МАКСИМАЛЬНО будет единица или ноль). Итак, я написал приведенный ниже код, но утверждение не представляет нет контрпримера с экземпляром P1 без D. Не могли бы вы помочь мне, как я могу определить мой факт с точки зрения наличия МАКСИМАЛЬНО одного экземпляра для p.D, где Я вижу контрпример, что p не имеет связи с 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

alloy
person user1021110    schedule 22.09.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ваша спецификация (введение знака P1) говорит, что для каждого p в P1 всегда связано d ровно с одним a в A. Ваш факт является избыточным («0 или 1» подразумевается «всегда 1»).

Вы можете объявить «sig P1 extends P (D : lone A}» (этот факт все равно будет излишним).

Также обратите внимание, что «& A» в вашем факте и утверждении избыточны.

Возможно, вы имели в виду факт {одиночный P1.D}, который говорит, что все те экземпляры P1, которые связаны с A, связаны с одним и тем же A.

person user1513683    schedule 23.09.2013
comment
Да. Вы правы я забыл что кратность по умолчанию равна единице и согласен с вами по поводу избыточности в коде, но на результат это не влияет. - person user1021110; 24.09.2013