************************************************************ * 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/hppr10_audio.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: 312.23828125 KB (i.e., 79933. 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): audOff < 40 + ptpOff Adding the following inequality: audOff < ptpOff + C1 Adding the following inequality: ptpOff <= audOff Adding the following inequality: C2 > 0 Adding the following inequality: driftDelta < D2 Computing post^3 from 2 states. Adding the following inequality (randomly selected among 3 inequalities): ptpOff + C1 + C2 <= 40 + audOff Adding the following inequality (randomly selected among 2 inequalities): 2*audOff + 10 < 2*ptpOff + C1 + C2 Computing post^4 from 4 states. Adding the following inequality: audOff + D2 < ptpOff + driftDelta + C1 + C2 Adding the following inequality: audOff < 20 + ptpOff Adding the following inequality: ptpOff + C1 + 2*C2 <= 20 + audOff Computing post^5 from 5 states. Computing post^6 from 4 states. Adding the following inequality: driftDelta + C2 <= D2 Computing post^7 from 4 states. Computing post^8 from 3 states. Computing post^9 from 2 states. Computing post^10 from 3 states. Computing post^11 from 2 states. Fixpoint reached after 12 iterations: 31 reachable states with 40 transitions. Analysis may have been non-deterministic: 3 random selections have been performed. Final constraint K0 (8 inequalities): ptpOff >= 0 & 20 > C1 & C1 > 0 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & driftDelta + 10 = D2 & C1 + 2*C2 = 20 Inverse method successfully finished after 0.162 second. Generating graphical output... Writing to file the states description... IMITATOR successfully terminated (after 0.242 second)