在实现书中问题A.3.6的同时，我需要表达一个条件：
戴上手套后，戴上手套的那只手会发生变化，而戴上手套的那只手应该保持不变。
如果手套在右手和手套在左手时，我如何在不指定条件的情况下巧妙地表达条件，因为这两个条件具有相同的结构。
我的代码在这里：https://github.com/huanhulan/alloy-exercises/blob/master/book/appendixA/gloves.als#L137
【问题讨论】：
标签： alloy
也许不能直接回答您的问题，但我忍不住要制作一个比您看起来更简单的模型。我通常不使用Time 模型，因为它使几乎任何问题都难以处理恕我直言。如果你走这条路线，你可能想结帐Electrum。这是一个可以有效隐藏Time 原子的分支，并且有很好的关键字来限制过去和未来。
module austere_surgery
open util/relation
open util/ordering[Operation]
abstract sig Surface {}
abstract sig Human extends Surface {}
one sig Surgeon extends Human {}
sig Patient extends Human {}
sig Glove {
inside : disj Inside,
outside : disj Outside
}
sig Inside, Outside extends Surface {}
sig Operation {
patient : disj Patient,
-- surfaces is a path from surgeon -> glove* -> patient
surfaces : Surface -> lone Surface,
gloves : set Glove,
contaminated : Human-> Surface
} {
-- constrain to be a proper path (could be improved)
dom[surfaces] = Surgeon + (gloves.(inside+outside)-ran[surfaces])
ran[surfaces] = patient + (gloves.(inside+outside)-dom[surfaces])
all g : gloves | g.inside in dom[surfaces] iff g.outside in ran[surfaces]
-- and no patient must come into contact with the blood of another patient.
surfaces.patient not in ran[contaminated - patient->Surface]
-- the surgeon must not come into contact with the blood of any patient,
Surgeon -> patient not in surfaces
Surgeon.surfaces not in Patient.contaminated
}
pred surgery {
Surface = Glove.inside + Glove.outside + Human
no first.contaminated
all o' : Operation-first, o : o'.prev {
o'.contaminated = o.contaminated
+ o.touches[o.patient]
+ o.touches[Surgeon]
+ o.touches[ran[o.contaminated-Surgeon->Surface]]
}
}
fun Operation.touches[ dirty : set Surface ] : (Patient+Surgeon)-> Surface {
{ from : dirty, to : Surface | from->to in this.surfaces or to->from in this.surfaces }
}
-- A surgeon must operate on three patients, but xe has only two pairs of gloves.
run surgery for 10 but exactly 3 Patient, exactly 3 Operation, exactly 2 Glove
解决方案：
┌──────────────┬─────────────────┬────────┬──────┬─────────────────┐
│this/Operation│surfaces │patient │gloves│contaminated │
├──────────────┼────────┬────────┼────────┼──────┼─────────────────┤
│Operation⁰ │Inside⁰ │Inside¹ │Patient²│Glove⁰│ │
│ ├────────┼────────┼────────┼──────┤ │
│ │Outside¹│Patient²│ │Glove¹│ │
│ ├────────┼────────┤ ├──────┤ │
│ │Surgeon⁰│Outside⁰│ │ │ │
├──────────────┼────────┼────────┼────────┼──────┼────────┬────────┤
│Operation¹ │Inside⁰ │Patient¹│Patient¹│Glove¹│Patient²│Outside¹│
│ ├────────┼────────┼────────┼──────┼────────┼────────┤
│ │Surgeon⁰│Outside⁰│ │ │Surgeon⁰│Outside⁰│
├──────────────┼────────┼────────┼────────┼──────┼────────┼────────┤
│Operation² │Inside⁰ │Outside¹│Patient⁰│Glove⁰│Patient¹│Inside⁰ │
│ ├────────┼────────┼────────┼──────┼────────┼────────┤
│ │Inside¹ │Patient⁰│ │Glove¹│Patient²│Outside¹│
│ ├────────┼────────┤ ├──────┼────────┼────────┤
│ │Surgeon⁰│Outside⁰│ │ │Surgeon⁰│Outside⁰│
└──────────────┴────────┴────────┴────────┴──────┴────────┴────────┘
【讨论】：
Time 来模拟问题仅仅是因为练习向我推荐了这种方式。
一种选择是将公式写在谓词中，然后传入在实例之间变化的部分（在这种情况下是 leftHand 和 rightHand 绑定到的关系）。
【讨论】：