************************************************** * 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.01 second. Program checked and converted after 0.078 second. Computing post^1 0 states merged. Computing post^2 Adding the following inequality (randomly selected among 2 inequalities): Off1 < 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): Off2 < WCET1 + Off1 Adding the following inequality (randomly selected among 4 inequalities): D2 + Off2 < D3 Adding the following inequality (randomly selected among 2 inequalities): Off1 < WCET3 + Off3 0 states merged. Computing post^3 Adding the following inequality: Off3 < WCET1 + Off1 2 states merged. Computing post^4 0 states merged. Computing post^5 Adding the following inequality (randomly selected among 2 inequalities): WCET1 + WCET2 <= per1 0 states merged. Computing post^6 Adding the following inequality (randomly selected among 3 inequalities): deadlineBasic < per2 + Off2 Adding the following inequality: WCET1 + WCET2 + WCET3 + Off2 <= per1 + Off1 1 states merged. Computing post^7 Adding the following inequality (randomly selected among 2 inequalities): deadlineBasic < per3 + Off3 0 states merged. Computing post^8 0 states merged. Computing post^9 Adding the following inequality: deadlineBasic < 2*per1 + Off1 0 states merged. Final constraint K : WCET1 + Off1 > Off3 & WCET1 + Off1 > Off2 & WCET2 + Off2 > Off1 & WCET3 + Off3 > Off1 & D3 + Off3 >= D2 + Off2 & D3 > D2 + Off2 & D2 + Off2 > D1 + Off1 & per1 >= WCET1 + WCET2 & per1 + Off1 >= WCET1 + WCET2 + WCET3 + Off2 & 2*per1 + Off1 > deadlineBasic & per2 + Off2 > deadlineBasic & per3 + Off3 > deadlineBasic Fixpoint reached after 9 iterations in 1.085 seconds: 31 reachable states with 33 transitions. Final constraint K0 : per1 >= WCET1 + WCET2 + WCET3 & Off1 >= 0 & 2*per1 + Off1 > deadlineBasic & Off1 + per2 > deadlineBasic & Off1 + per3 > deadlineBasic & WCET2 > 0 & D3 > D2 + Off1 & D2 > D1 & WCET1 > 0 & WCET3 > 0 & deadlineBasic >= per1 + Off1 & Off1 = Off2 & Off1 = Off3 HYMITATOR successfully terminated (after 1.494 seconds)