************************************************** * HYMITATOR 1.0 * * Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT * * 2009 - 2012 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * ************************************************** Mode: inverse method. Parsing done after 0.006 second. Program checked and converted after 0.035 second. Computing post^1 0 states merged. Computing post^2 Adding the following inequality (randomly selected among 2 inequalities): Off1 < WCET_2 + Off2 Adding the following inequality (randomly selected among 2 inequalities): Off3 < WCET_1 + Off1 Adding the following inequality (randomly selected among 2 inequalities): Off2 < WCET_3 + Off3 0 states merged. Computing post^3 Adding the following inequality: Off2 < WCET_1 + Off1 2 states merged. Computing post^4 0 states merged. Computing post^5 Adding the following inequality: WCET_2 + WCET_1 <= per1 0 states merged. Computing post^6 Adding the following inequality (randomly selected among 2 inequalities): WCET_3 + WCET_2 + WCET_1 <= per2 Adding the following inequality: per1 + Off1 < WCET_3 + WCET_2 + WCET_1 + Off2 Adding the following inequality: per1 < WCET_3 + WCET_2 + WCET_1 Adding the following inequality: per1 + Off1 < WCET_3 + WCET_2 + WCET_1 + Off3 1 states merged. Computing post^7 Adding the following inequality: WCET_1 + per1 + Off1 <= per2 + Off2 0 states merged. Computing post^8 Adding the following inequality: WCET_3 + WCET_2 + 2*WCET_1 <= per2 Adding the following inequality: WCET_3 + WCET_2 + 2*WCET_1 + Off2 <= 2*per1 + Off1 0 states merged. Computing post^9 Adding the following inequality: per2 + Off2 < 2*per1 + Off1 Adding the following inequality: per2 + Off2 < per3 + Off3 0 states merged. Computing post^10 Adding the following inequality: WCET_2 + per2 + Off2 <= 2*per1 + Off1 Adding the following inequality: WCET_2 + per2 + Off2 <= per3 + Off3 0 states merged. Computing post^11 Adding the following inequality: 2*per1 + Off1 < per3 + Off3 0 states merged. Computing post^12 Adding the following inequality: WCET_1 + 2*per1 + Off1 <= per3 + Off3 0 states merged. Computing post^13 Adding the following inequality: 3*per1 + Off1 < 2*per2 + Off2 Adding the following inequality: 3*per1 + Off1 < per3 + Off3 0 states merged. Computing post^14 Adding the following inequality: WCET_1 + 3*per1 + Off1 <= 2*per2 + Off2 Adding the following inequality: WCET_1 + 3*per1 + Off1 <= per3 + Off3 0 states merged. Computing post^15 0 states merged. Computing post^16 Adding the following inequality: per3 + Off3 < WCET_2 + 2*per2 + Off2 0 states merged. Computing post^17 0 states merged. Computing post^18 0 states merged. Computing post^19 0 states merged. Computing post^20 Adding the following inequality: WCET_3 + WCET_2 + WCET_1 + 2*per2 + Off2 <= 5*per1 + Off1 0 states merged. Computing post^21 6 states merged. Computing post^22 Adding the following inequality: 3*per2 + Off2 < WCET_1 + 5*per1 + Off1 Adding the following inequality: 5*per1 + Off1 < WCET_2 + 3*per2 + Off2 0 states merged. Computing post^23 0 states merged. Computing post^24 0 states merged. Computing post^25 3 states merged. Computing post^26 0 states merged. Computing post^27 Adding the following inequality (randomly selected among 2 inequalities): 4*per2 + Off2 < 7*per1 + Off1 0 states merged. Computing post^28 Adding the following inequality: 2*per3 + Off3 < WCET_2 + 4*per2 + Off2 Adding the following inequality: 2*per3 + Off3 < 7*per1 + Off1 Adding the following inequality: 4*per2 + Off2 < WCET_3 + 2*per3 + Off3 0 states merged. Computing post^29 Adding the following inequality: WCET_2 + 4*per2 + Off2 <= 7*per1 + Off1 0 states merged. Computing post^30 0 states merged. Computing post^31 0 states merged. Computing post^32 Adding the following inequality: WCET_3 + WCET_2 + WCET_1 + 4*per2 + Off2 <= 8*per1 + Off1 0 states merged. Computing post^33 Adding the following inequality: 8*per1 + Off1 < 5*per2 + Off2 3 states merged. Computing post^34 Adding the following inequality: WCET_1 + 8*per1 + Off1 <= 5*per2 + Off2 0 states merged. Computing post^35 0 states merged. Computing post^36 0 states merged. Computing post^37 0 states merged. Computing post^38 0 states merged. Computing post^39 0 states merged. Computing post^40 Adding the following inequality (randomly selected among 3 inequalities): deadlineBasic < WCET_3 + 3*per3 + Off3 Adding the following inequality (randomly selected among 3 inequalities): deadlineBasic < WCET_2 + 6*per2 + Off2 0 states merged. Computing post^41 Adding the following inequality (randomly selected among 2 inequalities): deadlineBasic < WCET_1 + 10*per1 + Off1 6 states merged. Computing post^42 0 states merged. Final constraint K : 2*per1 + Off1 > per2 + Off2 & WCET_2 + 3*per2 + Off2 > 5*per1 + Off1 & WCET_2 + Off2 > Off1 & 2*per2 + Off2 > 3*per1 + Off1 & per3 + Off3 > 3*per1 + Off1 & 5*per2 + Off2 > 8*per1 + Off1 & WCET_2 + 2*per2 + Off2 > per3 + Off3 & WCET_2 + 4*per2 + Off2 > 2*per3 + Off3 & 2*per2 + Off2 >= WCET_1 + 3*per1 + Off1 & per3 + Off3 >= WCET_1 + 3*per1 + Off1 & 5*per2 + Off2 >= WCET_1 + 8*per1 + Off1 & 7*per1 + Off1 >= WCET_2 + 4*per2 + Off2 & 2*per1 + Off1 >= WCET_2 + per2 + Off2 & WCET_3 + WCET_2 + WCET_1 + Off3 > per1 + Off1 & WCET_3 + WCET_2 + WCET_1 + Off2 > per1 + Off1 & 8*per1 + Off1 >= WCET_3 + WCET_2 + WCET_1 + 4*per2 + Off2 & WCET_3 + WCET_2 + WCET_1 > per1 & WCET_1 + Off1 > Off2 & WCET_1 + Off1 > Off3 & WCET_1 + 5*per1 + Off1 > 3*per2 + Off2 & WCET_3 + 3*per3 + Off3 > deadlineBasic & WCET_2 + 6*per2 + Off2 > deadlineBasic & WCET_1 + 10*per1 + Off1 > deadlineBasic Fixpoint reached after 42 iterations in 10.711 seconds: 208 reachable states with 228 transitions. Final constraint K0 : per1 >= 3*WCET_2 & 4*per1 >= 3*WCET_3 + 3*WCET_2 + 3*WCET_1 & per1 >= 3*WCET_1 & WCET_3 + WCET_2 + WCET_1 > per1 & Off1 >= 0 & WCET_1 + 10*per1 + Off1 > deadlineBasic & WCET_2 + 10*per1 + Off1 > deadlineBasic & deadlineBasic >= 10*per1 + Off1 & 5*per1 = 3*per2 & Off1 = Off2 & 10*per1 = 3*per3 & Off1 = Off3 HYMITATOR successfully terminated (after 18.619 seconds)