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

Question

在做书上的A.3.6题时，我需要表达这样一个条件：

After putting on a glove, for the hand that the glove is on something happens while for gloves on the other hand should stay the same.

手套在右手和手套在左手的情况下，如何在不指定条件的情况下简洁地表达条件，因为两个条件的结构相同。

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

Answer 1

一个选择是将公式写在谓词中，然后传入在实例化之间变化的部分（在本例中是 leftHand 和 rightHand 绑定到的关系）。

Answer 2

也许不能直接回答您的问题，但我忍不住要制作一个比您看起来正在处理的模型更简单的模型。我通常不使用 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⁰│
└──────────────┴────────┴────────┴────────┴──────┴────────┴────────┘

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

How to write let expression with 'or' condition

alloy