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 96668
************************************************************
* 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:40:42
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.019 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
K1 computed by IM after 395 iterations in 152.985 seconds: 204 states with 280 transitions explored.
b >= 10
& C3_WORST >= 20
& 18 > b
& 22 > C3_WORST
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 2
Considering the following pi2
b = 18
& C3_WORST = 20
K2 computed by IM after 395 iterations in 155.600 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: 3
Considering the following pi3
b = 28
& C3_WORST = 20
K3 computed by IM after 395 iterations in 153.177 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: 4
Considering the following pi4
b = 30
& C3_WORST = 20
K4 computed by IM after 395 iterations in 161.086 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: 5
Considering the following pi5
b = 41
& C3_WORST = 20
K5 computed by IM after 395 iterations in 162.683 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: 6
Considering the following pi6
b = 10
& C3_WORST = 22
K6 computed by IM after 395 iterations in 185.228 seconds: 204 states with 280 transitions explored.
C3_WORST >= 20
& 28 > C3_WORST
& b = 10
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 7
Considering the following pi7
b = 11
& C3_WORST = 22
K7 computed by IM after 395 iterations in 182.092 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 177.654 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 148.478 seconds: 207 states with 287 transitions explored.
b >= 10
& C3_WORST >= 20
& 30 > b
& 34 > 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 164.138 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 188.905 seconds: 210 states with 294 transitions explored.
100 >= 2*b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 64 >= b + C3_WORST
& 46 > 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 180.308 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: 13
Considering the following pi13
b = 25
& C3_WORST = 40
K13 computed by IM after 395 iterations in 150.130 seconds: 205 states with 282 transitions explored.
70 >= b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 28 > b
& 46 > C3_WORST
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 14
Considering the following pi14
b = 28
& C3_WORST = 40
K14 computed by IM after 395 iterations in 153.440 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: 15
Considering the following pi15
b = 30
& C3_WORST = 40
K15 computed by IM after 395 iterations in 153.797 seconds: 210 states with 294 transitions explored.
100 >= 2*b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 72 > b + C3_WORST
& 46 > C3_WORST
Constraint larger than another one previously computed: replace.
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 16
Considering the following pi16
b = 28
& C3_WORST = 44
K16 computed by IM after 395 iterations in 189.973 seconds: 225 states with 312 transitions explored.
100 >= 2*b + C3_WORST
& 74 > b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 30 > b
& 52 > C3_WORST
Constraint larger than another one previously computed: replace.
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 17
Considering the following pi17
b = 26
& C3_WORST = 48
K17 computed by IM after 395 iterations in 189.478 seconds: 223 states with 307 transitions explored.
100 >= 2*b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 28 > b
& 52 > C3_WORST
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 18
Considering the following pi18
b = 10
& C3_WORST = 52
K18 computed by IM after 395 iterations in 154.517 seconds: 204 states with 280 transitions explored.
b >= 10
& C3_WORST >= 20
& 64 >= b + C3_WORST
& 18 > b
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 19
Considering the following pi19
b = 13
& C3_WORST = 52
K19 computed by IM after 395 iterations in 155.445 seconds: 204 states with 280 transitions explored.
70 >= b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 18 > b
& 58 > C3_WORST
Constraint larger than another one previously computed: replace.
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 20
Considering the following pi20
b = 18
& C3_WORST = 52
K20 computed by IM after 395 iterations in 184.817 seconds: 205 states with 282 transitions explored.
70 >= b + C3_WORST
& b >= 10
& C3_WORST >= 20
& 28 > b
& 58 > C3_WORST
Constraint larger than another one previously computed: replace.
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 21
Considering the following pi21
b = 19
& C3_WORST = 52
K21 computed by IM after 395 iterations in 181.195 seconds: 205 states with 282 transitions explored.
72 > 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 = 20
& C3_WORST = 52
K22 computed by IM after 395 iterations in 230.006 seconds: 223 states with 307 transitions explored.
100 >= 2*b + C3_WORST
& 74 > 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 = 22
& C3_WORST = 52
K23 computed by IM after 395 iterations in 226.529 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: 24
Considering the following pi24
b = 10
& C3_WORST = 58
K24 computed by IM after 395 iterations in 170.478 seconds: 204 states with 280 transitions explored.
b >= 10
& C3_WORST >= 20
& 70 >= b + C3_WORST
& 18 > b
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 25
Considering the following pi25
b = 13
& C3_WORST = 58
K25 computed by IM after 395 iterations in 175.183 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 205.613 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 : 781
Average number of transitions : 1078
Global time spent : 4540.10253787 s
Time spent on IM : 4532.9481144 s
Time spent to compute next point: 5.32088398933 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 4541.110 seconds)
salloc: Relinquishing job allocation 96668
hoangia90@magi1:~/imitator$