合金初學者的概念

Question

我是合金新手，目前正在閱讀教程。我對事物的邏輯有點困惑。下面是我想要做的一件非常基本的事情。

• 一個人只能做至多任務
• 一個任務可以最多由1個人做
• 一個人只能做他/她能夠

當我運行以下，每個人都有相同的技能（所有技能），每項任務都需要相同的技能（所有技能）。每個人至少分配1個任務，但他們有時會得到相同的任務。

在此先感謝

some sig Skills{ } 


some sig Person { 
has: some Skills, 
assigned: lone Task 
} 

some sig Task 
{ 
requires: some Skills 
} 
{ 
// everyone must have the required task skills for assignment 
all p:Person | p.has= requires 
} 

pred Valid() 
{ 
//everyone must be assigned to single task 
    all p:Person | lone t:Task| p.assigned in t 
// no one can have the same task 
    no p1:Person , p2:Person | p1.assigned not in p2.assigned 
} 

run Valid 

Answer 1

有許多的事情是在你的模型不正確。

• 一個人只能做至多任務

爲了實現這一點，在Person簽名assigned領域lone多重修改就足夠了。如果您希望每個人只分配一個任務，則可以將lone更改爲one。

• 任務最多可以由1個人來完成

你在Valid謂詞約束是錯誤的，因爲代替p1.assigned not in p2.assigned，你應該以說，寫p1.assigned = p2.assigned有沒有兩個人分配了相同的任務。此外，您應該添加一個約束，確保p1 != p2。或者，你可以寫all p1, p2: Person | p1 != p2 implies p1.assigned != p2.assigned。最後，爲避免必須在量詞主體中編寫p1 != p2，可以使用disj關鍵字來表示，例如no disj p1, p2: Person | p1.assigned = p2.assigned或all disj p1, p2: Person | p1.assigned != p2.assigned。

• 一個人只能做他/她能夠

你在Task簽名的附加事實部分的約束是錯誤的，因爲它沒有提及assigned字段，這是你必須做的，以便爲每個人和分配給他們的任務說出 ，該人擁有該任務所需的所有技能。你寫的意思是說，對於每一項任務，每個人都具備完成該任務所需的所有技能。滿足這一點的唯一方法就是如果所有任務都具有相同的技能，這正是您在爲模型獲得的所有實例中注意到的。

這是我如何會對此建模（注意在現場和簽名名稱的細微變化，這使得模型稍微更易於閱讀和理解）：

some sig Skill {} 

some sig Person { 
    hasSkill: some Skill, 
    assignedTask: lone Task 
} 

some sig Task { 
    requiredSkills: some Skill 
} 

// everyone must have the required skills for the assigned task 
fact requiredTaskSkills { 
    all p:Person | p.hasSkill in p.assignedTask.requiredSkills 
} 

// everyone has at least one assigned task 
pred atLeastOneTask { 
    all p: Person | one p.assignedTask 
} 

// no two persons can have the same task assigned 
pred uniqueTaskAssignments { 
    no disj p1, p2: Person | p1.assignedTask = p2.assignedTask 
}  

run { 
    atLeastOneTask and uniqueTaskAssignments 
}