/*Vorgehensweise mit LTSA:
1. Build -> Compose
2. Im Textfeld RW_CHECK fuer naechstes Compose waehlen
3. Build -> Compose
4. Check -> Safety
*/

const Nread = 2
const Nwrite= 2
range Tread = 1..Nread
range Twrite = 1..Nwrite

READER = (acquire->examine->release->READER).
WRITER = (acquire->modify->release->WRITER).

||RW = (reader[Tread]:READER || writer[Twrite]:WRITER). 

property SAFE_RW =
  (reader[Tread].acquire->READING[1]
  |writer[Twrite].acquire->writer[Twrite].release->SAFE_RW),
READING[i:Tread] =
  (reader[Tread].acquire->READING[i+1]
  |when(i==1) reader[Tread].release -> SAFE_RW
  |when(i>1) reader[Tread].release -> READING[i-1]).

const False = 0
const True  = 1
range Bool  = False..True

RW_LOCK = RWL[0][False],
RWL[readers:0..Nread][writing:Bool] =
	(when (!writing) 
           reader[Tread].acquire -> RWL[readers+1][writing]
    |reader[Tread].release -> RWL[readers-1][writing]
	|when (readers==0 && !writing) 
           writer[Twrite].acquire -> RWL[readers][True]
    |writer[Twrite].release ->  RWL[readers][False]).


||RW_SYS = (RW || RW_LOCK).

||RW_CHECK = (RW_SYS || SAFE_RW).