(COMMENT
 Liveness problem: readers-writers synchronization problem
)
(VAR r p x y v1 v2 v3 v4 v5)
(RULES
 Rw ->= RIn(Rw)
 Ww ->= WIn(Ww)
 RAo(R) -> R                                          
 RAn(R) -> R                                          
 WAo(W) -> W                                          
 WAn(W) -> W                                          

 top(ok(sys_r(read(r, RIo(x)), write(W, Ww)))) ->= top(check(sys_r(read(RAo(r), x), write(W, Ww))))
 top(ok(sys_w(read(r, RIo(x)), write(W, Ww)))) ->= top(check(sys_w(read(RAo(r), x), write(W, Ww))))
 top(ok(sys_r(read(r, RIn(x)), write(W, Ww)))) ->= top(check(sys_r(read(RAn(r), x), write(W, Ww))))
 top(ok(sys_w(read(r, RIn(x)), write(W, Ww)))) ->= top(check(sys_w(read(RAn(r), x), write(W, Ww))))
 top(ok(sys_r(read(R, Rw), write(W, WIn(y))))) ->= top(check(sys_r(read(R, Rw), write(WAn(W), y))))
 top(ok(sys_w(read(R, Rw), write(W, WIn(y))))) ->= top(check(sys_w(read(R, Rw), write(WAn(W), y))))
 top(ok(sys_r(read(R, Rw), write(W, WIo(y))))) ->= top(check(sys_r(read(R, Rw), write(WAo(W), y))))
 top(ok(sys_w(read(R, Rw), write(W, WIo(y))))) ->= top(check(sys_w(read(R, Rw), write(WAo(W), y))))
 top(ok(sys_r(read(r, RIo(x)), write(W, y))))  ->= top(check(sys_w(read(RAo(r), x), write(W, y))))
 top(ok(sys_r(read(r, RIn(x)), write(W, y))))  ->= top(check(sys_w(read(RAn(r), x), write(W, y))))
 top(ok(sys_w(read(R, x), write(W, WIo(y)))))  ->= top(check(sys_r(read(R, x), write(WAo(W), y))))
 top(ok(sys_w(read(R, x), write(W, WIn(y)))))  ->= top(check(sys_r(read(R, x), write(WAn(W), y))))

 check(RIo(x)) ->= ok(RIo(x))
 check(RAo(x)) ->= RAo(check(x))
 check(RAn(x)) ->= RAn(check(x))
 check(WAo(x)) ->= WAo(check(x))
 check(WAn(x)) ->= WAn(check(x))
 check(RIo(x)) ->= RIo(check(x))
 check(RIn(x)) ->= RIn(check(x))
 check(WIo(x)) ->= WIo(check(x))
 check(WIn(x)) ->= WIn(check(x))
 check(sys_r(x, y)) ->= sys_r(check(x), y)
 check(sys_r(x, y)) ->= sys_r(x, check(y))
 check(sys_w(x, y)) ->= sys_w(check(x), y)
 check(sys_w(x, y)) ->= sys_w(x, check(y))

 RAo(ok(x)) ->= ok(RAo(x)) 
 RAn(ok(x)) ->= ok(RAn(x)) 
 WAo(ok(x)) ->= ok(WAo(x)) 
 WAn(ok(x)) ->= ok(WAn(x)) 
 RIn(ok(x)) ->= ok(RIn(x)) 
 WIo(ok(x)) ->= ok(WIo(x)) 
 WIn(ok(x)) ->= ok(WIn(x)) 
 sys_r(ok(x), y) ->= ok(sys_r(x, y))
 sys_r(x, ok(y)) ->= ok(sys_r(x, y))
 sys_w(ok(x), y) ->= ok(sys_w(x, y))
 sys_w(x, ok(y)) ->= ok(sys_w(x, y))
)