PRISM example

properties.pm

const int total_dropped;

S =? [ dropped = total_dropped]

P =? [ (F queue = MAX) & (F "done" & dropped = total_dropped)]

readerwriter.pm

const int REQ; // requests
const int MAX; // maximum size
const double MSG_RATE;

formula rate_read = 1 / (1 + MSG_RATE);
formula rate_write = 1 - rate_read;

formula queue_empty = queue = 0;
formula queue_full = queue = MAX;
formula msg_left = mleft > 0;


//One module, so that we can leave out stutter steps.

// DECISION TABLE
// mleft queue | R?  W?
//  T    empty | F   T
//  T    med   | T   T
//  T    full  | T   F  
//  F    empty | F   F
//  F    med   | T   F
//  F    full  | T   F

module readwrite
mleft: [0..REQ] init REQ;
queue: [0..MAX] init 0;
dropped: [0..REQ] init 0;

[] msg_left & queue_empty -> (queue' = queue + 1) & (mleft' = mleft - 1);
[] msg_left & !(queue_empty | queue_full) ->
	rate_read: (queue' = queue - 1) + 
	rate_write: (queue' = queue + 1) & (mleft' = mleft - 1);
[] msg_left & queue_full 
	& dropped < REQ -> //necessary so the model checker doesn't flip 
	rate_read: (queue' = queue - 1) + 
	rate_write: (mleft' = mleft - 1) & (dropped' = dropped + 1);
[] !msg_left & !queue_empty -> (queue' = queue - 1);
endmodule

label "done" = !msg_left & queue_empty;