hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/Sched2-100-0.imi ./test/Sched2-100-0.v0 -mode cover -merge -output-cart -time-limit 4500
salloc: Granted job allocation 96905
************************************************************
* 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: Tue Nov 18, 2014 01:11:41
Model: ./test/Sched2-100-0.imi
Mode: behavioral cartography algorithm with full coverage and step 1.
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.154 second.
Memory for abstract model: 400.410 KiB (i.e., 102505 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
K1 computed by IM after 32 iterations in 2.109 seconds: 121 states with 149 transitions explored.
C3_WORST >= 20
& b >= 10
& 72 > b + C3_WORST
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 2
Considering the following pi2
b = 52
& C3_WORST = 20
K2 computed by IM after 32 iterations in 1.705 seconds: 134 states with 168 transitions explored.
100 > b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 72 > b
& b + C3_WORST >= 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 3
Considering the following pi3
b = 72
& C3_WORST = 20
K3 computed by IM after 33 iterations in 2.361 seconds: 166 states with 222 transitions explored.
C3_WORST >= 20
& 28 > C3_WORST
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 4
Considering the following pi4
b = 73
& C3_WORST = 20
K4 computed by IM after 33 iterations in 4.216 seconds: 219 states with 293 transitions explored.
C3_WORST >= 20
& 172 > 2*b + C3_WORST
& b > 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 5
Considering the following pi5
b = 76
& C3_WORST = 20
K5 computed by IM after 33 iterations in 3.674 seconds: 259 states with 350 transitions explored.
76 >= b
& b > 72
& 2*b + C3_WORST = 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 6
Considering the following pi6
b = 77
& C3_WORST = 20
K6 computed by IM after 47 iterations in 9.397 seconds: 315 states with 431 transitions explored.
258 > 3*b + C3_WORST
& C3_WORST >= 20
& 100 > b + C3_WORST
& 2*b + C3_WORST > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 7
Considering the following pi7
b = 80
& C3_WORST = 20
K7 computed by IM after 47 iterations in 8.678 seconds: 338 states with 470 transitions explored.
80 >= b
& 4*b > 316
& b + C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 8
Considering the following pi8
b = 81
& C3_WORST = 20
K8 computed by IM after 47 iterations in 11.130 seconds: 367 states with 508 transitions explored.
81 >= b
& b > 72
& 4*b + C3_WORST = 344
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 9
Considering the following pi9
b = 82
& C3_WORST = 20
K9 computed by IM after 47 iterations in 14.422 seconds: 421 states with 578 transitions explored.
C3_WORST >= 20
& 272 > 3*b + C3_WORST
& 4*b + C3_WORST > 344
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 10
Considering the following pi10
b = 84
& C3_WORST = 20
K10 computed by IM after 47 iterations in 13.133 seconds: 426 states with 588 transitions explored.
84 >= b
& b > 72
& 3*b + C3_WORST = 272
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 11
Considering the following pi11
b = 85
& C3_WORST = 20
K11 computed by IM after 47 iterations in 15.750 seconds: 424 states with 585 transitions explored.
200 >= 2*b + C3_WORST
& C3_WORST >= 20
& 86 > b
& 3*b + C3_WORST > 272
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 12
Considering the following pi12
b = 86
& C3_WORST = 20
K12 computed by IM after 47 iterations in 20.375 seconds: 470 states with 650 transitions explored.
C3_WORST >= 20
& 28 >= C3_WORST
& b = 86
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 13
Considering the following pi13
b = 87
& C3_WORST = 20
K13 computed by IM after 47 iterations in 18.090 seconds: 494 states with 678 transitions explored.
C3_WORST >= 20
& 200 >= 2*b + C3_WORST
& 2*b > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 14
Considering the following pi14
b = 91
& C3_WORST = 20
K14 computed by IM after 47 iterations in 24.135 seconds: 501 states with 687 transitions explored.
100 > b
& 100 > C3_WORST
& C3_WORST >= 20
& 2*b > 172
& 2*b + C3_WORST > 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 15
Considering the following pi15
b = 100
& C3_WORST = 20
K15 computed by IM after 47 iterations in 25.449 seconds: 532 states with 764 transitions explored.
C3_WORST >= 20
& 100 > C3_WORST
& b = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 16
Considering the following pi16
b = 101
& C3_WORST = 20
K16 computed by IM after 47 iterations in 37.244 seconds: 593 states with 841 transitions explored.
100 > C3_WORST
& C3_WORST >= 20
& b > 100
& 1000 >= b
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 17
Considering the following pi17
b = 79
& C3_WORST = 21
K17 computed by IM after 47 iterations in 6.923 seconds: 334 states with 466 transitions explored.
b = 79
& C3_WORST = 21
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 18
Considering the following pi18
b = 80
& C3_WORST = 21
K18 computed by IM after 47 iterations in 14.551 seconds: 378 states with 520 transitions explored.
444 >= 5*b + 2*C3_WORST
& C3_WORST >= 20
& b + C3_WORST > 100
& 6*b + 2*C3_WORST > 516
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 19
Considering the following pi19
b = 78
& C3_WORST = 22
K19 computed by IM after 47 iterations in 7.183 seconds: 331 states with 459 transitions explored.
158 > 2*b
& b > 72
& b + C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 20
Considering the following pi20
b = 78
& C3_WORST = 23
K20 computed by IM after 47 iterations in 13.142 seconds: 371 states with 509 transitions explored.
258 > 3*b + C3_WORST
& b > 72
& b + C3_WORST > 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 21
Considering the following pi21
b = 80
& C3_WORST = 23
K21 computed by IM after 47 iterations in 10.689 seconds: 383 states with 527 transitions explored.
344 > 4*b + C3_WORST
& C3_WORST >= 20
& b > 72
& 5*b + 2*C3_WORST > 444
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 22
Considering the following pi22
b = 78
& C3_WORST = 24
K22 computed by IM after 47 iterations in 12.496 seconds: 374 states with 516 transitions explored.
b > 72
& 158 > 2*b
& 3*b + C3_WORST = 258
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 23
Considering the following pi23
b = 72
& C3_WORST = 28
K23 computed by IM after 33 iterations in 2.848 seconds: 186 states with 256 transitions explored.
b = 72
& C3_WORST = 28
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 24
Considering the following pi24
b = 71
& C3_WORST = 29
K24 computed by IM after 32 iterations in 2.287 seconds: 146 states with 188 transitions explored.
b >= 10
& 72 > b
& b + C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 25
Considering the following pi25
b = 72
& C3_WORST = 29
K25 computed by IM after 47 iterations in 4.910 seconds: 312 states with 425 transitions explored.
42 > C3_WORST
& C3_WORST > 28
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 26
Considering the following pi26
b = 86
& C3_WORST = 29
K26 computed by IM after 47 iterations in 29.563 seconds: 473 states with 654 transitions explored.
100 > C3_WORST
& C3_WORST > 28
& b = 86
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 27
Considering the following pi27
b = 71
& C3_WORST = 30
K27 computed by IM after 32 iterations in 3.829 seconds: 180 states with 234 transitions explored.
72 > b
& 2*b > 72
& 2*b + C3_WORST = 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 28
Considering the following pi28
b = 70
& C3_WORST = 31
K28 computed by IM after 32 iterations in 3.260 seconds: 167 states with 214 transitions explored.
b >= 10
& 172 > 2*b + C3_WORST
& 100 > C3_WORST
& b + C3_WORST > 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 29
Considering the following pi29
b = 71
& C3_WORST = 31
K29 computed by IM after 32 iterations in 3.843 seconds: 184 states with 238 transitions explored.
200 >= 2*b + C3_WORST
& 72 > b
& 100 > C3_WORST
& 2*b + C3_WORST > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 30
Considering the following pi30
b = 85
& C3_WORST = 31
K30 computed by IM after 47 iterations in 19.544 seconds: 431 states with 594 transitions explored.
86 > b
& 100 > C3_WORST
& b > 72
& 2*b + C3_WORST > 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 31
Considering the following pi31
b = 72
& C3_WORST = 42
K31 computed by IM after 47 iterations in 7.083 seconds: 315 states with 432 transitions explored.
b = 72
& C3_WORST = 42
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 32
Considering the following pi32
b = 72
& C3_WORST = 43
K32 computed by IM after 47 iterations in 6.076 seconds: 316 states with 433 transitions explored.
56 > C3_WORST
& 2*C3_WORST > 84
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 33
Considering the following pi33
b = 72
& C3_WORST = 56
K33 computed by IM after 47 iterations in 7.444 seconds: 355 states with 493 transitions explored.
b = 72
& C3_WORST = 56
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 34
Considering the following pi34
b = 72
& C3_WORST = 57
K34 computed by IM after 47 iterations in 7.637 seconds: 360 states with 498 transitions explored.
100 > C3_WORST
& C3_WORST > 56
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 35
Considering the following pi35
b = 71
& C3_WORST = 59
K35 computed by IM after 32 iterations in 3.289 seconds: 186 states with 240 transitions explored.
72 > b
& 100 > C3_WORST
& 2*b + C3_WORST > 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 36
Considering the following pi36
b = 10
& C3_WORST = 100
K36 computed by IM after 32 iterations in 3.338 seconds: 175 states with 225 transitions explored.
b >= 10
& 172 > 2*b + C3_WORST
& C3_WORST >= 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 37
Considering the following pi37
b = 36
& C3_WORST = 100
K37 computed by IM after 32 iterations in 3.088 seconds: 189 states with 246 transitions explored.
b >= 10
& 36 >= b
& 2*b + C3_WORST = 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 38
Considering the following pi38
b = 37
& C3_WORST = 100
K38 computed by IM after 32 iterations in 3.858 seconds: 193 states with 250 transitions explored.
200 >= 2*b + C3_WORST
& b >= 10
& 172 > b + C3_WORST
& C3_WORST >= 100
& 2*b + C3_WORST > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 39
Considering the following pi39
b = 51
& C3_WORST = 100
K39 computed by IM after 32 iterations in 3.812 seconds: 195 states with 252 transitions explored.
172 > b + C3_WORST
& C3_WORST >= 100
& 2*b + C3_WORST > 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 40
Considering the following pi40
b = 72
& C3_WORST = 100
K40 computed by IM after 47 iterations in 8.132 seconds: 383 states with 530 transitions explored.
b = 72
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 41
Considering the following pi41
b = 73
& C3_WORST = 100
K41 computed by IM after 47 iterations in 24.547 seconds: 450 states with 621 transitions explored.
86 > b
& b > 72
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 42
Considering the following pi42
b = 86
& C3_WORST = 100
K42 computed by IM after 47 iterations in 21.079 seconds: 497 states with 688 transitions explored.
b = 86
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 43
Considering the following pi43
b = 87
& C3_WORST = 100
K43 computed by IM after 47 iterations in 22.865 seconds: 517 states with 710 transitions explored.
100 > b
& 2*b > 172
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 44
Considering the following pi44
b = 100
& C3_WORST = 100
K44 computed by IM after 47 iterations in 26.351 seconds: 562 states with 808 transitions explored.
b = 100
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 45
Considering the following pi45
b = 101
& C3_WORST = 100
K45 computed by IM after 47 iterations in 38.963 seconds: 623 states with 886 transitions explored.
1000 >= b
& b > 100
& C3_WORST = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 46
Considering the following pi46
b = 71
& C3_WORST = 101
K46 computed by IM after 32 iterations in 4.114 seconds: 201 states with 260 transitions explored.
200 > b + C3_WORST
& b >= 10
& 72 > b
& b + C3_WORST >= 172
& 2*b + C3_WORST > 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 47
Considering the following pi47
b = 72
& C3_WORST = 101
K47 computed by IM after 47 iterations in 8.957 seconds: 385 states with 532 transitions explored.
128 > C3_WORST
& C3_WORST > 100
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 48
Considering the following pi48
b = 73
& C3_WORST = 101
K48 computed by IM after 47 iterations in 22.001 seconds: 452 states with 623 transitions explored.
272 > 2*b + C3_WORST
& C3_WORST > 100
& b > 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 49
Considering the following pi49
b = 86
& C3_WORST = 101
K49 computed by IM after 47 iterations in 22.933 seconds: 500 states with 691 transitions explored.
114 > C3_WORST
& C3_WORST > 100
& b = 86
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 50
Considering the following pi50
b = 87
& C3_WORST = 101
K50 computed by IM after 47 iterations in 28.072 seconds: 520 states with 713 transitions explored.
200 > b + C3_WORST
& C3_WORST > 100
& 2*b > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 51
Considering the following pi51
b = 99
& C3_WORST = 101
K51 computed by IM after 47 iterations in 28.662 seconds: 523 states with 716 transitions explored.
100 > b
& b + C3_WORST >= 200
& 1000 >= C3_WORST
& 2*b > 172
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 52
Considering the following pi52
b = 100
& C3_WORST = 101
K52 computed by IM after 47 iterations in 27.342 seconds: 562 states with 805 transitions explored.
C3_WORST > 100
& 1000 >= C3_WORST
& b = 100
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 53
Considering the following pi53
b = 101
& C3_WORST = 101
K53 computed by IM after 47 iterations in 41.117 seconds: 627 states with 889 transitions explored.
C3_WORST > 100
& b > 100
& 1000 >= C3_WORST
& 1000 >= b
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 54
Considering the following pi54
b = 85
& C3_WORST = 102
K54 computed by IM after 47 iterations in 23.922 seconds: 453 states with 624 transitions explored.
86 > b
& b > 72
& 2*b + C3_WORST = 272
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 55
Considering the following pi55
b = 85
& C3_WORST = 103
K55 computed by IM after 47 iterations in 20.145 seconds: 454 states with 625 transitions explored.
200 > b + C3_WORST
& 86 > b
& 2*b + C3_WORST > 272
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 56
Considering the following pi56
b = 86
& C3_WORST = 114
K56 computed by IM after 47 iterations in 24.192 seconds: 503 states with 693 transitions explored.
C3_WORST >= 114
& 1000 >= C3_WORST
& b = 86
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 57
Considering the following pi57
b = 85
& C3_WORST = 115
K57 computed by IM after 47 iterations in 18.118 seconds: 461 states with 634 transitions explored.
86 > b
& b > 72
& 1000 >= C3_WORST
& b + C3_WORST >= 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 58
Considering the following pi58
b = 72
& C3_WORST = 128
K58 computed by IM after 47 iterations in 8.152 seconds: 388 states with 536 transitions explored.
b = 72
& C3_WORST = 128
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 59
Considering the following pi59
b = 71
& C3_WORST = 129
K59 computed by IM after 32 iterations in 3.285 seconds: 203 states with 262 transitions explored.
b >= 10
& 72 > b
& 1000 >= C3_WORST
& b + C3_WORST >= 200
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 60
Considering the following pi60
b = 72
& C3_WORST = 129
K60 computed by IM after 47 iterations in 6.739 seconds: 390 states with 537 transitions explored.
C3_WORST > 128
& 1000 >= C3_WORST
& b = 72
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 61
Considering the following pi61
b = 28
& C3_WORST = 144
K61 computed by IM after 32 iterations in 3.364 seconds: 199 states with 258 transitions explored.
b >= 10
& 200 >= 2*b + C3_WORST
& b + C3_WORST >= 172
^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A^[[A
**************************************************
END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM
Size of V0: 972171
Unsuccessful points: 972110
61 different constraints were computed.
Average number of states : 363
Average number of transitions : 499
Global time spent : 1885.06331396 s
Time spent on IM : 825.646217346 s
Time spent to compute next point: 1056.02211499 s
**************************************************
Generation of the graphical cartography...
Plot cartography in 2D projected on parameters b and C3_WORST to file './test/Sched2-100-0_cart_bc.png'.
IMITATOR successfully terminated (after 1889.663 seconds)
salloc: Relinquishing job allocation 96905
salloc: Job allocation 96905 has been revoked.
hoangia90@magi1:~/imitator$ squeue