************************************************** * 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.07 second. Computing post^1 Adding the following inequality (randomly selected among 2 inequalities): Off1 < Off2 0 states merged. Computing post^2 Adding the following inequality: Off3 < WCET1 + Off1 Adding the following inequality (randomly selected among 2 inequalities): D1 + Off1 <= D2 + Off2 Adding the following inequality: Off3 < Off2 Adding the following inequality: D1 + Off1 <= D3 + Off3 Adding the following inequality (randomly selected among 3 inequalities): D1 + Off1 < D3 Adding the following inequality: Off1 < WCET3 + Off3 0 states merged. Computing post^3 Adding the following inequality: WCET1 + Off1 <= Off2 0 states merged. Computing post^4 Adding the following inequality: D2 + Off2 < D3 + Off3 Adding the following inequality: Off2 < per1 + Off1 Adding the following inequality: Off2 < WCET1 + WCET3 + Off1 Adding the following inequality: Off2 < WCET1 + WCET3 + Off3 0 states merged. Computing post^5 Adding the following inequality: per1 + Off1 < WCET2 + Off2 Adding the following inequality: D1 + per1 + Off1 < D2 + Off2 0 states merged. Computing post^6 0 states merged. Computing post^7 Adding the following inequality (randomly selected among 2 inequalities): D2 + Off2 <= D1 + 2*per1 + Off1 Adding the following inequality: WCET1 + WCET2 + Off2 <= 2*per1 + Off1 0 states merged. Computing post^8 Adding the following inequality (randomly selected among 3 inequalities): 2*per1 + Off1 < per2 + Off2 Adding the following inequality: 2*WCET1 + WCET2 + WCET3 <= 2*per1 0 states merged. Computing post^9 Adding the following inequality: 2*per1 + Off1 < per3 + Off3 1 states merged. Computing post^10 Adding the following inequality (randomly selected among 2 inequalities): per2 + Off2 < per3 + Off3 0 states merged. Computing post^11 Adding the following inequality: per2 + Off2 < 3*per1 + Off1 Adding the following inequality: 3*per1 + Off1 < per3 + Off3 1 states merged. Computing post^12 Adding the following inequality: D2 + per2 + Off2 <= D1 + 3*per1 + Off1 0 states merged. Computing post^13 Adding the following inequality: WCET2 + 3*per1 + Off1 <= per3 + Off3 1 states merged. Computing post^14 Adding the following inequality (randomly selected among 2 inequalities): per3 + Off3 < 2*per2 + Off2 0 states merged. Computing post^15 Adding the following inequality: per3 + Off3 < 4*per1 + Off1 Adding the following inequality: WCET1 + WCET2 + 3*per1 + Off1 <= 2*per2 + Off2 0 states merged. Computing post^16 Adding the following inequality: D2 + 2*per2 + Off2 < D3 + per3 + Off3 Adding the following inequality: 2*per2 + Off2 < 4*per1 + Off1 Adding the following inequality: 2*per2 + Off2 < WCET3 + per3 + Off3 0 states merged. Computing post^17 Adding the following inequality: 4*per1 + Off1 < WCET2 + 2*per2 + Off2 Adding the following inequality: D1 + 4*per1 + Off1 < D2 + 2*per2 + Off2 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 + per3 + Off3 <= 3*per2 + Off2 Adding the following inequality: D1 + 5*per1 + Off1 < D3 + per3 + Off3 Adding the following inequality: 5*per1 + Off1 < WCET1 + WCET2 + WCET3 + per3 + Off3 0 states merged. Computing post^21 0 states merged. Computing post^22 Adding the following inequality: D2 + 3*per2 + Off2 <= D3 + per3 + Off3 Adding the following inequality (randomly selected among 2 inequalities): D2 + 3*per2 + Off2 < D3 + per3 1 states merged. Computing post^23 Adding the following inequality (randomly selected among 2 inequalities): D2 + 3*per2 + Off2 <= D1 + 6*per1 + Off1 Adding the following inequality: WCET2 + 3*per2 + Off2 <= 6*per1 + Off1 2 states merged. Computing post^24 Adding the following inequality: D3 + per3 + Off3 <= D1 + 6*per1 + Off1 Adding the following inequality: D1 + 6*per1 + Off1 <= D3 + per3 + Off3 1 states merged. Computing post^25 Adding the following inequality: WCET1 + WCET2 + 6*per1 + Off1 <= 4*per2 + Off2 1 states merged. Computing post^26 Adding the following inequality: D3 + 4*per2 + Off2 < D1 + 6*per1 + Off1 + per3 Adding the following inequality: 2*WCET1 + 2*WCET2 + WCET3 + D1 + 7*per1 + Off1 <= D3 + 4*per2 + Off2 Adding the following inequality: 2*WCET1 + 2*WCET2 + WCET3 + D1 <= D3 Adding the following inequality: 3*WCET1 + 3*WCET2 + WCET3 + 4*per1 + Off1 <= 4*per2 + Off2 Adding the following inequality: 3*WCET1 + 3*WCET2 + WCET3 <= 3*per1 3 states merged. Computing post^27 Adding the following inequality: 4*per2 + Off2 < 7*per1 + Off1 3 states merged. Computing post^28 Adding the following inequality: D1 + 7*per1 + Off1 < D2 + 4*per2 + Off2 Adding the following inequality (randomly selected among 2 inequalities): D3 + per1 <= D1 + per3 0 states merged. Computing post^29 Adding the following inequality (randomly selected among 2 inequalities): D1 + per3 < WCET1 + D3 + per1 1 states merged. Computing post^30 Adding the following inequality: deadlineBasic < WCET1 + 7*per1 + Off1 1 states merged. Computing post^31 0 states merged. Final constraint K : D1 + 3*per1 + Off1 >= D2 + per2 + Off2 & 7*per1 + Off1 > 4*per2 + Off2 & D1 + per3 >= D3 + per1 & 4*per2 + Off2 >= 3*WCET1 + 3*WCET2 + WCET3 + 4*per1 + Off1 & D1 + 6*per1 + Off1 >= D2 + 3*per2 + Off2 & D3 + per3 > D2 + 3*per2 + Off2 & WCET2 + 2*per2 + Off2 > 4*per1 + Off1 & D2 + Off2 > D1 + per1 + Off1 & per1 + Off1 > Off2 & D2 + 4*per2 + Off2 > D1 + 7*per1 + Off1 & WCET2 + Off2 > per1 + Off1 & WCET1 + D3 + per1 > D1 + per3 & WCET1 + D3 + per3 > D1 + 6*per1 & WCET1 + 7*per1 + Off1 > deadlineBasic & 6*per1 + Off1 >= WCET2 + 3*per2 + Off2 & D1 + 3*per1 >= WCET2 + D3 & WCET1 + WCET3 + D1 + 6*per1 + Off1 > D3 + Off2 + per3 & WCET1 + WCET3 + Off1 > Off2 & 2*per2 + Off2 >= WCET1 + WCET2 + 3*per1 + Off1 & D3 + 3*per2 + Off2 >= WCET1 + WCET2 + WCET3 + D1 + 6*per1 + Off1 & 2*per1 >= 2*WCET1 + WCET2 + WCET3 & D3 + 4*per2 + Off2 >= 2*WCET1 + 2*WCET2 + WCET3 + D1 + 7*per1 + Off1 & D3 + 2*per2 + Off2 > D1 + 6*per1 + Off1 & WCET1 + WCET2 + WCET3 + D1 + per1 > D3 & D1 + 6*per1 + Off1 = D3 + per3 + Off3 Fixpoint reached after 31 iterations in 66.06 seconds: 76 reachable states with 91 transitions. Final constraint K0 : 2*D3 + 5*Off1 > 2*D1 + 5*Off2 & Off1 >= 0 & 5*D2 + 5*Off2 > 3*D1 + 2*D3 + 5*Off1 & 9*D1 + 5*D2 + 20*per2 + 5*Off2 > 14*D3 + 5*Off1 & 5*WCET1 + 14*D3 + 5*Off1 > 5*deadlineBasic + 14*D1 & 5*WCET1 + 5*WCET2 + D1 > D3 & 12*D3 > 7*D1 + 5*D2 + 15*per2 + 5*Off2 & D3 >= 5*WCET2 + D1 & 14*D3 + 5*Off1 > 14*D1 + 20*per2 + 5*Off2 & 6*D3 + 5*Off1 >= D1 + 5*D2 + 5*per2 + 5*Off2 & 8*D1 + 20*per2 + 5*Off2 >= 15*WCET1 + 15*WCET2 + 5*WCET3 + 8*D3 + 5*Off1 & 5*WCET2 + 8*D1 + 10*per2 + 5*Off2 > 8*D3 + 5*Off1 & 7*D1 + 15*per2 + 5*Off2 >= 5*WCET1 + 5*WCET2 + 5*WCET3 + 7*D3 + 5*Off1 & 4*D3 >= 10*WCET1 + 5*WCET2 + 5*WCET3 + 4*D1 & 5*WCET2 + 2*D1 + 5*Off2 > 2*D3 + 5*Off1 & 5*WCET1 + 5*WCET2 + 5*WCET3 + 3*D1 > 3*D3 & 5*deadlineBasic + 14*D1 >= 14*D3 + 5*Off1 & 2*D1 + 5*per1 = 2*D3 & 7*D1 + 5*per3 = 7*D3 & Off1 = Off3 HYMITATOR successfully terminated (after 318.959 seconds)