Some of the possible errors
Trace extracted from the `backward search space' (not from forward exploration!)
Each formula represents the `minimal' configurations (i.e. it denotes an upward closed set)

The Rule No refers to the model shown in the home page (and in the tech-rep)

init

== Rule 1 ==>

initP(_317,_318)

== Rule 7 ==>

initP(_447,_448) | wf(_440,_448):{_440-_447>0.0}

== Rule 2 ==>

initI(_628,_629) | wf(_623,_629):{_623-_628>0.0}

== Rule 6 ==>

initI(_816,_817) | wf(_811,_817) | rf(_816,_817): {_816-_811< -0.0}

== Rule 6 ==>

initI(_999,_1000) | wf(_999,_1000) | rf(_989,_1000) | pt(_989,_1000,unlock,notowner,_985)

== Rule 5 ==>

wf(_1149,_1150) | pt(_1149,_1150,unlock,owner,read) | rf(_1136,_1150) | pt(_1136,_1150,unlock,notowner,_1132)

== Rule 4 ==>

hWi(_1302,_1303) | pt(_1302,_1303,lock,_1297,_1298) | rf(_1289,_1303) | pt(_1289,_1303,unlock,notowner,_1285)

== Rule 16 ==>

rf(_1450,_1451) | pt(_1450,_1451,unlock,notowner,nil) | pt(_1434,_1451,unlock,owner,write)

== Rule 8 ==>

hRp(_1592,_1593) | pt(_1584,_1593,unlock,owner,write) | pt(_1592,_1593,lock,_1579,_1580)

== Rule 9 ==>

hRe(_1734,_1735) | pt(_1734,_1735,lock,_1729,_1730) | pt(_1718,_1735,_1720,_1721,write)

== Rule 10 ==>

UNSAFE STATES: 
pt(_1868,_1869,_1870,_1871,read) | pt(_1860,_1869,_1862,_1863,write)

(readers and writers access should be mutually exclusive!)

------------------------------------------------------------------------------------------------------

Another possible error trace (Error 3 of [FG98]): read handler interleaved with write handler on the owenr 

...


wf(_1149,_1150) | pt(_1149,_1150,unlock,owner,read) | hrp(_1136,_1150) | pt(_1136,_1150,lock,notowner,_1132)

== Rule 4 ==>

hWi(_1302,_1303) | pt(_1302,_1303,lock,_1297,_1298) | hrp(_1289,_1303) | pt(_1289,_1303,lock,notowner,_1285)

== Rule 16 ==>

hrp(_1450,_1451) | pt(_1450,_1451,lock,notowner,nil) | pt(_1434,_1451,unlock,owner,write)

== Rule 9 ==>

hRe(_1734,_1735) | pt(_1734,_1735,lock,_1729,_1730) | pt(_1718,_1735,_1720,_1721,write)

== Rule 10 ==>

UNSAFE STATES: 
pt(_1868,_1869,_1870,_1871,read) | pt(_1860,_1869,_1862,_1863,write)