如何在'or'条件下编写 let 表达式

Question

在暗示书中的问题A.3.6时，我需要表达一个条件，例如：

戴上手套后，手套所在的手发生了一些事情，而另一方面的手套应该保持不变。

我如何在不指定手套在右手和手套在左手时的条件的情况下整齐地表达条件，因为这两个条件具有相同的结构。

我的代码在这里：https://github.com/huanhulan/alloy-exercises/blob/master/book/appendixA/gloves.als#L137

Answer 1

也许不是直接回答你的问题，但我忍不住制作一个比你看起来更简单的模型。我通常不使用Time模型，因为它使几乎所有问题都变得笨拙恕我直言。如果你去这条路线，你可能想结账 轻质.这是一个有效地隐藏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⁰│
└──────────────┴────────┴────────┴────────┴──────┴────────┴────────┘

Answer 2

一种选择是在谓词中编写公式，然后传入在实例化之间变化的部分(在本例中为左手和右手绑定到的关系(。