平等合金

我有包含以下內容的合金型號：平等合金

abstract sig person{} 

one sig john,Steve extends person {Gender: man} 

sig man{} 

fact { 
    all name: person, Gender: man | 
     name.Gender = name.Gender => person =person}

我怎樣才能讓兩個簽名之間的平等？

來源

2013-06-21 Moody

從您的問題中不清楚您想要做什麼，從您的示例合金代碼看起來好像您可能正在遭受一些混淆。

首先，您顯示的模型以兩種不同的方式使用名稱Gender，這本身並不違法，但似乎暗示了一些混淆。（它肯定會讓讀者感到困惑）

在兩個單身人士簽名約翰和史蒂夫的聲明中，Gender代表兩個二元關係，一個是簽名john和簽名人之間的關係，另一個是Steve和男人。要用符號形式來表達同樣的東西，性別表示（a）約翰 - >人的一些子集，以及（b）史蒂夫的一些子集 - >人。

然而，在匿名事實中，性別表示男子類型的變量。

如果您找到重命名其中一個的方法，您的模型將更容易理解。由於在量化表達變量名是任意的，你實際上將意味着同樣的事情，如果你重新制定它作爲

fact { all P : person, M : man | P.M = P.M => person = person }

如果這不是你的意思說了，那麼你的意思是不是說類似

fact { all P : person, M : man | 
    P.Gender = P.Gender => person = person 
}

重命名變量會強制您選擇一個含義或其他含義。這是一件好事。（不幸的是，這兩種配方在合金中都沒有令人滿意，但我們一次只處理一個問題;擺脫名稱Gender的雙重使用是第一步。）

第二期無論你表達的是什麼意思，它幾乎肯定不意味着你想表達的意思。忽略模型的細節了一會兒，你實際上採取的形式

fact { all V1 : sig1, V2 : sig2 | 
    Expression = Expression => sig1 = sig1 
}

其中表達式是V1.V2或V1.Relation，在模型中定義有一定的關係。錯在這裏有幾件事情：

V1.V2是沒有意義的，其中V1和V2是爲在給定的籤名，簽名或變量的兩個名字：點運算符是有意義的，只是如果它的一個參數是名稱一個關係。
如果任何表達式E都有意義，那麼無論E表示什麼意思，E = E形式的布爾表達式（例如person.Gender = person.Gender）都是真的。 E表示的任何東西自然會與自己相等。因此，有條件的不妨寫
```
1 = 1 => person = person 
```
出於同樣的原因，人=人將永遠是真實的，不管模型：對於任何模型實例中的實例中的人員的將是相同的實例中的一組人員。所以條件永遠是真實的，事實上不會對模型的實例施加任何約束。

目前尚不清楚如何最好地幫助您前進。也許開始的一種方法是問你自己以下哪些陳述是你試圖在你的模型中捕獲的。

有一組人員。
有些人是男性（有性別='男性'）。其他人不是男性。
約翰是一個男性個體。
史蒂夫是一個男性個體。
約翰和史蒂夫是不同的個人。
如果x和y是具有相同性別的個體，那麼x和y是相同的個體。即沒有兩個人具有相同的性別。

注意，這些語句不能全部是真實的在同一時間。（如果這不是很明顯，你可能會做不如試着找出原因。合金可以在這一努力的幫助。）

好運。

來源

2013-06-21 17:41:25

回答

相關問題