************************************************** * 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.011 second. Program checked and converted after 0.125 second. Computing post^1 0 states merged. Computing post^2 Adding the following inequality (randomly selected among 2 inequalities): Off3 < WCET2 + Off2 Adding the following inequality: D1 + Off1 < D2 + Off2 Adding the following inequality: D2 + Off2 <= D3 + Off3 Adding the following inequality (randomly selected among 2 inequalities): Off3 < WCET1 + Off1 Adding the following inequality (randomly selected among 4 inequalities): D2 + per3 < D3 Adding the following inequality (randomly selected among 2 inequalities): Off1 < WCET3 + Off3 0 states merged. Computing post^3 Adding the following inequality: Off2 < WCET1 + Off1 Adding the following inequality: Off1 < WCET2 + Off2 2 states merged. Computing post^4 0 states merged. Computing post^5 Adding the following inequality: WCET1 + WCET2 <= per1 0 states merged. Computing post^6 Adding the following inequality (randomly selected among 2 inequalities): WCET1 + WCET2 + WCET3 <= per2 Adding the following inequality: per1 + Off1 < WCET1 + WCET2 + WCET3 + Off2 Adding the following inequality: D1 + per1 + Off1 < D3 + Off3 Adding the following inequality: per1 < WCET1 + WCET2 + WCET3 Adding the following inequality: per1 + Off1 < WCET1 + WCET2 + WCET3 + Off3 1 states merged. Computing post^7 0 states merged. Computing post^8 Adding the following inequality: per2 + Off2 < 2*per1 + Off1 0 states merged. Computing post^9 Adding the following inequality: per2 + Off2 < per3 + Off3 Adding the following inequality: WCET2 + per2 + Off2 <= 2*per1 + Off1 Adding the following inequality: 2*per1 + Off1 <= WCET2 + per2 + Off2 Adding the following inequality: WCET2 + D1 < D2 0 states merged. Computing post^10 Adding the following inequality: 2*per1 + Off1 <= per3 + Off3 0 states merged. Computing post^11 Adding the following inequality (randomly selected among 2 inequalities): 2*per1 + Off1 < per3 + Off3 Adding the following inequality: WCET2 + per1 < per2 0 states merged. Computing post^12 Adding the following inequality: 2*WCET1 + WCET2 + WCET3 <= per2 Adding the following inequality: WCET1 + 2*per1 + Off1 <= per3 + Off3 1 states merged. Computing post^13 Adding the following inequality: 3*per1 + Off1 < per3 + Off3 Adding the following inequality: WCET1 + WCET2 + per1 <= per2 3 states merged. Computing post^14 Adding the following inequality (randomly selected among 2 inequalities): per3 + Off3 <= WCET1 + 3*per1 + Off1 0 states merged. Computing post^15 Adding the following inequality: 2*per1 + Off1 + per2 <= WCET2 + per3 + Off3 0 states merged. Computing post^16 3 states merged. Computing post^17 Adding the following inequality: D1 + per1 < WCET1 + D2 0 states merged. Computing post^18 0 states merged. Computing post^19 0 states merged. Computing post^20 Adding the following inequality (randomly selected among 2 inequalities): WCET1 + WCET2 <= WCET3 Adding the following inequality: per1 <= 2*WCET1 + WCET2 0 states merged. Computing post^21 3 states merged. Computing post^22 3 states merged. Computing post^23 Adding the following inequality: 2*WCET1 + WCET2 + D1 < D2 0 states merged. Computing post^24 6 states merged. Computing post^25 2 states merged. Computing post^26 Adding the following inequality: per3 <= 6*WCET1 + 4*WCET2 13 states merged. Computing post^27 Adding the following inequality: 6*WCET1 + 4*WCET2 <= per3 2 states merged. Computing post^28 0 states merged. Computing post^29 Adding the following inequality: WCET2 <= WCET1 Adding the following inequality: WCET1 <= WCET2 0 states merged. Computing post^30 0 states merged. Computing post^31 0 states merged. Computing post^32 0 states merged. Computing post^33 0 states merged. Computing post^34 2 states merged. Computing post^35 1 states merged. Computing post^36 0 states merged. Computing post^37 1 states merged. Computing post^38 1 states merged. Computing post^39 0 states merged. Computing post^40 0 states merged. Computing post^41 0 states merged. Computing post^42 0 states merged. Computing post^43 0 states merged. Computing post^44 0 states merged. Computing post^45 0 states merged. Computing post^46 0 states merged. Computing post^47 0 states merged. Final constraint K : D3 > 10*WCET1 + D2 & D2 > 3*WCET1 + D1 & WCET1 > 0 & WCET1 = WCET2 & 2*WCET1 = WCET3 & 3*WCET1 = per1 & 5*WCET1 = per2 & Off1 = Off2 & 10*WCET1 = per3 & Off1 = Off3 Fixpoint reached after 47 iterations in 9.085 seconds: 254 reachable states with 326 transitions. Final constraint K0 : deadlineBasic >= 34*WCET1 + Off1 & WCET1 > 0 & Off1 >= 0 & D2 > 3*WCET1 + D1 & D3 > 10*WCET1 + D2 & WCET1 = WCET2 & 2*WCET1 = WCET3 & 3*WCET1 = per1 & 5*WCET1 = per2 & Off1 = Off2 & 10*WCET1 = per3 & Off1 = Off3 HYMITATOR successfully terminated (after 11.765 seconds)