Example: Readers-Writers with Writers Priority

Browse: RWP.csv

Add: Database:1.r,Database:1.w,Database:1.wr,Database:1.ww

Abbreviations: Database:1.r = r,Database:1.w = w,Database:1.wr = wr, Database:1.ww = ww

Sample Properties:

// Basic Readers-Writers Policy

G [ (r > 0 -> w = 0) &&
    (w > 0  -> r = 0) &&
    (w = 0 || w = 1)
  ]

// Writers Priority

G [ (r > 0 && ww > 0 -> r' <= r) ]

// Another way of writing the above

G [ (r > 0 -> w = 0) &&
    (w > 0  -> r = 0) &&
    (w = 0 || w = 1) &&
    (r > 0 && ww > 0 -> r' <= r) 
  ]

// Note: r < r' need not be satisfied

G [ r > 0 && ww > 0 -> r' < r ]