合金初学者概念

Question

我对合金很陌生，目前正在读麻省理工学院的教程。我有点被事情的逻辑卡住了。我想做的一件非常基本的事情是下面。

• 一个人最多只能完成一项任务。
• 一项任务最多可由一人完成
• 一个人只能做他能做的事。

当我运行以下程序时，每个人都有相同的技能(所有技能)，而每个任务都需要相同的技能(再次)。这些人至少每人分配一项任务，但有时他们得到的任务是相同的。

提前感谢

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

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

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

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

• 一项任务最多可由一人完成

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
}