hoangia90@magi1:~/imitator$ salloc -n 12 mpirun ./bin/imitator ./test/A1.imi ./test/A1.v0 -mode cover -EFIM -distributed subpart -merge -output-cart with -depth-limit 10 -time-limit 4500 salloc: Granted job allocation 96883 *** Warning: The argument 'with' will be ignored. *** Warning: The argument 'with' will be ignored. ************************************************************ * 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) * ************************************************************ *** Warning: The argument 'with' will be ignored. ************************************************************ * 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) * ************************************************************ *** Warning: The argument 'with' will be ignored. ************************************************************ * 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) * ************************************************************ *** Warning: The argument 'with' will be ignored. *** Warning: The argument 'with' will be ignored. ************************************************************ * 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) * ************************************************************ *** Warning: The argument 'with' will be ignored. ************************************************************ * 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:37:09 Model: ./test/A1.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: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.imi Mode: behavioral cartography algorithm with full coverage and step 1. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.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: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.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: Considering a limit of 10 for the depth of the Post operation. *** 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) * ************************************************************ 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 argument 'with' will be ignored. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.imi Analysis time: Mon Nov 17, 2014 23:37:09 *** Warning: The argument 'with' will be ignored. ************************************************************ * 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) * ************************************************************ Mode: behavioral cartography algorithm with full coverage and step 1. Considering algorithm EFIM (work in progress). *** Warning: The argument 'with' will be ignored. Model: ./test/A1.imi Mode: behavioral cartography algorithm with full coverage and step 1. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.imi Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.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) * ************************************************************ Considering algorithm EFIM (work in progress). 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. 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: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. 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: Considering a limit of 10 for the depth of the Post operation. *** 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) * ************************************************************ 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: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.imi Analysis time: Mon Nov 17, 2014 23:37:09 Model: ./test/A1.imi *** Warning: Considering a limit of 10 for the depth of the Post operation. *** 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. Mode: behavioral cartography algorithm with full coverage and step 1. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. 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: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. *** Warning: Considering a limit of 10 for the depth of the Post operation. *** Warning: The argument 'with' will be ignored. *** Warning: The program will try to stop after 4500 seconds. *** Warning: The argument 'with' will be ignored. ************************************************************ * 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:37:09 ************************************************************ * 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) * ************************************************************ Model: ./test/A1.imi Analysis time: Mon Nov 17, 2014 23:37:09 Mode: behavioral cartography algorithm with full coverage and step 1. Model: ./test/A1.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. Considering algorithm EFIM (work in progress). Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. Considering a distributed mode with "shuffle" enumeration of pi0 points. *** Warning: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. *** Warning: Considering a limit of 10 for the depth of the Post operation. *** Warning: The program will try to stop after 4500 seconds. Parsing completed after 0.009 second. Parsing completed after 0.009 second. Parsing completed after 0.009 second. Parsing completed after 0.009 second. Parsing completed after 0.010 second. Parsing completed after 0.010 second. Parsing completed after 0.010 second. Parsing completed after 0.009 second. Parsing completed after 0.010 second. Parsing completed after 0.010 second. Parsing completed after 0.010 second. Parsing completed after 0.010 second. *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.921 KiB (i.e., 34796 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.921 KiB (i.e., 34796 words) *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. a = 0..10 & b = 0..10 Number of points inside V0: 121 Number of points inside V0: 121 *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. ************************************************** *** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.921 KiB (i.e., 34796 words) *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.921 KiB (i.e., 34796 words) START THE BEHAVIORAL CARTOGRAPHY ALGORITHM *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.910 KiB (i.e., 34793 words) ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..4 & b = 8..10 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 8..10 & b = 0..4 a = 5..7 & b = 0..4 Number of points inside V0: 15 Number of points inside V0: 15 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..4 & b = 0..1 Number of points inside V0: 10 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..4 & b = 2..4 Number of points inside V0: 15 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: Number of points inside V0: 15 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 5..7 & b = 8..10 Number of points inside V0: 9 a = 5..7 & b = 5..7 Number of points inside V0: 9 a = 8..10 & b = 8..10 Number of points inside V0: 9 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 8..10 & b = 5..7 Number of points inside V0: 9 K1 computed by IM after 2 iterations in 0.003 second: 1 state with 0 transition explored. K1 computed by IM after 2 iterations in 0.003 second: 1 state with 0 transition explored. *** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model. Memory for abstract model: 135.921 KiB (i.e., 34796 words) ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..1 & b = 5..7 Number of points inside V0: 6 K1 computed by IM after 2 iterations in 0.004 second: 2 states with 1 transition explored. b >= 2 K1 computed by IM after 2 iterations in 0.004 second: 2 states with 1 transition explored. b >= 2 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..10 & b = 0..10 Number of points inside V0: 121 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 2..4 & b = 5..7 Number of points inside V0: 9 a > b & 2 > b & b >= 0 a > b & 2 > b & b >= 0 K2 computed by IM after 2 iterations in 0.003 second: 1 state with 0 transition explored. a > b & b >= 0 & 2 > b K3 computed by IM after 2 iterations in 0.003 second: 1 state with 0 transition explored. a > b & b >= 0 & 2 > b Constraint included in another one previously computed: dropped. K2 computed by IM after 2 iterations in 0.004 second: 2 states with 1 transition explored. b >= 2 K2 computed by IM after 2 iterations in 0.004 second: 2 states with 1 transition explored. b >= 2 ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 8..10 & b = 0 Number of points inside V0: 3 K3 computed by IM after 2 iterations in 0.003 second: 1 state with 0 transition explored. a > b & b >= 0 & 2 > b Constraint included in another one previously computed: dropped. *** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore. *** Warning: This execution of IM has stopped prematurely. K3 computed by IM after 11 iterations in 0.022 second: 11 states with 10 transitions explored. This constraint is discarded due to premature termination. ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: a = 0..4 & b = 0 Number of points inside V0: 5 *** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore. *** Warning: This execution of IM has stopped prematurely. *** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore. *** Warning: This execution of IM has stopped prematurely. K1 computed by IM after 11 iterations in 0.019 second: 11 states with 10 transitions explored. This constraint is discarded due to premature termination. *** Warning: This execution of IM has stopped prematurely. K4 computed by IM after 11 iterations in 0.019 second: 20 states with 19 transitions explored. This constraint is valid despite premature termination. 5*b >= 1 & b >= a OR 9*b >= 2 & b >= a OR 4*b >= 1 & b >= a OR 7*b >= 2 & b >= a OR 3*b >= 1 & b >= a OR 5*b >= 2 & b >= a OR 2*b >= 1 & b >= a OR 3*b >= 2 & b >= a OR b >= 1 & b >= a *** Warning: This execution of IM has stopped prematurely. [Master] All workers done ************************************************** END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM [Worker 7] Number of unsuccessful points: 4 [Worker 7] Waiting time : 0.0070538520813 s [Worker 7] Time spent on IM : 0.0424761772156 s [Worker 7] Time to find next pi0 : 5.3882598877e-05 s Size of V0: 121 Unsuccessful points: 57 3 different constraints were computed. Average number of states : 8 Average number of transitions : 6 [Worker 7] Total time : 0.0529761314392 s [Worker 7] Occupancy : 86.6848486485 % Global time spent : 0.0508708953857 s Time spent on IM : 0.0312430858612 s Time spent to compute next point: 0. s ************************************************** [Master] Splitting time : 0.0010712146759 s [Master] Processing time : 0.00209736824036 s [Master] Waiting time : 0.0445346832275 s [Master] Occupancy : 12.5898472597 % [Master] wasted Tiles 1 end!!!!!! ************************************************** Generation of the graphical cartography... Plot cartography in 2D projected on parameters a and b to file './test/A1_cart_patator.png'. IMITATOR successfully terminated (after 0.344 second) IMITATOR successfully terminated (after 0.344 second) salloc: Relinquishing job allocation 96883 hoangia90@magi1:~/imitator$