0

私は合金にまったく慣れておらず、現在mitでチュートリアルを読んでいます。私は物事の論理に少し行き詰まりました。私がやろうとしている非常に基本的なことは以下のとおりです。

  • 人はせいぜい 1 つのタスクしか実行できません
  • タスクは最大 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
4

1 に答える 1

0

あなたのモデルには多くの不正確な点があります。

  • 人はせいぜい 1 つのタスクしか実行できません

これを実装するには、署名内のフィールドのlone多重度修飾子で十分です。すべての人にタスクを 1 つだけ割り当てたい場合は、 に変更できます。assignedPersonloneone

  • タスクは最大 1 人で実行できます

同じタスクが割り当てられている2人の人物はいないと言うために代わりに書く必要がValidあるため、述語の制約は間違っています。さらに、それを保証する制約を追加する必要があります。あるいは、 と書くこともできます。最後に、量指定子本体に書き込む必要をなくすために、キーワードを使用して、たとえば、、または.p1.assigned not in p2.assignedp1.assigned = p2.assignedp1 != p2all p1, p2: Person | p1 != p2 implies p1.assigned != p2.assignedp1 != p2disjno disj p1, p2: Person | p1.assigned = p2.assignedall 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 に答える