// location top : size= 1000, type= compartment; location ra3 in top : size= normal_room, type= compartment; location rb3 in top : size= normal_room, type= compartment; location rc3 in top : size= normal_room, type= compartment; location ha3 in top : size= normal_room, type= compartment; location lw3 in top : size= normal_room, type= compartment; location se3 in top : size= normal_room, type= compartment; location sw3 in top : size= normal_room, type= compartment; location le3 in top : size= normal_room, type= compartment; location out in top : size= normal_room, type= compartment; // // Rooms a and b are connected by doors d_ab location d1_ra3_ha3 in top : size= normal_door, type= compartment;//1 location d2_ra3_ha3 in top : size= normal_door, type= compartment;//2 location d3_ra3_ha3 in top : size= normal_door, type= compartment;//3 location d1_rb3_ha3 in top : size= normal_door, type= compartment;//4 location d2_rb3_ha3 in top : size= normal_door, type= compartment;//5 location d1_rc3_ha3 in top : size= normal_door, type= compartment;//6 location d2_rc3_ha3 in top : size= normal_door, type= compartment;//7 location d1_ha3_le3 in top : size= normal_door, type= compartment;//8 location d1_le3_se3 in top : size= normal_door, type= compartment;//9 location d1_ha3_lw3 in top : size= normal_door, type= compartment;//10 location d1_lw3_sw3 in top : size= normal_door, type= compartment;//11 // out_e is the immaterial door 12 // out_w is the immaterial door 13 normal_room = 100; // used to give a dimension to rooms normal_door = 10; // used to give a dimension to doors big_int = 1000; // a big integer, e.g. for top compartment back = 1; // to tune "wrong" direction if needed // ++++++++++++++++++ Standard parameters from EVAC //ustep = 60; // human speed //udr = 30; // door crossing //r = 60; // reply rate for getting instructions //a = 60; // asking rate for getting instructions //s = 60; // getting releasing a place // in our understanding it becomes: // // to_room_door entering door from room // // from_room_door entering room from door // // to_r_di = time to ask and get information about which door (2 secs) + // time to leave a place (1 sec) + // time to get the door (specific of a door/room) // // from_r_di = time to cross the door + // time to get the place // // = 2 secs + 1 sec = 20 BUT 30 seems to give more accurate results when a door can be crossed by only one individual at the time to_ra3_d1 = 6; // 3 + (60/7); to_ra3_d2 = 6; //3 + (60/7); to_ra3_d3 = 6; //3 + (60/7); to_rb3_d4 = 6; //3 + (60/7); to_rb3_d5 = 6; //3 + (60/7); to_rc3_d6 = 6; //3 + (60/7); to_rc3_d7 = 6; //3 + (60/7); to_ha3_d1 = 10.0 / 3.0; //3 + 4; to_ha3_d2 = 10.0 / 3.0; //3 + 4; to_ha3_d3 = 10.0 / 3.0; //3 + 4; to_ha3_d4 = 10.0 / 3.0; //3 + 4; to_ha3_d5 = 10.0 / 3.0; //3 + 4; to_ha3_d6 = 10.0 / 3.0; //3 + 4; to_ha3_d7 = 10.0 / 3.0; //3 + 4; to_ha3_d8 = 10.0 / 3.0; //3 + 4; to_ha3_d10 = 10.0 / 3.0; //3 + 4; to_le3_d8 = 7.5; //3 + 12; to_le3_d9 = 60.0/13.0; // 3 + 6 ; to_lw3_d10 = 7.5; //3 + 12; to_lw3_d11 = 60.0/13.0; //3 + 6; to_se3_d9 = 60.0/13.0; //3 + 6; to_se3_d12 = 100; to_sw3_d11 = 60.0/13.0; //3 + 6; to_sw3_d13 = 100; door_exit_rate = 20; // if all the same from_d1 = door_exit_rate; from_d2 = door_exit_rate; from_d3 = door_exit_rate; from_d4 = door_exit_rate; from_d5 = door_exit_rate; from_d6 = door_exit_rate; from_d7 = door_exit_rate; from_d8 = door_exit_rate; from_d9 = door_exit_rate; from_d10 = door_exit_rate; from_d11 = door_exit_rate; // ++++++++++++++++++ Path information // // Put the following to 0 if you want only expected path enabled // towards east and west exits bad_for_e = 0; bad_for_w = 0; // ------------------ Path information // DOORS PARAMETERS <<<<<<<< normal_capacity = 2; open_d1 = 1; capacity_d1 = normal_capacity; occupancy_d1 = D1_ra3_e@d1_ra3_ha3 + D1_ra3_w@d1_ra3_ha3 + D1_ha3_e@d1_ra3_ha3 + D1_ha3_w@d1_ra3_ha3; full_d1 = H(capacity_d1 - occupancy_d1); switch_d1 = open_d1*full_d1; open_d2 = 1; capacity_d2 = normal_capacity; occupancy_d2 = D2_ra3_e@d2_ra3_ha3 + D2_ra3_w@d2_ra3_ha3 + D2_ha3_e@d2_ra3_ha3 + D2_ha3_w@d2_ra3_ha3; full_d2 = H(capacity_d2 - occupancy_d2); switch_d2 = open_d2*full_d2; open_d3 = 1; capacity_d3 = normal_capacity; occupancy_d3 = D3_ra3_e@d3_ra3_ha3 + D3_ra3_w@d3_ra3_ha3 + D3_ha3_e@d3_ra3_ha3 + D3_ha3_w@d3_ra3_ha3; full_d3 = H(capacity_d3 - occupancy_d3); switch_d3 = open_d3*full_d3; open_d4 = 1; capacity_d4 = normal_capacity; occupancy_d4 = D4_rb3_e@d1_rb3_ha3 + D4_rb3_w@d1_rb3_ha3 + D4_ha3_e@d1_rb3_ha3 + D4_ha3_w@d1_rb3_ha3; full_d4 = H(capacity_d4 - occupancy_d4); switch_d4 = open_d4*full_d4; open_d5 = 1; capacity_d5 = normal_capacity; occupancy_d5 = D5_rb3_e@d2_rb3_ha3 + D5_rb3_w@d2_rb3_ha3 + D5_ha3_e@d2_rb3_ha3 + D5_ha3_w@d2_rb3_ha3; full_d5 = H(capacity_d5 - occupancy_d5); switch_d5 = open_d5*full_d5; open_d6 = 1; capacity_d6 = normal_capacity; occupancy_d6 = D6_rc3_e@d1_rc3_ha3 + D6_rc3_w@d1_rc3_ha3 + D6_ha3_e@d1_rc3_ha3 + D6_ha3_w@d1_rc3_ha3; full_d6 = H(capacity_d6 - occupancy_d6); switch_d6 = open_d6*full_d6; open_d7 = 1; capacity_d7 = normal_capacity; occupancy_d7 = D7_rc3_e@d2_rc3_ha3 + D7_rc3_w@d2_rc3_ha3 + D7_ha3_e@d2_rc3_ha3 + D7_ha3_w@d2_rc3_ha3; full_d7 = H(capacity_d7 - occupancy_d7); switch_d7 = open_d7*full_d7; open_d8 = 1; capacity_d8 = normal_capacity; occupancy_d8 = D8_le3_e@d1_ha3_le3 + D8_le3_w@d1_ha3_le3 + D8_ha3_e@d1_ha3_le3 + D8_ha3_w@d1_ha3_le3; full_d8 = H(capacity_d8 - occupancy_d8); switch_d8 = open_d8*full_d8; open_d9 = 1; capacity_d9 = normal_capacity; occupancy_d9 = D9_le3_e@d1_le3_se3 + D9_le3_w@d1_le3_se3 + D9_se3_w@d1_le3_se3; full_d9 = H(capacity_d9 - occupancy_d9); switch_d9 = open_d9*full_d9; open_d10 = 1; capacity_d10 = normal_capacity; occupancy_d10 = D10_lw3_e@d1_ha3_lw3 + D10_lw3_w@d1_ha3_lw3 + D10_ha3_e@d1_ha3_lw3 + D10_ha3_w@d1_ha3_lw3; full_d10 = H(capacity_d10 - occupancy_d10); switch_d10 = open_d10*full_d10; open_d11 = 1; capacity_d11 = normal_capacity; occupancy_d11 = D11_lw3_e@d1_lw3_sw3 + D11_lw3_w@d1_lw3_sw3 + D11_sw3_e@d1_lw3_sw3; full_d11 = H(capacity_d11 - occupancy_d11); switch_d11 = open_d11*full_d11; switch_d12 = 1; switch_d13 = 1; // ++++++++++++++++++ Non-negative sanity-check // // Due to implementation, this constraints agents to be present in doors and rooms // before a reaction regarding them can happen. Otherwise, actions with non-zero rates // seem to be enabled even with in absence of agents, whose number would then may become // even negative. ra3e_in_safe = H(RA3e@ra3); ra3w_in_safe = H(RA3w@ra3); ha3e_in_safe = H(HA3e@ha3); ha3w_in_safe = H(HA3w@ha3); rb3e_in_safe = H(RB3e@rb3); rb3w_in_safe = H(RB3w@rb3); rc3e_in_safe = H(RC3e@rc3); rc3w_in_safe = H(RC3w@rc3); le3e_in_safe = H(LE3e@le3); le3w_in_safe = H(LE3w@le3); lw3e_in_safe = H(LW3e@lw3); lw3w_in_safe = H(LW3w@lw3); se3e_in_safe = H(SE3e@se3); se3w_in_safe = H(SE3w@se3); sw3e_in_safe = H(SW3e@sw3); sw3w_in_safe = H(SW3w@sw3); safeD1_ra3_e = H(D1_ra3_e@d1_ra3_ha3); safeD1_ra3_w = H(D1_ra3_w@d1_ra3_ha3); safeD1_ha3_e = H(D1_ha3_e@d1_ra3_ha3); safeD1_ha3_w = H(D1_ha3_w@d1_ra3_ha3); safeD2_ra3_e = H(D2_ra3_e@d2_ra3_ha3); safeD2_ra3_w = H(D2_ra3_w@d2_ra3_ha3); safeD2_ha3_e = H(D2_ha3_e@d2_ra3_ha3); safeD2_ha3_w = H(D2_ha3_w@d2_ra3_ha3); safeD3_ra3_e = H(D3_ra3_e@d3_ra3_ha3); safeD3_ra3_w = H(D3_ra3_w@d3_ra3_ha3); safeD3_ha3_e = H(D3_ha3_e@d3_ra3_ha3); safeD3_ha3_w = H(D3_ha3_w@d3_ra3_ha3); safeD4_rb3_e = H(D4_rb3_e@d1_rb3_ha3); safeD4_rb3_w = H(D4_rb3_w@d1_rb3_ha3); safeD4_ha3_e = H(D4_ha3_e@d1_rb3_ha3); safeD4_ha3_w = H(D4_ha3_w@d1_rb3_ha3); safeD5_rb3_e = H(D5_rb3_e@d2_rb3_ha3); safeD5_rb3_w = H(D5_rb3_w@d2_rb3_ha3); safeD5_ha3_e = H(D5_ha3_e@d2_rb3_ha3); safeD5_ha3_w = H(D5_ha3_w@d2_rb3_ha3); safeD6_rc3_e = H(D6_rc3_e@d1_rc3_ha3); safeD6_rc3_w = H(D6_rc3_w@d1_rc3_ha3); safeD6_ha3_e = H(D6_ha3_e@d1_rc3_ha3); safeD6_ha3_w = H(D6_ha3_w@d1_rc3_ha3); safeD7_rc3_e = H(D7_rc3_e@d2_rc3_ha3); safeD7_rc3_w = H(D7_rc3_w@d2_rc3_ha3); safeD7_ha3_e = H(D7_ha3_e@d2_rc3_ha3); safeD7_ha3_w = H(D7_ha3_w@d2_rc3_ha3); safeD8_ha3_e = H(D8_ha3_e@d1_ha3_le3); safeD8_ha3_w = H(D8_ha3_w@d1_ha3_le3); safeD8_le3_e = H(D8_le3_e@d1_ha3_le3); safeD8_le3_w = H(D8_le3_w@d1_ha3_le3); safeD9_le3_e = H(D9_le3_e@d1_le3_se3); safeD9_le3_w = H(D9_le3_w@d1_le3_se3); safeD9_se3_w = H(D9_se3_w@d1_le3_se3); safeD10_ha3_e = H(D10_ha3_e@d1_ha3_lw3); safeD10_ha3_w = H(D10_ha3_w@d1_ha3_lw3); safeD10_lw3_e = H(D10_lw3_e@d1_ha3_lw3); safeD10_lw3_w = H(D10_lw3_w@d1_ha3_lw3); safeD11_lw3_e = H(D11_lw3_e@d1_lw3_sw3); safeD11_lw3_w = H(D11_lw3_w@d1_lw3_sw3); safeD11_sw3_e = H(D11_sw3_e@d1_lw3_sw3); // ----------------- Non-negative sanity-check // ++++++++++++++++++ Room allowance and occupancy (for plotting purposes) allowance_top = 1; allowance_ra3 = H(211 - RA3e@ra3 - RA3w@ra3); allowance_rb3 = H(92 - RB3e@rb3 - RB3w@rb3); allowance_rc3 = H(99 - RC3e@rc3 - RC3w@rc3); allowance_ha3 = H(133 - HA3e@ha3 - HA3w@ha3); allowance_le3 = H(16 - LE3e@le3 - LE3w@le3); allowance_lw3 = H(25 - LW3e@lw3 - LW3e@lw3); allowance_se3 = H(13 - SE3e@se3 - SE3w@se3); // 13 allowance_sw3 = H(22 - SW3e@sw3 - SW3w@sw3); // 22 allowance_out = 1; occupancy_ra3 = RA3e@ra3 + RA3w@ra3; occupancy_rb3 = RB3e@rb3 + RB3w@rb3; occupancy_rc3 = RC3e@rc3 + RC3w@rc3; occupancy_ha3 = HA3e@ha3 + HA3w@ha3; occupancy_le3 = LE3e@le3 + LE3w@le3; occupancy_lw3 = LW3w@lw3 + LW3e@lw3; occupancy_se3 = SE3e@se3 + SE3w@se3; occupancy_sw3 = SW3e@sw3 + SW3w@sw3; occupancy_out_E = OUT_e@out; occupancy_out_W = OUT_w@out; // ----------------- Room allowance // doors specific properties // Auxiliary functions all_door_occupancy = occupancy_d1 + occupancy_d2 + occupancy_d3 + occupancy_d4 + occupancy_d5 + occupancy_d6 + occupancy_d7 + occupancy_d8 + occupancy_d9 + occupancy_d10 + occupancy_d11; // There are rates to access a door from a room and from a door into a room. // Rates are mediated by capacity constraints and routing algorithms, and ... // To start with, all doors have same in/out rate. // From ra to ha through d1 kineticLawOf ra3e_in__d1_ra3_ha3 : fMA(to_ra3_d1 * switch_d1 * ra3e_in_safe); kineticLawOf ha3e_out__d1_ra3_ha3 : fMA(from_d1 * open_d1 * safeD1_ra3_e * allowance_ha3); kineticLawOf ra3w_in__d1_ra3_ha3 : fMA(to_ra3_d1 *switch_d1 * ra3w_in_safe); kineticLawOf ha3w_out__d1_ra3_ha3 : fMA(from_d1 * open_d1 * safeD1_ra3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d1_ra3_ha3 : fMA(to_ha3_d1 * back * switch_d1 * ha3e_in_safe * bad_for_e); kineticLawOf ra3e_out__d1_ra3_ha3 : fMA(from_d1 * back * open_d1 * safeD1_ha3_e * allowance_ra3); kineticLawOf ha3w_in__d1_ra3_ha3 : fMA(to_ha3_d1 * back * switch_d1 * ha3w_in_safe * bad_for_w); kineticLawOf ra3w_out__d1_ra3_ha3 : fMA(from_d1 * back * open_d1 * safeD1_ha3_w * allowance_ra3); // From ra3 to ha3 through d2 kineticLawOf ra3e_in__d2_ra3_ha3 : fMA(to_ra3_d2 * switch_d2 * ra3e_in_safe); kineticLawOf ha3e_out__d2_ra3_ha3 : fMA(from_d2 * open_d2 * safeD2_ra3_e * allowance_ha3); kineticLawOf ra3w_in__d2_ra3_ha3 : fMA(to_ra3_d2 * switch_d2 * ra3w_in_safe); kineticLawOf ha3w_out__d2_ra3_ha3 : fMA(from_d2 * open_d2 * safeD2_ra3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d2_ra3_ha3 : fMA(to_ha3_d2 * back * switch_d2 * ha3e_in_safe * bad_for_e); kineticLawOf ra3e_out__d2_ra3_ha3 : fMA(from_d2 * back * open_d2 * safeD2_ha3_e * allowance_ra3); kineticLawOf ha3w_in__d2_ra3_ha3 : fMA(to_ha3_d2 * back * switch_d2 * ha3w_in_safe * bad_for_w); kineticLawOf ra3w_out__d2_ra3_ha3 : fMA(from_d2 * back * open_d2 * safeD2_ha3_w * allowance_ra3); // From ra3 to ha3 through d3 kineticLawOf ra3e_in__d3_ra3_ha3 : fMA(to_ra3_d3 * switch_d3 * ra3e_in_safe); kineticLawOf ha3e_out__d3_ra3_ha3 : fMA(from_d3 * open_d3 * safeD3_ra3_e * allowance_ha3); kineticLawOf ra3w_in__d3_ra3_ha3 : fMA(to_ra3_d3 * switch_d3 * ra3w_in_safe); kineticLawOf ha3w_out__d3_ra3_ha3 : fMA(from_d3 * open_d3 * safeD3_ra3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d3_ra3_ha3 : fMA(to_ha3_d3 * back * switch_d3 * ha3e_in_safe * bad_for_e); kineticLawOf ra3e_out__d3_ra3_ha3 : fMA(from_d3 * back * open_d3 * safeD3_ha3_e * allowance_ra3); kineticLawOf ha3w_in__d3_ra3_ha3 : fMA(to_ha3_d3 * back * switch_d3 * ha3w_in_safe * bad_for_w); kineticLawOf ra3w_out__d3_ra3_ha3 : fMA(from_d3 * back * open_d3 * safeD3_ha3_w * allowance_ra3); // From rb to ha through d1 [i.e. d4] ... kineticLawOf rb3e_in__d1_rb3_ha3 : fMA(to_rb3_d4 * switch_d4 * rb3e_in_safe); kineticLawOf ha3e_out__d1_rb3_ha3 : fMA(from_d4 * open_d4 * safeD4_rb3_e * allowance_ha3); kineticLawOf rb3w_in__d1_rb3_ha3 : fMA(to_rb3_d4 * switch_d4 * rb3w_in_safe); kineticLawOf ha3w_out__d1_rb3_ha3 : fMA(from_d4 * open_d4 * safeD4_rb3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d1_rb3_ha3 : fMA(to_ha3_d4 * back * switch_d4 * ha3e_in_safe * bad_for_e); kineticLawOf rb3e_out__d1_rb3_ha3 : fMA(from_d4 * back * open_d4 * safeD4_ha3_e * allowance_rb3); kineticLawOf ha3w_in__d1_rb3_ha3 : fMA(to_ha3_d4 * back * switch_d4 * ha3w_in_safe * bad_for_w); kineticLawOf rb3w_out__d1_rb3_ha3 : fMA(from_d4 * back * open_d4 * safeD4_ha3_w * allowance_rb3); // From rb to ha through d2 [i.e. d5] ... kineticLawOf rb3e_in__d2_rb3_ha3 : fMA(to_rb3_d5 * switch_d5 * rb3e_in_safe); kineticLawOf ha3e_out__d2_rb3_ha3 : fMA(from_d5 * open_d5 * safeD5_rb3_e * allowance_ha3); kineticLawOf rb3w_in__d2_rb3_ha3 : fMA(to_rb3_d5 * switch_d5 * rb3w_in_safe); kineticLawOf ha3w_out__d2_rb3_ha3 : fMA(from_d5 * open_d5 * safeD5_rb3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d2_rb3_ha3 : fMA(to_ha3_d5 * back * switch_d5 * ha3e_in_safe * bad_for_e); kineticLawOf rb3e_out__d2_rb3_ha3 : fMA(from_d5 * back * open_d5 * safeD5_ha3_e * allowance_rb3); kineticLawOf ha3w_in__d2_rb3_ha3 : fMA(to_ha3_d5 * back * switch_d5 * ha3w_in_safe * bad_for_w); kineticLawOf rb3w_out__d2_rb3_ha3 : fMA(from_d5 * back * open_d5 * safeD5_ha3_w * allowance_rb3); // From rc to ha through d1 [i.e. d6] ... kineticLawOf rc3e_in__d1_rc3_ha3 : fMA(to_rc3_d6 * switch_d6 * rc3e_in_safe); kineticLawOf ha3e_out__d1_rc3_ha3 : fMA(from_d6 * open_d6 * safeD6_rc3_e * allowance_ha3); kineticLawOf rc3w_in__d1_rc3_ha3 : fMA(to_rc3_d6 * switch_d6 * rc3w_in_safe); kineticLawOf ha3w_out__d1_rc3_ha3 : fMA(from_d6 * open_d6 * safeD6_rc3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d1_rc3_ha3 : fMA(to_ha3_d6 * back * switch_d6 * ha3e_in_safe * bad_for_e); kineticLawOf rc3e_out__d1_rc3_ha3 : fMA(from_d6 * back * open_d6 * safeD6_ha3_e * allowance_rc3); kineticLawOf ha3w_in__d1_rc3_ha3 : fMA(to_ha3_d6 * back * switch_d6 * ha3w_in_safe * bad_for_w); kineticLawOf rc3w_out__d1_rc3_ha3 : fMA(from_d6 * back * open_d6 * safeD6_ha3_w * allowance_rc3); // From rc to ha through d2 [i.e. d7] ... kineticLawOf rc3e_in__d2_rc3_ha3 : fMA(to_rc3_d7 * switch_d7 * rc3e_in_safe); kineticLawOf ha3e_out__d2_rc3_ha3 : fMA(from_d7 * open_d7 * safeD7_rc3_e * allowance_ha3); kineticLawOf rc3w_in__d2_rc3_ha3 : fMA(to_rc3_d7 * switch_d7 * rc3w_in_safe); kineticLawOf ha3w_out__d2_rc3_ha3 : fMA(from_d7 * open_d7 * safeD7_rc3_w * allowance_ha3); // ... and back kineticLawOf ha3e_in__d2_rc3_ha3 : fMA(to_ha3_d7 * back * switch_d7 * ha3e_in_safe * bad_for_e); kineticLawOf rc3e_out__d2_rc3_ha3 : fMA(from_d7 * back * open_d7 * safeD7_ha3_e * allowance_rc3); kineticLawOf ha3w_in__d2_rc3_ha3 : fMA(to_ha3_d7 * back * switch_d7 * ha3w_in_safe * bad_for_w); kineticLawOf rc3w_out__d2_rc3_ha3 : fMA(from_d7 * back * open_d7 * safeD7_ha3_w * allowance_rc3); // From ha to le through d1 [i.e. d8] ... kineticLawOf ha3e_in__d1_ha3_le3 : fMA(to_ha3_d8 * switch_d8 * ha3e_in_safe); kineticLawOf le3e_out__d1_ha3_le3 : fMA(from_d8 * open_d8 * safeD8_ha3_e * allowance_le3); kineticLawOf ha3w_in__d1_ha3_le3 : fMA(to_ha3_d8 * switch_d8 * ha3w_in_safe * bad_for_w); kineticLawOf le3w_out__d1_ha3_le3 : fMA(from_d8 * open_d8 * safeD8_ha3_w * allowance_le3); // ... and back kineticLawOf le3e_in__d1_ha3_le3 : fMA(to_le3_d8 * back * switch_d8 * le3e_in_safe * bad_for_e); kineticLawOf ha3e_out__d1_ha3_le3 : fMA(from_d8 * back * open_d8 * safeD8_le3_e * allowance_ha3); kineticLawOf le3w_in__d1_ha3_le3 : fMA(to_le3_d8 * back * switch_d8 * le3w_in_safe * bad_for_w); kineticLawOf ha3w_out__d1_ha3_le3 : fMA(from_d8 * back * open_d8 * safeD8_le3_w * allowance_ha3); // From le to se through d1 [d9] kineticLawOf le3e_in__d1_le3_se3 : fMA(to_le3_d9 * switch_d9 * le3e_in_safe); kineticLawOf se3e_out__d1_le3_se3 : fMA(from_d9 * open_d9 * safeD9_le3_e * allowance_se3); kineticLawOf le3w_in__d1_le3_se3 : fMA(to_le3_d9 * switch_d9 * le3w_in_safe * bad_for_w); kineticLawOf se3w_out__d1_le3_se3 : fMA(from_d9 * open_d9 * safeD9_le3_w * allowance_se3); // ... and back //kineticLawOf se3e_in__d1_le3_se3 : back; check this rate //kineticLawOf le3e_out__d1_le3_se3 : back; check this rate kineticLawOf se3w_in__d1_le3_se3 : fMA(to_se3_d9 * back * switch_d9 * se3w_in_safe * bad_for_w); kineticLawOf le3w_out__d1_le3_se3 : fMA(from_d9 * back * open_d9 * safeD9_se3_w * allowance_le3); // From ha to lw through d1 [d10] kineticLawOf ha3e_in__d1_ha3_lw3 : fMA(to_ha3_d10 * switch_d10 * ha3e_in_safe * bad_for_e); kineticLawOf lw3e_out__d1_ha3_lw3 : fMA(from_d10 * open_d10 * safeD10_ha3_e * allowance_lw3); kineticLawOf ha3w_in__d1_ha3_lw3 : fMA(to_ha3_d10 * switch_d10 * ha3w_in_safe); kineticLawOf lw3w_out__d1_ha3_lw3 : fMA(from_d10 * open_d10 * safeD10_ha3_w * allowance_lw3); // ... and back kineticLawOf lw3e_in__d1_ha3_lw3 : fMA(to_lw3_d10 * back * switch_d10 * lw3e_in_safe * bad_for_e); kineticLawOf ha3e_out__d1_ha3_lw3 : fMA(from_d10 * back * open_d10 * safeD10_lw3_e * allowance_ha3); kineticLawOf lw3w_in__d1_ha3_lw3 : fMA(to_lw3_d10 * back * switch_d10 * lw3w_in_safe * bad_for_w); kineticLawOf ha3w_out__d1_ha3_lw3 : fMA(from_d10 * back * open_d10 * safeD10_lw3_w * allowance_ha3); // From lw to sw through d1 [d11] kineticLawOf lw3e_in__d1_lw3_sw3 : fMA(to_lw3_d11 * switch_d11 * lw3e_in_safe * bad_for_e); kineticLawOf sw3e_out__d1_lw3_sw3 : fMA(from_d11 * open_d11 * safeD11_lw3_e * allowance_sw3); kineticLawOf lw3w_in__d1_lw3_sw3 : fMA(to_lw3_d11 * switch_d11 * lw3w_in_safe); kineticLawOf sw3w_out__d1_lw3_sw3 : fMA(from_d11 * open_d11 * safeD11_lw3_w * allowance_sw3); // ... and back kineticLawOf sw3e_in__d1_lw3_sw3 : fMA(to_sw3_d11 * back * switch_d11 * sw3e_in_safe * bad_for_e); kineticLawOf lw3e_out__d1_lw3_sw3 : fMA(from_d11 * back * open_d11 * safeD11_sw3_e * allowance_lw3); //kineticLawOf sw3w_in__d1_lw3_sw3 : back * switch_d9; //kineticLawOf lw3w_out__d1_lw3_sw3 : back; // Exit kineticLawOf se3e_in__d1_se3_out : fMA(to_se3_d12 * switch_d12 * se3e_in_safe); kineticLawOf sw3w_in__d1_sw3_out : fMA(to_sw3_d13 * switch_d13 * sw3w_in_safe); // Evac have different behavior in different rooms // Process Pe stays in room p and want to go towards e exit. // It can either enter in a door between two rooms, e.g. ra3e_in_d1_ra3_ha3, // or exit from a door in which it has entered as a different process, // e.g. ra3e_out_d1_ra3_ha3say. That is, action names are relative to the // process in the room viewpoint. There are in/out action for any door for any // kind of process, i.e. process with destination est or west. RA3e = (ra3e_in__d1_ra3_ha3, 1) << RA3e@ra3 + (ra3e_in__d2_ra3_ha3, 1) << RA3e@ra3 + (ra3e_in__d3_ra3_ha3, 1) << RA3e@ra3 + (ra3e_out__d1_ra3_ha3, 1) >> RA3e@ra3 + (ra3e_out__d2_ra3_ha3, 1) >> RA3e@ra3 + (ra3e_out__d3_ra3_ha3, 1) >> RA3e@ra3; RA3w = (ra3w_in__d1_ra3_ha3, 1) << RA3w@ra3 + (ra3w_in__d2_ra3_ha3, 1) << RA3w@ra3 + (ra3w_in__d3_ra3_ha3, 1) << RA3w@ra3 + (ra3w_out__d1_ra3_ha3, 1) >> RA3w@ra3 + (ra3w_out__d2_ra3_ha3, 1) >> RA3w@ra3 + (ra3w_out__d3_ra3_ha3, 1) >> RA3w@ra3; HA3e = (ha3e_in__d1_ha3_le3, 1) << HA3e@ha3 + (ha3e_in__d1_ha3_lw3, 1) << HA3e@ha3 + (ha3e_in__d1_ra3_ha3, 1) << HA3e@ha3 + (ha3e_in__d2_ra3_ha3, 1) << HA3e@ha3 + (ha3e_in__d3_ra3_ha3, 1) << HA3e@ha3 + (ha3e_in__d1_rb3_ha3, 1) << HA3e@ha3 + (ha3e_in__d2_rb3_ha3, 1) << HA3e@ha3 + (ha3e_in__d1_rc3_ha3, 1) << HA3e@ha3 + (ha3e_in__d2_rc3_ha3, 1) << HA3e@ha3 + (ha3e_out__d1_ha3_le3, 1) >> HA3e@ha3 + (ha3e_out__d1_ha3_lw3, 1) >> HA3e@ha3 + (ha3e_out__d1_ra3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d2_ra3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d3_ra3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d1_rb3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d2_rb3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d1_rc3_ha3, 1) >> HA3e@ha3 + (ha3e_out__d2_rc3_ha3, 1) >> HA3e@ha3; HA3w = (ha3w_in__d1_ha3_le3, 1) << HA3w@ha3 + (ha3w_in__d1_ha3_lw3, 1) << HA3w@ha3 + (ha3w_in__d1_ra3_ha3, 1) << HA3w@ha3 + (ha3w_in__d2_ra3_ha3, 1) << HA3w@ha3 + (ha3w_in__d3_ra3_ha3, 1) << HA3w@ha3 + (ha3w_in__d1_rb3_ha3, 1) << HA3w@ha3 + (ha3w_in__d2_rb3_ha3, 1) << HA3w@ha3 + (ha3w_in__d1_rc3_ha3, 1) << HA3w@ha3 + (ha3w_in__d2_rc3_ha3, 1) << HA3w@ha3 + (ha3w_out__d1_ha3_le3, 1) >> HA3w@ha3 + (ha3w_out__d1_ha3_lw3, 1) >> HA3w@ha3 + (ha3w_out__d1_ra3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d2_ra3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d3_ra3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d1_rb3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d2_rb3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d1_rc3_ha3, 1) >> HA3w@ha3 + (ha3w_out__d2_rc3_ha3, 1) >> HA3w@ha3; RB3e = (rb3e_in__d1_rb3_ha3, 1) << RB3e@rb3 + (rb3e_in__d2_rb3_ha3, 1) << RB3e@rb3 + (rb3e_out__d1_rb3_ha3, 1) >> RB3e@rb3 + (rb3e_out__d2_rb3_ha3, 1) >> RB3e@rb3; RB3w = (rb3w_in__d1_rb3_ha3, 1) << RB3w@rb3 + (rb3w_in__d2_rb3_ha3, 1) << RB3w@rb3 + (rb3w_out__d1_rb3_ha3, 1) >> RB3w@rb3 + (rb3w_out__d2_rb3_ha3, 1) >> RB3w@rb3; RC3e = (rc3e_in__d1_rc3_ha3, 1) << RC3e@rc3 + (rc3e_in__d2_rc3_ha3, 1) << RC3e@rc3 + (rc3e_out__d1_rc3_ha3, 1) >> RC3e@rc3 + (rc3e_out__d2_rc3_ha3, 1) >> RC3e@rc3; RC3w = (rc3w_in__d1_rc3_ha3, 1) << RC3w@rc3 + (rc3w_in__d2_rc3_ha3, 1) << RC3w@rc3 + (rc3w_out__d1_rc3_ha3, 1) >> RC3w@rc3 + (rc3w_out__d2_rc3_ha3, 1) >> RC3w@rc3; LE3e = (le3e_in__d1_le3_se3, 1) << LE3e@le3 + (le3e_in__d1_ha3_le3, 1) << LE3e@le3 + // (le3e_out__d1_le3_se3, 1) >> LE3e@le3 + (le3e_out__d1_ha3_le3, 1) >> LE3e@le3; LE3w = (le3w_in__d1_le3_se3, 1) << LE3w@le3 + (le3w_in__d1_ha3_le3, 1) << LE3w@le3 + (le3w_out__d1_le3_se3, 1) >> LE3w@le3 + (le3w_out__d1_ha3_le3, 1) >> LE3w@le3; SE3e = (se3e_in__d1_se3_out, 1) << SE3e@se3 + (se3e_out__d1_le3_se3, 1) >> SE3e@se3; SE3w = (se3w_in__d1_le3_se3, 1) << SE3w@se3 + (se3w_out__d1_le3_se3, 1) >> SE3w@se3; LW3e = (lw3e_in__d1_lw3_sw3, 1) << LW3e@lw3 + (lw3e_in__d1_ha3_lw3, 1) << LW3e@lw3 + (lw3e_out__d1_lw3_sw3, 1) >> LW3e@lw3 + (lw3e_out__d1_ha3_lw3, 1) >> LW3e@lw3; LW3w = (lw3w_in__d1_lw3_sw3, 1) << LW3w@lw3 + (lw3w_in__d1_ha3_lw3, 1) << LW3w@lw3 + // (lw3w_out__d1_lw3_sw3, 1) >> LW3w@lw3 + (lw3w_out__d1_ha3_lw3, 1) >> LW3w@lw3; SW3w = (sw3w_in__d1_sw3_out, 1) << SW3w@sw3 + (sw3w_out__d1_lw3_sw3, 1) >> SW3w@sw3; SW3e = (sw3e_in__d1_lw3_sw3, 1) << SW3e@sw3 + (sw3e_out__d1_lw3_sw3, 1) >> SW3e@sw3; // Process P_D is a process crossing door D from [being] P, // with final destination e or w. // Hence, RA3e_d1 comes from RA3 through door d1, is hence going towards // ha3 [given the door d1] with final destination e. D1_ra3_e = (ra3e_in__d1_ra3_ha3, 1) >> D1_ra3_e@d1_ra3_ha3 + (ha3e_out__d1_ra3_ha3, 1) << D1_ra3_e@d1_ra3_ha3; D1_ra3_w = (ra3w_in__d1_ra3_ha3, 1) >> D1_ra3_w@d1_ra3_ha3 + (ha3w_out__d1_ra3_ha3, 1) << D1_ra3_w@d1_ra3_ha3; D1_ha3_e = (ha3e_in__d1_ra3_ha3, 1) >> D1_ha3_e@d1_ra3_ha3 + (ra3e_out__d1_ra3_ha3, 1) << D1_ha3_e@d1_ra3_ha3; D1_ha3_w = (ha3w_in__d1_ra3_ha3, 1) >> D1_ha3_w@d1_ra3_ha3 + (ra3w_out__d1_ra3_ha3, 1) << D1_ha3_w@d1_ra3_ha3; D2_ra3_e = (ra3e_in__d2_ra3_ha3, 1) >> D2_ra3_e@d2_ra3_ha3 + (ha3e_out__d2_ra3_ha3, 1) << D2_ra3_e@d2_ra3_ha3; D2_ra3_w = (ra3w_in__d2_ra3_ha3, 1) >> D2_ra3_w@d2_ra3_ha3 + (ha3w_out__d2_ra3_ha3, 1) << D2_ra3_w@d2_ra3_ha3; D2_ha3_e = (ha3e_in__d2_ra3_ha3, 1) >> D2_ha3_e@d2_ra3_ha3 + (ra3e_out__d2_ra3_ha3, 1) << D2_ha3_e@d2_ra3_ha3; D2_ha3_w = (ha3w_in__d2_ra3_ha3, 1) >> D2_ha3_w@d2_ra3_ha3 + (ra3w_out__d2_ra3_ha3, 1) << D2_ha3_w@d2_ra3_ha3; D3_ra3_e = (ra3e_in__d3_ra3_ha3, 1) >> D3_ra3_e@d3_ra3_ha3 + (ha3e_out__d3_ra3_ha3, 1) << D3_ra3_e@d3_ra3_ha3; D3_ra3_w = (ra3w_in__d3_ra3_ha3, 1) >> D3_ra3_w@d3_ra3_ha3 + (ha3w_out__d3_ra3_ha3, 1) << D3_ra3_w@d3_ra3_ha3; D3_ha3_e = (ha3e_in__d3_ra3_ha3, 1) >> D3_ha3_e@d3_ra3_ha3 + (ra3e_out__d3_ra3_ha3, 1) << D3_ha3_e@d3_ra3_ha3; D3_ha3_w = (ha3w_in__d3_ra3_ha3, 1) >> D3_ha3_w@d3_ra3_ha3 + (ra3w_out__d3_ra3_ha3, 1) << D3_ha3_w@d3_ra3_ha3; D4_rb3_e = (rb3e_in__d1_rb3_ha3, 1) >> D4_rb3_e@d1_rb3_ha3 + (ha3e_out__d1_rb3_ha3, 1) << D4_rb3_e@d1_rb3_ha3; D4_rb3_w = (rb3w_in__d1_rb3_ha3, 1) >> D4_rb3_w@d1_rb3_ha3 + (ha3w_out__d1_rb3_ha3, 1) << D4_rb3_w@d1_rb3_ha3; D4_ha3_e = (ha3e_in__d1_rb3_ha3, 1) >> D4_ha3_e@d1_rb3_ha3 + (rb3e_out__d1_rb3_ha3, 1) << D4_ha3_e@d1_rb3_ha3; D4_ha3_w = (ha3w_in__d1_rb3_ha3, 1) >> D4_ha3_w@d1_rb3_ha3 + (rb3w_out__d1_rb3_ha3, 1) << D4_ha3_w@d1_rb3_ha3; D5_rb3_e = (rb3e_in__d2_rb3_ha3, 1) >> D5_rb3_e@d2_rb3_ha3 + (ha3e_out__d2_rb3_ha3, 1) << D5_rb3_e@d2_rb3_ha3; D5_rb3_w = (rb3w_in__d2_rb3_ha3, 1) >> D5_rb3_w@d2_rb3_ha3 + (ha3w_out__d2_rb3_ha3, 1) << D5_rb3_w@d2_rb3_ha3; D5_ha3_e = (ha3e_in__d2_rb3_ha3, 1) >> D5_ha3_e@d2_rb3_ha3 + (rb3e_out__d2_rb3_ha3, 1) << D5_ha3_e@d2_rb3_ha3; D5_ha3_w = (ha3w_in__d2_rb3_ha3, 1) >> D5_ha3_w@d2_rb3_ha3 + (rb3w_out__d2_rb3_ha3, 1) << D5_ha3_w@d2_rb3_ha3; D6_rc3_e = (rc3e_in__d1_rc3_ha3, 1) >> D6_rc3_e@d1_rc3_ha3 + (ha3e_out__d1_rc3_ha3, 1) << D6_rc3_e@d1_rc3_ha3; D6_rc3_w = (rc3w_in__d1_rc3_ha3, 1) >> D6_rc3_w@d1_rc3_ha3 + (ha3w_out__d1_rc3_ha3, 1) << D6_rc3_w@d1_rc3_ha3; D6_ha3_e = (ha3e_in__d1_rc3_ha3, 1) >> D6_ha3_e@d1_rc3_ha3 + (rc3e_out__d1_rc3_ha3, 1) << D6_ha3_e@d1_rc3_ha3; D6_ha3_w = (ha3w_in__d1_rc3_ha3, 1) >> D6_ha3_w@d1_rc3_ha3 + (rc3w_out__d1_rc3_ha3, 1) << D6_ha3_w@d1_rc3_ha3; D7_rc3_e = (rc3e_in__d2_rc3_ha3, 1) >> D7_rc3_e@d2_rc3_ha3 + (ha3e_out__d2_rc3_ha3, 1) << D7_rc3_e@d2_rc3_ha3; D7_rc3_w = (rc3w_in__d2_rc3_ha3, 1) >> D7_rc3_w@d2_rc3_ha3 + (ha3w_out__d2_rc3_ha3, 1) << D7_rc3_w@d2_rc3_ha3; D7_ha3_e = (ha3e_in__d2_rc3_ha3, 1) >> D7_ha3_e@d2_rc3_ha3 + (rc3e_out__d2_rc3_ha3, 1) << D7_ha3_e@d2_rc3_ha3; D7_ha3_w = (ha3w_in__d2_rc3_ha3, 1) >> D7_ha3_w@d2_rc3_ha3 + (rc3w_out__d2_rc3_ha3, 1) << D7_ha3_w@d2_rc3_ha3; D8_ha3_e = (ha3e_in__d1_ha3_le3, 1) >> D8_ha3_e@d1_ha3_le3 + (le3e_out__d1_ha3_le3, 1) << D8_ha3_e@d1_ha3_le3; D8_ha3_w = (ha3w_in__d1_ha3_le3, 1) >> D8_ha3_w@d1_ha3_le3 + (le3w_out__d1_ha3_le3, 1) << D8_ha3_w@d1_ha3_le3; D8_le3_e = (le3e_in__d1_ha3_le3, 1) >> D8_le3_e@d1_ha3_le3 + (ha3e_out__d1_ha3_le3, 1) << D8_le3_e@d1_ha3_le3; D8_le3_w = (le3w_in__d1_ha3_le3, 1) >> D8_le3_w@d1_ha3_le3 + (ha3w_out__d1_ha3_le3, 1) << D8_le3_w@d1_ha3_le3; D9_le3_e = (le3e_in__d1_le3_se3, 1) >> D9_le3_e@d1_le3_se3 + (se3e_out__d1_le3_se3, 1) << D9_le3_e@d1_le3_se3; D9_le3_w = (le3w_in__d1_le3_se3, 1) >> D9_le3_w@d1_le3_se3 + (se3w_out__d1_le3_se3, 1) << D9_le3_w@d1_le3_se3; // D9_se3_e = (se3e_in__d1_le3_se3, 1) >> D9_se3_e@d1_le3_se3 + // (le3e_out__d1_le3_se3, 1) << D9_se3_e@d1_le3_se3; D9_se3_w = (se3w_in__d1_le3_se3, 1) >> D9_se3_w@d1_le3_se3 + (le3w_out__d1_le3_se3, 1) << D9_se3_w@d1_le3_se3; D10_ha3_e = (ha3e_in__d1_ha3_lw3, 1) >> D10_ha3_e@d1_ha3_lw3 + (lw3e_out__d1_ha3_lw3, 1) << D10_ha3_e@d1_ha3_lw3; D10_ha3_w = (ha3w_in__d1_ha3_lw3, 1) >> D10_ha3_w@d1_ha3_lw3 + (lw3w_out__d1_ha3_lw3, 1) << D10_ha3_w@d1_ha3_lw3; D10_lw3_e = (lw3e_in__d1_ha3_lw3, 1) >> D10_lw3_e@d1_ha3_lw3 + (ha3e_out__d1_ha3_lw3, 1) << D10_lw3_e@d1_ha3_lw3; D10_lw3_w = (lw3w_in__d1_ha3_lw3, 1) >> D10_lw3_w@d1_ha3_lw3 + (ha3w_out__d1_ha3_lw3, 1) << D10_lw3_w@d1_ha3_lw3; D11_lw3_e = (lw3e_in__d1_lw3_sw3, 1) >> D11_lw3_e@d1_lw3_sw3 + (sw3e_out__d1_lw3_sw3, 1) << D11_lw3_e@d1_lw3_sw3; D11_lw3_w = (lw3w_in__d1_lw3_sw3, 1) >> D11_lw3_w@d1_lw3_sw3 + (sw3w_out__d1_lw3_sw3, 1) << D11_lw3_w@d1_lw3_sw3; D11_sw3_e = (sw3e_in__d1_lw3_sw3, 1) >> D11_sw3_e@d1_lw3_sw3 + (lw3e_out__d1_lw3_sw3, 1) << D11_sw3_e@d1_lw3_sw3; // D11_sw3_w = (sw3w_in__d1_lw3_sw3, 1) >> D11_sw3_w@d1_lw3_sw3 + // (lw3w_out__d1_lw3_sw3, 1) << D11_sw3_w@d1_lw3_sw3; OUT_e = (se3e_in__d1_se3_out, 1) >> OUT_e@out; OUT_w = (sw3w_in__d1_sw3_out, 1) >> OUT_w@out; third_floor ::= ( RA3e@ra3[18] <> // 18 RA3w@ra3[18] <> // 18 HA3e@ha3[0] <> HA3w@ha3[0] <> RB3e@rb3[0] <> RB3w@rb3[16] <> // 16 RC3e@rc3[18] <> // 18 RC3w@rc3[0] <> LE3e@le3[0] <> LE3w@le3[0] <> SE3e@se3[0] <> SE3w@se3[0] <> LW3e@lw3[0] <> LW3w@lw3[0] <> SW3w@sw3[0] <> SW3e@sw3[0] ) <*> ( D1_ra3_e@d1_ra3_ha3[0] <> D1_ra3_w@d1_ra3_ha3[0] <> D1_ha3_e@d1_ra3_ha3[0] <> D1_ha3_w@d1_ra3_ha3[0] <> D2_ra3_e@d2_ra3_ha3[0] <> D2_ra3_w@d2_ra3_ha3[0] <> D2_ha3_e@d2_ra3_ha3[0] <> D2_ha3_w@d2_ra3_ha3[0] <> D3_ra3_e@d3_ra3_ha3[0] <> D3_ra3_w@d3_ra3_ha3[0] <> D3_ha3_e@d3_ra3_ha3[0] <> D3_ha3_w@d3_ra3_ha3[0] <> D4_rb3_e@d1_rb3_ha3[0] <> D4_rb3_w@d1_rb3_ha3[0] <> D4_ha3_e@d1_rb3_ha3[0] <> D4_ha3_w@d1_rb3_ha3[0] <> D5_rb3_e@d2_rb3_ha3[0] <> D5_rb3_w@d2_rb3_ha3[0] <> D5_ha3_e@d2_rb3_ha3[0] <> D5_ha3_w@d2_rb3_ha3[0] <> D6_rc3_e@d1_rc3_ha3[0] <> D6_rc3_w@d1_rc3_ha3[0] <> D6_ha3_e@d1_rc3_ha3[0] <> D6_ha3_w@d1_rc3_ha3[0] <> D7_rc3_e@d2_rc3_ha3[0] <> D7_rc3_w@d2_rc3_ha3[0] <> D7_ha3_e@d2_rc3_ha3[0] <> D7_ha3_w@d2_rc3_ha3[0] <> D8_ha3_e@d1_ha3_le3[0] <> D8_ha3_w@d1_ha3_le3[0] <> D8_le3_e@d1_ha3_le3[0] <> D8_le3_w@d1_ha3_le3[0] <> D9_le3_e@d1_le3_se3[0] <> D9_le3_w@d1_le3_se3[0] <> // D9_se3_e@d1_le3_se3[0] <> D9_se3_w@d1_le3_se3[0] <> D10_ha3_e@d1_ha3_lw3[0] <> D10_ha3_w@d1_ha3_lw3[0] <> D10_lw3_e@d1_ha3_lw3[0] <> D10_lw3_w@d1_ha3_lw3[0] <> D11_lw3_e@d1_lw3_sw3[0] <> D11_lw3_w@d1_lw3_sw3[0] <> D11_sw3_e@d1_lw3_sw3[0] <> // D11_sw3_w@d1_lw3_sw3[0] <> OUT_e@out[0] <> OUT_w@out[0] ); third_floor