Example: Readers-Writers with Writers Priority Browse: readers_writers_trace_may6 Add: Database:1.r,Database:1.w,Database:1.wr,Database:1.ww, Database:1.data Abbreviations: Database:1.r = r,Database:1.w = w,Database:1.wr = wr, Database:1.ww = ww, Database:1.data = data Sample Properties: // Basic Readers-Writers Policy G [ (r > 0 -> w = 0) && (w > 0 -> r = 0) && (w = 0 || w = 1) ]; // data is in ascending order G [ data' >= data ]; // data does not change when readers are in progress G [ r > 0 -> data == data' ]; // ---------------- // Writers Priority: Must re-program for priority and set ww // ---------------- 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 ]; // A more complex way of writing writers priority G [ r > 0 && ww > 0 -> for(N, 1:r, F[r == N && F[r == N-1]]) ]