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 96689 ************************************************************ * 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:07:10 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:07:10 ************************************************************ * 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:07:10 ************************************************************ * 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:07:10 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) * ************************************************************ Analysis time: Mon Nov 17, 2014 23:07:10 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) * ************************************************************ Analysis time: Mon Nov 17, 2014 23:07:10 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) * ************************************************************ Analysis time: Mon Nov 17, 2014 23:07:10 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:07:10 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. ************************************************************ * 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:07:10 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. ************************************************************ * 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) * ************************************************************ 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. Analysis time: Mon Nov 17, 2014 23:07:10 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. Analysis time: Mon Nov 17, 2014 23:07:10 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. 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. 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. 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. Analysis time: Mon Nov 17, 2014 23:07:10 Model: ./test/Sched2-50-0.imi Model: ./test/Sched2-50-0.imi Mode: behavioral cartography algorithm with full coverage and step 1. Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). Considering algorithm EFIM (work in progress). Considering a distributed mode with "shuffle" enumeration of pi0 points. Considering a distributed mode with "shuffle" enumeration of pi0 points. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: The program will try to stop after 4500 seconds. *** Warning: The program will try to stop after 4500 seconds. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 second. Parsing completed after 0.028 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: 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 ************************************************** 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: 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: 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: 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 ************************************************** 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 = 10..29 & C3_WORST = 60..79 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 60..79 b = 30..50 & C3_WORST = 40..59 Number of points inside V0: 420 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: Number of points inside V0: 420 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..29 & C3_WORST = 20..39 Number of points inside V0: 400 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: Number of points inside V0: 400 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..50 & C3_WORST = 90..100 Number of points inside V0: 231 b = 10..29 & C3_WORST = 40..59 Number of points inside V0: 400 b = 30..50 & C3_WORST = 80..89 Number of points inside V0: 210 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 10..29 & C3_WORST = 80..89 Number of points inside V0: 200 Parametric rectangle V0: b = 10..29 & C3_WORST = 90..100 Number of points inside V0: 220 ************************************************** 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: b = 10..50 & C3_WORST = 20..100 Number of points inside V0: 3321 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 30..39 & C3_WORST = 20..39 Number of points inside V0: 200 START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: b = 40..50 & C3_WORST = 20..39 Number of points inside V0: 220 K1 computed by IM after 33 iterations in 0.751 second: 132 states with 165 transitions explored. 22 > b & 50 > b + C3_WORST & 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.937 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.937 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.267 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: 109 3 different constraints were computed. Average number of states : 170 Average number of transitions : 219 Global time spent : 3.44183588028 s Time spent on IM : 2.95723628998 s Time spent to compute next point: 0. s ************************************************** [Master] Splitting time : 0.000831127166748 s [Master] Processing time : 0.00471615791321 s [Master] Waiting time : 3.42180609703 s [Master] Occupancy : 0.584471053593 % [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 3.812 seconds) salloc: Relinquishing job allocation 96689 hoangia90@magi1:~/imitator$