// File : ws-9-8-6-6.pepa


// A PEPA model of a web server which can be scaled by
// varying the number of servers, number of readers, number
// of writers or buffer size.


// Rate definitions
rsf = 1.0;
rsw = 1.0;
rwbw = 1.0;
rrsrr = 1.12;
rsrl = 0.94;
rsfr = 3.0;
rsfsw = 0.9;
rwra = 1.0;
rsgsfra = 2.0;


// Server definitions 
Server = (s_read_request, infty).Server_read + (s_fail, rsf).Server_fail + (s_write, rsw).Server;
Server_read  = (s_read_lookup, rsrl).Server;
Server_fail  = (s_fail_recover, rsfr).Server + (s_fail_recover_all, infty).Server + (s_write, rsfsw).Server_fail;


// Server groups
Server_group_0  = (s_fail, infty).Server_group_1;
Server_group_1 = (s_fail, infty).Server_group_2 + (s_fail_recover, infty).Server_group_0;
Server_group_2 = (s_fail, infty).Server_group_3 + (s_fail_recover, infty).Server_group_1;
Server_group_3 = (s_fail, infty).Server_group_4 + (s_fail_recover, infty).Server_group_2;
Server_group_4 = (s_fail, infty).Server_group_5 + (s_fail_recover, infty).Server_group_3;
Server_group_5 = (s_fail, infty).Server_group_6 + (s_fail_recover, infty).Server_group_4;
Server_group_6 = (s_fail, infty).Server_group_7 + (s_fail_recover, infty).Server_group_5;
Server_group_7 = (s_fail, infty).Server_group_8 + (s_fail_recover, infty).Server_group_6;
Server_group_8 = (s_fail, infty).Server_group_9 + (s_fail_recover, infty).Server_group_7;
Server_group_9 = (s_fail_recover_all, rsgsfra).Server_group_0;


// Write buffer
Write_buffer_0 = (b_write, infty).Write_buffer_1;
Write_buffer_1 = (b_write, infty).Write_buffer_2 + (s_write, infty).Write_buffer_0;
Write_buffer_2 = (b_write, infty).Write_buffer_3 + (s_write, infty).Write_buffer_0;
Write_buffer_3 = (b_write, infty).Write_buffer_4 + (s_write, infty).Write_buffer_0;
Write_buffer_4 = (b_write, infty).Write_buffer_5 + (s_write, infty).Write_buffer_0;
Write_buffer_5 = (b_write, infty).Write_buffer_6 + (s_write, infty).Write_buffer_0;
Write_buffer_6 = (b_write, infty).Write_buffer_7 + (s_write, infty).Write_buffer_0;
Write_buffer_7 = (b_write, infty).Write_buffer_8 + (s_write, infty).Write_buffer_0;
Write_buffer_8 = (s_write, infty).Write_buffer_0;


// Writer definition
Writer      = (b_write,rwbw).Writer_writ;
Writer_writ = (rw_reset_all,infty).Writer;


// Reader component
Reader       = (s_read_request,rrsrr).Reader_next;
Reader_next  = (s_read_lookup, infty).Reader_read;
Reader_read  = (rw_reset_all, infty).Reader;


// Reader/Writer reset
RW_reset = (rw_reset_all, rwra).RW_reset;


// System equation 
((Writer
		<rw_reset_all> Writer
		<rw_reset_all> Writer
		<rw_reset_all> Writer
		<rw_reset_all> Writer
		<rw_reset_all> Writer <rw_reset_all> (
Reader
		<rw_reset_all> Reader
		<rw_reset_all> Reader
		<rw_reset_all> Reader
		<rw_reset_all> Reader
		<rw_reset_all> Reader) <rw_reset_all> RW_reset)
 <b_write,s_read_request,s_read_lookup> (
((Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server
		<s_write,s_fail_recover_all> Server)
 <s_fail,s_fail_recover,s_fail_recover_all> Server_group_0
) <s_write> Write_buffer_0))