0

私は単純な Alloy コードを書いていますが、AT MOST 1 つの A が pD に関連付けられているとどのように言うことができるか理解できません (したがって、AT MOST は 1 または 0 になります)。だから私は以下のコードを書きましたが、アサーションはDのないP1のインスタンスで反例を提示しません.私が反例を見ることができるpDのAT MOST 1つのインスタンスを持つという点で私の事実を定義する方法を教えてください. 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
4

1 に答える 1

2

あなたの仕様 (sig P1 の導入) は、P1 の各 p は常に d によって A の正確に 1 つの a に関連付けられていることを示しています。事実は冗長です (「0 または 1」は「常に 1」によって暗示されます)。

「sig P1 extends P (D : lone A}」と宣言することもできます (この事実はまだ冗長です)。

また、ファクトとアサーションの「& A」は冗長であることにも注意してください。

A に関連する P1 のすべてのインスタンスが同じ A に関連していることを示すファクト {lone P1.D} であるという事実を意味している可能性があります。

于 2013-09-23T05:08:48.007 に答える