1 producer – 1 consumer – buffer with capacity 1 (finer) Abstract solution (with guards): # variables just as before Producer ::do true then# invariant I b Deposit: ; B := a; od Consumer ::do true then# invariant I b Fetch: ; aa := B; od
{}