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 96663 ************************************************************ * 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:28:17 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.010 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 26.546 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 26.752 seconds: 245 states with 344 transitions explored. 14 >= b & 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 = 15 & C3_WORST = 20 K3 computed by IM after 210 iterations in 27.377 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: 4 Considering the following pi4 b = 16 & C3_WORST = 20 K4 computed by IM after 210 iterations in 28.441 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: 5 Considering the following pi5 b = 10 & C3_WORST = 22 K5 computed by IM after 209 iterations in 31.305 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: 6 Considering the following pi6 b = 12 & C3_WORST = 22 K6 computed by IM after 209 iterations in 32.269 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: 7 Considering the following pi7 b = 10 & C3_WORST = 26 K7 computed by IM after 209 iterations in 29.876 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: 8 Considering the following pi8 b = 10 & C3_WORST = 30 K8 computed by IM after 209 iterations in 28.653 seconds: 240 states with 334 transitions explored. 46 > b + C3_WORST & 50 >= 2*b + C3_WORST & 18 > b & 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: 3313 3 different constraints were computed. Average number of states : 649 Average number of transitions : 905 Global time spent : 231.655328035 s Time spent on IM : 231.223066568 s Time spent to compute next point: 0.21831703186 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 232.146 seconds) salloc: Relinquishing job allocation 96663 salloc: Job allocation 96663 has been revoked. hoangia90@magi1:~/imitator$