# Safety property one: a read request from processor 1 will eventually
# be serviced
AG (( proc1.proc_state = READING ) -> AF (proc1.acknowledge = 1));