How to write let expression with 'or' condition

While impleting the question A.3.6 on the book, I need to express a condition like:

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.

How can I express the condition neatly without specifying the conditions when glove is on the right hand and when the glove is on the left hand, since both conditions have the same structure.

My code is here: https://github.com/huanhulan/alloy-exercises/blob/master/book/appendixA/gloves.als#L137

Solution

Maybe not an answer to your question directly, but I could not resist to make a simpler model than you seem to appear to work on. I generally do not use the Time model since it makes almost any problem unwieldy imho. If you go to this route, you might want to checkout Electrum. This is a fork that hides the Time atom effectively and has nice keywords for constraining the past and future.

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

A solution:

┌──────────────┬─────────────────┬────────┬──────┬─────────────────┐
│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⁰│
└──────────────┴────────┴────────┴────────┴──────┴────────┴────────┘