The Algorithm (Q)
Variables: V = {state-name, request, release, used, grant, not-grant}
Invariants on each variable: 1. state-name = S0; 2. buffer-size(request) <= maximum-buffer-size; 3. Buffer-size(release) <= maximum-buffer-size; 4. Used <= 7; 5. Number-of(grant) < 7;
Invariants on pairs: 1. Usedɟ ->grant; …