- Phi Init
and always [A] and WF(A)
- Init op = "ready"
and forall in Address: memory()
in MemVal
- A A or A
or A
- A A
or A
- w <op, adr, val,
memory>
- A(,) forall in Address:
( = ) (memory()' = )
and( notequal ) (memory()' = memory())
- Fairness condition:
- Memory eventually responds to each request.
- Processor need not issue requests.