0

我对合金很陌生，目前正在阅读 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
4

1 回答 1

0

您的模型中有许多不正确的地方。

  • 一个人最多只能完成一项任务

要实现这一点，签名中字段的lone多重性修饰符就足够了。如果您希望每个人都只分配一个任务，您可以更改为.assignedPersonloneone

  • 一项任务最多可由 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
}
于 2012-11-01T16:51:47.233 回答