************************************************************ * IMITATOR 2.5.0 * * * * Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT * * 2009 - 2012 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, Sorbonne Paris Cite, France * ************************************************************ Model: examples/Scheduling/generic_fp.imi Mode: inverse method. Merging technique of [AFS12] enabled. Graphical output will be generated. Log (description of states) will be generated. Parsing completed after 0.003 second. Memory for abstract program: 473.24609375 KB (i.e., 121151. words) The model contains stopwatches. Computing post^1 from 1 state. Computing post^2 from 3 states. Adding the following inequality (randomly selected among 2 inequalities): Off3 < 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 Computing post^3 from 6 states. Adding the following inequality: Off2 < WCET_1 + Off1 Adding the following inequality: Off1 < WCET_2 + Off2 Computing post^4 from 4 states. Computing post^5 from 4 states. Adding the following inequality: WCET_2 + WCET_1 <= per1 Computing post^6 from 4 states. Adding the following inequality (randomly selected among 2 inequalities): per1 + Off1 < per2 + Off2 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 Computing post^7 from 3 states. Adding the following inequality: WCET_1 + per1 + Off1 <= per2 + Off2 Computing post^8 from 3 states. 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 Computing post^9 from 3 states. Adding the following inequality: per2 + Off2 < 2*per1 + Off1 Adding the following inequality: per2 + Off2 < per3 + Off3 Computing post^10 from 3 states. Adding the following inequality: WCET_2 + per2 + Off2 <= 2*per1 + Off1 Adding the following inequality: WCET_2 + per2 + Off2 <= per3 + Off3 Computing post^11 from 3 states. Adding the following inequality: 2*per1 + Off1 < per3 + Off3 Computing post^12 from 3 states. Adding the following inequality: WCET_1 + 2*per1 + Off1 <= per3 + Off3 Computing post^13 from 3 states. Adding the following inequality: 3*per1 + Off1 < 2*per2 + Off2 Adding the following inequality: 3*per1 + Off1 < per3 + Off3 Computing post^14 from 3 states. Adding the following inequality: WCET_1 + 3*per1 + Off1 <= 2*per2 + Off2 Adding the following inequality: WCET_1 + 3*per1 + Off1 <= per3 + Off3 Computing post^15 from 3 states. Computing post^16 from 6 states. Adding the following inequality: per3 + Off3 < WCET_2 + 2*per2 + Off2 Computing post^17 from 6 states. Computing post^18 from 6 states. Computing post^19 from 6 states. Computing post^20 from 6 states. Adding the following inequality: WCET_3 + WCET_2 + WCET_1 + 2*per2 + Off2 <= 5*per1 + Off1 Computing post^21 from 6 states. Computing post^22 from 6 states. Adding the following inequality: 3*per2 + Off2 < WCET_1 + 5*per1 + Off1 Adding the following inequality: 5*per1 + Off1 < WCET_2 + 3*per2 + Off2 Computing post^23 from 6 states. Computing post^24 from 6 states. Computing post^25 from 6 states. Computing post^26 from 3 states. Computing post^27 from 3 states. Adding the following inequality (randomly selected among 2 inequalities): 2*per3 + Off3 < 7*per1 + Off1 Computing post^28 from 6 states. Adding the following inequality: 4*per2 + Off2 < 7*per1 + Off1 Adding the following inequality: 2*per3 + Off3 < WCET_2 + 4*per2 + Off2 Adding the following inequality: 4*per2 + Off2 < WCET_3 + 2*per3 + Off3 Computing post^29 from 6 states. Adding the following inequality: WCET_2 + 4*per2 + Off2 <= 7*per1 + Off1 Computing post^30 from 6 states. Computing post^31 from 6 states. Computing post^32 from 6 states. Adding the following inequality: WCET_3 + WCET_2 + WCET_1 + 4*per2 + Off2 <= 8*per1 + Off1 Computing post^33 from 6 states. Adding the following inequality: 8*per1 + Off1 < 5*per2 + Off2 Computing post^34 from 3 states. Adding the following inequality: WCET_1 + 8*per1 + Off1 <= 5*per2 + Off2 Computing post^35 from 3 states. Computing post^36 from 3 states. Computing post^37 from 3 states. Computing post^38 from 3 states. Computing post^39 from 3 states. Computing post^40 from 9 states. Adding the following inequality (randomly selected among 3 inequalities): deadlineBasic < WCET_3 + 3*per3 + Off3 Adding the following inequality (randomly selected among 3 inequalities): 3*per3 + Off3 < WCET_2 + 6*per2 + Off2 Computing post^41 from 18 states. Adding the following inequality (randomly selected among 2 inequalities): 3*per3 + Off3 < WCET_1 + 10*per1 + Off1 Adding the following inequality (randomly selected among 2 inequalities): deadlineBasic < WCET_2 + 6*per2 + Off2 Computing post^42 from 12 states. Adding the following inequality: deadlineBasic < WCET_1 + 10*per1 + Off1 Fixpoint reached after 43 iterations: 208 reachable states with 228 transitions. Analysis may have been non-deterministic: 9 random selections have been performed. Final constraint K0 (12 inequalities): 4*per1 >= 3*WCET_3 + 3*WCET_2 + 3*WCET_1 & per1 >= 3*WCET_1 & WCET_3 + WCET_2 + WCET_1 > per1 & per1 >= 3*WCET_2 & Off1 >= 0 & WCET_1 + 10*per1 + Off1 > deadlineBasic & WCET_2 + 10*per1 + Off1 > deadlineBasic & deadlineBasic >= 10*per1 + Off1 & 10*per1 = 3*per3 & Off1 = Off3 & 5*per1 = 3*per2 & Off1 = Off2 Inverse method successfully finished after 3.184 seconds. Generating graphical output... Writing to file the states description... IMITATOR successfully terminated (after 5.497 seconds)