使用合金中的功能獲取父對象

Question

我正在嘗試學習合金，但我很難找到合適的學習材料。 所以我正在嘗試一些模型，看看它們是否有效。

我想找到並返回包含給定醫生的診所的功能，但它不起作用。我如何在不改變診所和醫生的情況下做到這一點？

abstract sig Clinic { 
    doctors : set Doctor 
} 
abstract sig Doctor {} 

fun getClinicsOfDoctor [ d : Doctor ] : set Clinic { 
    all c : Clinic | d in c.doctors 
} 

Answer 1

你看過什麼材料？試試Alloy book。另請參閱Alloy website上的教程和論文。

你的模型有什麼問題是你的函數的主體是一個公式。它應該是一個表達。以下任何一種都可以使用

doctors.d 
d.~doctors 
{c: Clinic | d in c.doctors}