************************************************************ * 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/am02.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.004 second. *** Warning: 'deadline', which is assigned a valuation in pi0, is not a valid parameter name. Memory for abstract program: 355.015625 KB (i.e., 90884. words) The model contains stopwatches. Computing post^1 from 1 state. Computing post^2 from 3 states. Computing post^3 from 5 states. Computing post^4 from 6 states. Computing post^5 from 7 states. Computing post^6 from 11 states. Adding the following inequality: 10 <= wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 Computing post^7 from 14 states. Computing post^8 from 12 states. Adding the following inequality: 10 <= wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 Computing post^9 from 6 states. Computing post^10 from 3 states. Fixpoint reached after 11 iterations: 53 reachable states with 70 transitions. Analysis has been fully deterministic. Final constraint K0 (5 inequalities): wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & 10 > wcet_m2_job2 + wcet_m2_job1 & 10 > wcet_m2_job2 + wcet_m1_job1 Inverse method successfully finished after 0.091 second. Generating graphical output... Writing to file the states description... IMITATOR successfully terminated (after 0.184 second)