// File : ws-5-4-3-3.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_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 = (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 Writer Writer ( Reader Reader Reader) RW_reset) ( ((Server Server Server Server Server) Server_group_0 ) Write_buffer_0))