合金初学者的概念

Question

我对合金很陌生，目前正在阅读 mit 的教程。我有点卡在事情的逻辑上。我正在尝试做的一个非常基本的事情如下。

• 一个人最多只能完成一项任务
• 一项任务最多可由 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 = p2.assigned 而不是p1.assigned not in 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
}