SPL parsing, Textbook Example

local y1, y2 : bool where y1 = false, y2 = false
local      s : [1..2]

P1:: [
    l0: while (true) do [
        l1: noncritical;
        l2: (y1, s) := (true, 1);
        l3: await (!y2 \/ s = 2);
        l4: critical;
        l5: y1 := false
    ]
]

||

P2:: [
    m0: while (true) do [
        m1: noncritical;
        m2: (y2, s) := (true, 2);
        m3: await (!y1 \/ s = 1);
        m4: critical;
    	m5: y2 := false	
    ]
]

---

step-comments@CS.Stanford.EDU