hoangia90@magi1:~/imitator$ salloc -n 12 mpirun ./bin/imitator ./test/Sched2-50-0.imi ./test/Sched2-50-0.v0 -mode cover -EFIM -distributed subpart -merge -output-cart -time-limit 4500 salloc: Granted job allocation 96681 ************************************************************ * 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) * ************************************************************ ************************************************************ * 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 23:02:44 ************************************************************ * 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 23:02:44 Model: ./test/Sched2-50-0.imi ************************************************************ * 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) * ************************************************************ ************************************************************ * 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 23:02:44 ************************************************************ * 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 23:02:44 ************************************************************ * 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 23:02:44 Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. ************************************************************ * 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 23:02:44 Model: ./test/Sched2-50-0.imi Model: ./test/Sched2-50-0.imi ************************************************************ * 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) * ************************************************************ ************************************************************ * 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 23:02:44 Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. ************************************************************ * 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 23:02:44 Analysis time: Mon Nov 17, 2014 23:02:44 Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Analysis time: Mon Nov 17, 2014 23:02:44 Model: ./test/Sched2-50-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. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. ************************************************************ * 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 23:02:44 Model: ./test/Sched2-50-0.imi Analysis time: Mon Nov 17, 2014 23:02:44 Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. 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.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Parsing completed after 0.027 second. Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) Memory for abstract model: 384.929 KiB (i.e., 98542 words) ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 Number of points inside V0: 3321 Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 Number of points inside V0: 3321 b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 40..59 Number of points inside V0: 420 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 60..79 b = 10..29 & C3_WORST = 60..79 Number of points inside V0: 400 Number of points inside V0: 420 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..39 & C3_WORST = 20..39 Number of points inside V0: 200 b = 10..29 & C3_WORST = 90..100 Number of points inside V0: 220 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 40..50 & C3_WORST = 20..39 Parametric rectangle V0: Number of points inside V0: 220 b = 10..29 & C3_WORST = 40..59 Number of points inside V0: 400 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..29 & C3_WORST = 80..89 Number of points inside V0: 200 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 80..89 Number of points inside V0: 210 b = 10..29 & C3_WORST = 20..39 Number of points inside V0: 400 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 90..100 Number of points inside V0: 231 K1 computed by IM after 33 iterations in 0.751 second: 132 states with 165 transitions explored. 50 > b + C3_WORST & 22 > b & b >= 0 & C3_WORST >= 0 K1 computed by IM after 33 iterations in 0.751 second: 132 states with 165 transitions explored. b >= 0 & C3_WORST >= 0 & 22 > b & 50 > b + C3_WORST K2 computed by IM after 33 iterations in 0.948 second: 159 states with 204 transitions explored. C3_WORST >= 20 & b >= 10 & b + C3_WORST >= 50 OR C3_WORST >= 20 & b + C3_WORST >= 50 & b >= 10 K2 computed by IM after 33 iterations in 0.948 second: 159 states with 204 transitions explored. b + C3_WORST >= 50 & b >= 10 & C3_WORST >= 20 OR b + C3_WORST >= 50 & b >= 10 & C3_WORST >= 20 K3 computed by IM after 33 iterations in 1.364 seconds: 219 states with 290 transitions explored. b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 20 OR b > 22 & C3_WORST >= 0 OR b > 22 & C3_WORST >= 0 [Master] All workers done ************************************************** END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM Size of V0: 3321 Unsuccessful points: 138 3 different constraints were computed. Average number of states : 170 Average number of transitions : 219 Global time spent : 4.72958707809 s Time spent on IM : 3.06454730034 s Time spent to compute next point: 0. s ************************************************** [Master] Splitting time : 0.000925779342651 s [Master] Processing time : 0.0121276378632 s [Master] Waiting time : 4.69577336311 s [Master] Occupancy : 0.71705716208 % [Master] wasted Tiles 0 end!!!!!! ************************************************** Generation of the graphical cartography... Plot cartography in 2D projected on parameters b and C3_WORST to file './test/Sched2-50-0_cart_patator.png'. IMITATOR successfully terminated (after 5.098 seconds) salloc: Relinquishing job allocation 96681 hoangia90@magi1:~/imitator$