hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/Sched2-50-2.imi ./test/Sched2-50-2.v0 -mode cover -EFIM -merge -output-cart -time-limit 4500 salloc: Granted job allocation 96667 ************************************************************ * IMITATOR 2.6.2 * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2014 * * LSV, ENS de Cachan & CNRS, France * * Universite Paris 13, Sorbonne Paris Cite, LIPN, France * * * * Build: 1311 (2014-11-17 19:19:49 UTC) * ************************************************************ Analysis time: Mon Nov 17, 2014 22:34:29 Model: ./test/Sched2-50-2.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Parsing completed after 0.014 second. Memory for abstract model: 383.660 KiB (i.e., 98217 words) ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 1 Considering the following pi1 b = 10 & C3_WORST = 20 K1 computed by IM after 210 iterations in 30.152 seconds: 245 states with 344 transitions explored. 34 > b + C3_WORST & 14 >= b & 22 > C3_WORST & b >= 0 & C3_WORST >= 0 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 2 Considering the following pi2 b = 14 & C3_WORST = 20 K2 computed by IM after 210 iterations in 28.023 seconds: 245 states with 344 transitions explored. 18 > b & 50 >= 2*b + C3_WORST & 22 > C3_WORST & b >= 0 & C3_WORST >= 0 Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 3 Considering the following pi3 b = 16 & C3_WORST = 20 K3 computed by IM after 210 iterations in 26.881 seconds: 256 states with 355 transitions explored. C3_WORST >= 20 & b >= 10 & 2*b + C3_WORST > 50 OR C3_WORST >= 20 & b >= 10 & 2*b + C3_WORST > 50 OR C3_WORST >= 20 & b >= 10 & 2*b + C3_WORST > 50 OR C3_WORST >= 20 & b >= 10 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 OR b >= 10 & C3_WORST >= 20 & 2*b + C3_WORST > 50 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 4 Considering the following pi4 b = 10 & C3_WORST = 22 K4 computed by IM after 209 iterations in 26.847 seconds: 239 states with 332 transitions explored. 18 > b & 34 > b + C3_WORST & 50 >= 2*b + C3_WORST & 26 > C3_WORST & b >= 0 & C3_WORST >= 0 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 5 Considering the following pi5 b = 12 & C3_WORST = 22 K5 computed by IM after 209 iterations in 27.212 seconds: 239 states with 332 transitions explored. 18 > b & 50 >= 2*b + C3_WORST & 26 > C3_WORST & b >= 0 & C3_WORST >= 0 Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 6 Considering the following pi6 b = 10 & C3_WORST = 26 K6 computed by IM after 209 iterations in 27.204 seconds: 239 states with 332 transitions explored. 18 > b & 40 > b + C3_WORST & 50 >= 2*b + C3_WORST & 32 > C3_WORST & b >= 0 & C3_WORST >= 0 Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 7 Considering the following pi7 b = 10 & C3_WORST = 30 K7 computed by IM after 209 iterations in 27.514 seconds: 240 states with 334 transitions explored. 18 > b & 50 >= 2*b + C3_WORST & 32 > C3_WORST & b >= 0 & C3_WORST >= 0 Constraint larger than another one previously computed: replace. ************************************************** END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM Size of V0: 3321 Unsuccessful points: 3314 3 different constraints were computed. Average number of states : 567 Average number of transitions : 791 Global time spent : 194.143426895 s Time spent on IM : 193.837211847 s Time spent to compute next point: 0.146271944046 s ************************************************** Generation of the graphical cartography... Plot cartography in 2D projected on parameters b and C3_WORST to file './test/Sched2-50-2_cart_bc.png'. IMITATOR successfully terminated (after 194.711 seconds) salloc: Relinquishing job allocation 96667 hoangia90@magi1:~/imitator$