************************************************** * HYMITATOR 1.0 * * Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT * * 2009 - 2012 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * ************************************************** Mode: inverse method. Timed mode is off. Considering file LA02_2.imi. Considering reference valuation in file LA02_2.pi0. Parsing done after 0.009 second. 3 automata, 21 declared labels, 2 analog variables, 1 clock variable, 0 discrete variable, 11 parameters, 14 variables. Program checked and converted after 0.041 second. Performing reachability analysis from state: checker: check_1, job_1: m_0_waiting, job_2: m_4_waiting ==> 231 >= time & time >= 0 & deadline = 231 & wcet_m_0_job_1 = 20 & wcet_m_3_job_1 = 87 & wcet_m_1_job_1 = 31 & wcet_m_4_job_1 = 76 & wcet_m_2_job_1 = 17 & c_1 = 0 & c_2 = 0 Computing post^1 Number of recently found state: 1. 0 states merged. Computing post^2 Number of recently found states: 3. 0 states merged. Computing post^3 Number of recently found states: 6. Found a pi0-incompatible state. Adding the following inequality: 20 < wcet_m_4_job_2 4 states merged. Computing post^4 Number of recently found states: 7. 1 states merged. Computing post^5 Number of recently found states: 10. Found a pi0-incompatible state. Adding the following inequality: 20 < wcet_m_2_job_2 6 states merged. Computing post^6 Number of recently found states: 11. 2 states merged. Computing post^7 Number of recently found states: 14. 6 states merged. Computing post^8 Number of recently found states: 20. 7 states merged. Computing post^9 Number of recently found states: 29. Found a pi0-incompatible state. Adding the following inequality: wcet_m_0_job_2 < 87 Found a pi0-incompatible state. Adding the following inequality: wcet_m_1_job_2 < 20 16 states merged. Computing post^10 Number of recently found states: 39. Found a pi0-incompatible state. Adding the following inequality: 20 < wcet_m_3_job_2 24 states merged. Computing post^11 Number of recently found states: 44. Found a pi0-incompatible state. Adding the following inequality: wcet_m_0_job_2 < 31 24 states merged. Computing post^12 Number of recently found states: 46. Found a pi0-incompatible state. Adding the following inequality: wcet_m_3_job_2 < 87 22 states merged. Computing post^13 Number of recently found states: 46. 25 states merged. Computing post^14 Number of recently found states: 49. 17 states merged. Computing post^15 Number of recently found states: 45. Found a pi0-incompatible state. Adding the following inequality: 17 < wcet_m_0_job_2 Found a pi0-incompatible state. Adding the following inequality: 93 < wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2 25 states merged. Computing post^16 Number of recently found states: 42. 19 states merged. Computing post^17 Number of recently found states: 38. Found a pi0-incompatible state. Adding the following inequality: 93 <= wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_3_job_2 Found a pi0-incompatible state. Adding the following inequality: wcet_m_3_job_2 < 76 + wcet_m_1_job_2 Found a pi0-incompatible state. Adding the following inequality: 17 < wcet_m_1_job_2 19 states merged. Computing post^18 Number of recently found states: 29. 13 states merged. Computing post^19 Number of recently found states: 20. 9 states merged. Computing post^20 Number of recently found states: 13. 4 states merged. Computing post^21 Number of recently found states: 4. 0 states merged. Final constraint K : wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_3_job_2 >= 93 & wcet_m_2_job_2 > 20 & wcet_m_0_job_2 > 17 & wcet_m_1_job_2 > 17 & wcet_m_4_job_2 > 20 & wcet_m_3_job_2 > 20 & 87 > wcet_m_3_job_2 & 20 > wcet_m_1_job_2 & wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2 > 93 & 31 > wcet_m_0_job_2 Fixpoint reached after 21 iterations in 63.39 seconds: 371 reachable states with 528 transitions. invariant cache: filled: 69.% hits : 1181 misses: 138 coll. : 239 flow cache: filled: 69.% hits : 402 misses: 138 coll. : 239 partition cache: filled: 0.% hits : 0 misses: 0 coll. : 0 Final constraint K0 : 20 > wcet_m_1_job_2 & wcet_m_3_job_2 > 31 + wcet_m_1_job_2 & 31 > wcet_m_0_job_2 & 87 > wcet_m_3_job_2 & wcet_m_1_job_2 > 17 & wcet_m_0_job_2 > 17 & wcet_m_2_job_2 > 20 & wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_3_job_2 >= 93 & wcet_m_4_job_2 > 20 & 113 >= wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2 & wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2 > 93 & deadline = 231 & wcet_m_0_job_1 = 20 & wcet_m_3_job_1 = 87 & wcet_m_1_job_1 = 31 & wcet_m_4_job_1 = 76 & wcet_m_2_job_1 = 17 HYMITATOR successfully terminated (after 67.291 seconds)