hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/Sched2-100-2.imi ./test/Sched2-100-2.v0 -mode cover -EFIM -merge -output-cart -time-limit 4500 salloc: Granted job allocation 96669 ************************************************************ * 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:44:57 Model: ./test/Sched2-100-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.012 second. Memory for abstract model: 401.648 KiB (i.e., 102822 words) ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..1000 & C3_WORST = 20..1000 Number of points inside V0: 972171 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 1 Considering the following pi1 b = 10 & C3_WORST = 20 ^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B^[[B K1 computed by IM after 395 iterations in 141.763 seconds: 204 states with 280 transitions explored. C3_WORST >= 20 & 28 > C3_WORST & b = 10 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 2 Considering the following pi2 b = 11 & C3_WORST = 20 K2 computed by IM after 395 iterations in 159.063 seconds: 204 states with 280 transitions explored. b >= 10 & C3_WORST >= 20 & 18 > b & 22 > C3_WORST ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 3 Considering the following pi3 b = 18 & C3_WORST = 20 K3 computed by IM after 395 iterations in 168.089 seconds: 205 states with 282 transitions explored. b >= 10 & C3_WORST >= 20 & 28 > b & 22 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 4 Considering the following pi4 b = 28 & C3_WORST = 20 K4 computed by IM after 395 iterations in 186.920 seconds: 207 states with 287 transitions explored. b >= 10 & C3_WORST >= 20 & 30 > b & 22 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 5 Considering the following pi5 b = 30 & C3_WORST = 20 K5 computed by IM after 395 iterations in 179.558 seconds: 210 states with 294 transitions explored. b >= 10 & C3_WORST >= 20 & 100 >= 2*b + C3_WORST & 22 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 6 Considering the following pi6 b = 41 & C3_WORST = 20 K6 computed by IM after 395 iterations in 186.949 seconds: 229 states with 313 transitions explored. C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 7 Considering the following pi7 b = 11 & C3_WORST = 22 K7 computed by IM after 395 iterations in 184.562 seconds: 204 states with 280 transitions explored. b >= 10 & C3_WORST >= 20 & 18 > b & 28 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 8 Considering the following pi8 b = 18 & C3_WORST = 22 K8 computed by IM after 395 iterations in 174.972 seconds: 205 states with 282 transitions explored. b >= 10 & C3_WORST >= 20 & 28 > b & 28 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 9 Considering the following pi9 b = 28 & C3_WORST = 22 K9 computed by IM after 395 iterations in 180.545 seconds: 207 states with 287 transitions explored. 64 >= b + C3_WORST & b >= 10 & C3_WORST >= 20 & 30 > b & 40 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 10 Considering the following pi10 b = 30 & C3_WORST = 22 K10 computed by IM after 395 iterations in 175.961 seconds: 210 states with 294 transitions explored. b >= 10 & C3_WORST >= 20 & 100 >= 2*b + C3_WORST & 28 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 11 Considering the following pi11 b = 30 & C3_WORST = 28 K11 computed by IM after 395 iterations in 150.279 seconds: 210 states with 294 transitions explored. 100 >= 2*b + C3_WORST & b >= 10 & C3_WORST >= 20 & 64 >= b + C3_WORST & 34 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 12 Considering the following pi12 b = 35 & C3_WORST = 30 K12 computed by IM after 395 iterations in 149.353 seconds: 210 states with 294 transitions explored. b >= 10 & C3_WORST >= 20 & 100 >= 2*b + C3_WORST & 34 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 13 Considering the following pi13 b = 30 & C3_WORST = 34 K13 computed by IM after 395 iterations in 148.739 seconds: 210 states with 294 transitions explored. b >= 10 & C3_WORST >= 20 & 100 >= 2*b + C3_WORST & 64 >= b + C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 14 Considering the following pi14 b = 31 & C3_WORST = 34 K14 computed by IM after 395 iterations in 155.659 seconds: 210 states with 294 transitions explored. b >= 10 & C3_WORST >= 20 & 100 >= 2*b + C3_WORST & 40 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 15 Considering the following pi15 b = 25 & C3_WORST = 40 K15 computed by IM after 395 iterations in 153.294 seconds: 205 states with 282 transitions explored. 70 >= b + C3_WORST & b >= 10 & C3_WORST >= 20 & 28 > b & 46 > C3_WORST ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 16 Considering the following pi16 b = 28 & C3_WORST = 40 K16 computed by IM after 395 iterations in 154.140 seconds: 207 states with 287 transitions explored. 70 >= b + C3_WORST & b >= 10 & C3_WORST >= 20 & 30 > b & 46 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 17 Considering the following pi17 b = 30 & C3_WORST = 40 K17 computed by IM after 395 iterations in 157.052 seconds: 210 states with 294 transitions explored. 100 >= 2*b + C3_WORST & b >= 10 & C3_WORST >= 20 & 70 >= b + C3_WORST & 58 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 18 Considering the following pi18 b = 29 & C3_WORST = 42 K18 computed by IM after 395 iterations in 168.895 seconds: 207 states with 287 transitions explored. 72 > b + C3_WORST & 100 >= 2*b + C3_WORST & b >= 10 & C3_WORST >= 20 & 30 > b & 58 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 19 Considering the following pi19 b = 28 & C3_WORST = 44 K19 computed by IM after 395 iterations in 235.718 seconds: 225 states with 312 transitions explored. 100 >= 2*b + C3_WORST & b >= 10 & C3_WORST >= 20 & 30 > b & 46 > C3_WORST ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 20 Considering the following pi20 b = 26 & C3_WORST = 46 K20 computed by IM after 395 iterations in 230.895 seconds: 223 states with 307 transitions explored. 100 >= 2*b + C3_WORST & 74 > b + C3_WORST & b >= 10 & C3_WORST >= 20 & 28 > b & 52 > C3_WORST ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 21 Considering the following pi21 b = 26 & C3_WORST = 48 K21 computed by IM after 395 iterations in 229.317 seconds: 223 states with 307 transitions explored. 100 >= 2*b + C3_WORST & 76 >= b + C3_WORST & b >= 10 & C3_WORST >= 20 & 28 > b & 58 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 22 Considering the following pi22 b = 23 & C3_WORST = 54 K22 computed by IM after 395 iterations in 220.692 seconds: 223 states with 307 transitions explored. 100 >= 2*b + C3_WORST & b >= 10 & C3_WORST >= 20 & 28 > b & 58 > C3_WORST Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 23 Considering the following pi23 b = 10 & C3_WORST = 58 K23 computed by IM after 395 iterations in 173.601 seconds: 204 states with 280 transitions explored. C3_WORST >= 20 & 60 >= C3_WORST & b = 10 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 24 Considering the following pi24 b = 11 & C3_WORST = 58 K24 computed by IM after 395 iterations in 172.335 seconds: 204 states with 280 transitions explored. b >= 10 & C3_WORST >= 20 & 70 >= b + C3_WORST & 18 > b Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 25 Considering the following pi25 b = 13 & C3_WORST = 58 K25 computed by IM after 395 iterations in 150.356 seconds: 204 states with 280 transitions explored. b >= 10 & C3_WORST >= 20 & 72 > b + C3_WORST & 18 > b Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 26 Considering the following pi26 b = 14 & C3_WORST = 58 K26 computed by IM after 395 iterations in 175.532 seconds: 222 states with 305 transitions explored. b >= 10 & C3_WORST >= 20 & 74 > b + C3_WORST & 18 > b Constraint larger than another one previously computed: replace. ************************************************** END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM Size of V0: 972171 Unsuccessful points: 37638 7 different constraints were computed. Average number of states : 783 Average number of transitions : 1083 Global time spent : 4573.03121305 s Time spent on IM : 4564.25370002 s Time spent to compute next point: 6.97815275192 s ************************************************** Generation of the graphical cartography... Plot cartography in 2D projected on parameters b and C3_WORST to file './test/Sched2-100-2_cart_bc.png'. IMITATOR successfully terminated (after 4573.880 seconds) salloc: Relinquishing job allocation 96669 hoangia90@magi1:~/imitator$