************************************************************ * 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/concurent_tasks_chain.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.008 second. Memory for abstract program: 584.75390625 KB (i.e., 149697. words) The model contains stopwatches. Computing post^1 from 1 state. Adding the following inequality: offset_1_1 < offset_2_1 Computing post^2 from 1 state. Computing post^3 from 2 states. Computing post^4 from 3 states. Adding the following inequality: offset_1_1 + wcet1_1 + wcet2_1 <= offset_2_2 Computing post^5 from 4 states. Computing post^6 from 5 states. Computing post^7 from 9 states. Computing post^8 from 10 states. Computing post^9 from 18 states. Computing post^10 from 19 states. Computing post^11 from 30 states. Computing post^12 from 27 states. Computing post^13 from 36 states. Computing post^14 from 30 states. Computing post^15 from 20 states. Fixpoint reached after 16 iterations: 215 reachable states with 264 transitions. Analysis has been fully deterministic. Final constraint K0 (17 inequalities): offset_2_1 > offset_1_1 & offset_2_2 >= offset_1_1 + wcet1_1 + wcet2_1 & wcet1_2 > 0 & wcet1_3 > 0 & wcet1_4 > 0 & wcet2_1 > 0 & wcet2_2 > 0 & wcet2_3 > 0 & wcet2_3 >= bcet2_3 & wcet2_2 >= bcet2_2 & wcet2_1 >= bcet2_1 & wcet1_4 >= bcet1_4 & wcet1_3 >= bcet1_3 & wcet1_2 >= bcet1_2 & wcet1_1 >= bcet1_1 & offset_1_1 + wcet1_1 > offset_2_1 & offset_1_1 >= 0 Inverse method successfully finished after 15.456 seconds. Generating graphical output... Writing to file the states description... IMITATOR successfully terminated (after 15.957 seconds)