hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/spsmall.imi ./test/spsmall.v0 -mode cover -EFIM -merge -output-cart -time-limit 4500 salloc: Granted job allocation 96645 ************************************************************ * 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 21:56:31 Model: ./test/spsmall.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.015 second. *** Warning: The synclab 'up_wen' is not used in (at least) the automaton 'env' where it is declared: it will thus be removed from the whole model. *** Warning: 'd_up_q_0', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_net27', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_d_inta', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_d_inta', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_wela', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_wela', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_net45a', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_net45a', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_net13a', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_net13a', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_net45', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_net45', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_d_int', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_d_int', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_en_latchd', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_en_latchd', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_en_latchwen', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_en_latchwen', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_wen_h', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_wen_h', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_up_d_h', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'd_dn_d_h', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'tHI', which is assigned a valuation in v0, is not a valid parameter name. *** Warning: 'tLO', which is assigned a valuation in v0, is not a valid parameter name. Memory for abstract model: 965.578 KiB (i.e., 247188 words) ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: tsetupd = 65..110 & tsetupwen = 0..66 Number of points inside V0: 3082 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 1 Considering the following pi1 tsetupd = 65 & tsetupwen = 0 K1 computed by IM after 34 iterations in 0.468 second: 36 states with 35 transitions explored. 4 >= tsetupwen & 66 >= tsetupd & tsetupd >= 65 & tsetupwen >= 0 OR 66 >= tsetupd & 4 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 0 OR 4 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 0 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 2 Considering the following pi2 tsetupd = 67 & tsetupwen = 0 K2 computed by IM after 34 iterations in 0.573 second: 44 states with 43 transitions explored. 4 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 & tsetupwen >= 0 OR tsetupwen >= 0 & 4 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 0 & 4 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 4 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 0 & 67 >= tsetupd OR 4 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 0 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 3 Considering the following pi3 tsetupd = 70 & tsetupwen = 0 K3 computed by IM after 31 iterations in 0.472 second: 32 states with 31 transitions explored. tsetupwen >= 0 & 4 >= tsetupwen & 78 >= tsetupd & tsetupd >= 69 OR 4 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 0 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 4 Considering the following pi4 tsetupd = 79 & tsetupwen = 0 K4 computed by IM after 31 iterations in 0.500 second: 32 states with 31 transitions explored. tsetupwen >= 0 & 4 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 4 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 0 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 5 Considering the following pi5 tsetupd = 83 & tsetupwen = 0 K5 computed by IM after 31 iterations in 0.472 second: 32 states with 31 transitions explored. tsetupwen >= 0 & 4 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 82 OR 4 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 0 & tsetupwen + 87 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 6 Considering the following pi6 tsetupd = 88 & tsetupwen = 0 K6 computed by IM after 31 iterations in 0.438 second: 32 states with 31 transitions explored. 91 >= tsetupd & tsetupwen >= 0 & tsetupd >= 87 + tsetupwen OR tsetupd >= 87 + tsetupwen & tsetupwen >= 0 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 7 Considering the following pi7 tsetupd = 92 & tsetupwen = 0 K7 computed by IM after 31 iterations in 0.510 second: 32 states with 31 transitions explored. tsetupwen >= 0 & 4 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 4 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 0 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 8 Considering the following pi8 tsetupd = 96 & tsetupwen = 0 K8 computed by IM after 31 iterations in 0.445 second: 32 states with 31 transitions explored. 97 >= tsetupd & tsetupwen >= 0 & tsetupd >= 95 + tsetupwen OR tsetupd >= 95 + tsetupwen & tsetupwen >= 0 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 9 Considering the following pi9 tsetupd = 98 & tsetupwen = 0 K9 computed by IM after 32 iterations in 0.507 second: 33 states with 32 transitions explored. tsetupd >= 95 + tsetupwen & tsetupwen >= 0 & 99 >= tsetupd & tsetupd >= 97 OR tsetupd >= 97 & tsetupd >= 95 + tsetupwen & tsetupwen >= 0 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 10 Considering the following pi10 tsetupd = 100 & tsetupwen = 0 K10 computed by IM after 33 iterations in 0.593 second: 36 states with 37 transitions explored. tsetupd >= 99 & tsetupwen >= 0 & 4 >= tsetupwen & tsetupwen + 102 >= tsetupd & 103 >= tsetupd OR 4 >= tsetupwen & tsetupwen + 102 >= tsetupd & tsetupd >= 99 & tsetupwen >= 0 & 103 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 11 Considering the following pi11 tsetupd = 103 & tsetupwen = 0 K11 computed by IM after 33 iterations in 0.597 second: 46 states with 45 transitions explored. 103 >= tsetupd & tsetupwen >= 0 & tsetupd >= 102 + tsetupwen OR tsetupd >= 102 + tsetupwen & tsetupwen >= 0 & 106 >= tsetupd & tsetupd >= 103 OR tsetupd >= 102 + tsetupwen & tsetupwen >= 0 & 103 >= tsetupd OR tsetupd >= 103 & tsetupd >= 102 + tsetupwen & tsetupwen >= 0 & 106 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 12 Considering the following pi12 tsetupd = 107 & tsetupwen = 0 K12 computed by IM after 33 iterations in 0.569 second: 34 states with 33 transitions explored. tsetupwen >= 0 & 4 >= tsetupwen & 110 >= tsetupd & tsetupd >= 106 OR 4 >= tsetupwen & tsetupd >= 106 & tsetupwen >= 0 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 13 Considering the following pi13 tsetupd = 96 & tsetupwen = 2 K13 computed by IM after 31 iterations in 0.521 second: 32 states with 31 transitions explored. 4 >= tsetupwen & tsetupwen + 95 >= tsetupd & 97 >= tsetupd & tsetupd >= 95 OR 4 >= tsetupwen & tsetupwen + 95 >= tsetupd & tsetupd >= 95 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 14 Considering the following pi14 tsetupd = 104 & tsetupwen = 3 K14 computed by IM after 33 iterations in 0.601 second: 34 states with 33 transitions explored. 4 >= tsetupwen & tsetupwen + 102 >= tsetupd & tsetupd >= 103 OR tsetupd >= 103 & tsetupwen + 102 >= tsetupd & 4 >= tsetupwen ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 15 Considering the following pi15 tsetupd = 98 & tsetupwen = 4 K15 computed by IM after 32 iterations in 0.696 second: 40 states with 40 transitions explored. 8 >= tsetupwen & tsetupwen + 95 >= tsetupd & 99 >= tsetupd & tsetupd >= 97 OR 8 >= tsetupwen & tsetupwen + 95 >= tsetupd & tsetupd >= 97 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 16 Considering the following pi16 tsetupd = 65 & tsetupwen = 5 K16 computed by IM after 34 iterations in 0.604 second: 36 states with 35 transitions explored. 8 >= tsetupwen & 66 >= tsetupd & tsetupd >= 65 & tsetupwen >= 4 OR 66 >= tsetupd & 8 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 4 OR 8 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 4 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 17 Considering the following pi17 tsetupd = 67 & tsetupwen = 5 K17 computed by IM after 34 iterations in 0.630 second: 44 states with 43 transitions explored. 8 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 & tsetupwen >= 4 OR tsetupwen >= 4 & 8 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 4 & 8 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 8 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 4 & 67 >= tsetupd OR 8 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 4 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 18 Considering the following pi18 tsetupd = 70 & tsetupwen = 5 K18 computed by IM after 31 iterations in 0.551 second: 32 states with 31 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 78 >= tsetupd & tsetupd >= 69 OR 8 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 4 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 19 Considering the following pi19 tsetupd = 79 & tsetupwen = 5 K19 computed by IM after 31 iterations in 0.601 second: 32 states with 31 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 8 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 4 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 20 Considering the following pi20 tsetupd = 83 & tsetupwen = 5 K20 computed by IM after 31 iterations in 0.525 second: 32 states with 31 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 8 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 4 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 21 Considering the following pi21 tsetupd = 92 & tsetupwen = 5 K21 computed by IM after 31 iterations in 0.605 second: 33 states with 33 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 8 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 4 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 22 Considering the following pi22 tsetupd = 96 & tsetupwen = 5 K22 computed by IM after 31 iterations in 0.569 second: 32 states with 31 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 8 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 4 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 23 Considering the following pi23 tsetupd = 100 & tsetupwen = 5 K23 computed by IM after 33 iterations in 0.639 second: 37 states with 39 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 103 >= tsetupd & tsetupd >= 99 OR 8 >= tsetupwen & tsetupd >= 99 & tsetupwen >= 4 & 103 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 24 Considering the following pi24 tsetupd = 104 & tsetupwen = 5 K24 computed by IM after 33 iterations in 0.553 second: 34 states with 33 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 106 >= tsetupd & tsetupd >= 103 OR 8 >= tsetupwen & tsetupd >= 103 & tsetupwen >= 4 & 106 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 25 Considering the following pi25 tsetupd = 107 & tsetupwen = 5 K25 computed by IM after 33 iterations in 0.586 second: 35 states with 35 transitions explored. tsetupwen >= 4 & 8 >= tsetupwen & 110 >= tsetupd & tsetupd >= 106 OR 8 >= tsetupwen & tsetupd >= 106 & tsetupwen >= 4 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 26 Considering the following pi26 tsetupd = 65 & tsetupwen = 9 K26 computed by IM after 34 iterations in 0.659 second: 36 states with 35 transitions explored. 30 >= tsetupwen & 66 >= tsetupd & tsetupd >= 65 & tsetupwen >= 8 OR 66 >= tsetupd & 30 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 8 OR 30 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 8 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 27 Considering the following pi27 tsetupd = 67 & tsetupwen = 9 K27 computed by IM after 34 iterations in 0.696 second: 44 states with 43 transitions explored. 30 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 & tsetupwen >= 8 OR tsetupwen >= 8 & 30 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 8 & 30 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 30 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 8 & 67 >= tsetupd OR 30 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 8 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 28 Considering the following pi28 tsetupd = 70 & tsetupwen = 9 K28 computed by IM after 31 iterations in 0.573 second: 32 states with 31 transitions explored. tsetupwen >= 8 & 30 >= tsetupwen & 78 >= tsetupd & tsetupd >= 69 OR 30 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 8 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 29 Considering the following pi29 tsetupd = 79 & tsetupwen = 9 K29 computed by IM after 31 iterations in 0.604 second: 32 states with 31 transitions explored. tsetupwen >= 8 & 30 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 30 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 8 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 30 Considering the following pi30 tsetupd = 83 & tsetupwen = 9 K30 computed by IM after 31 iterations in 0.585 second: 32 states with 31 transitions explored. tsetupwen >= 8 & 30 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 30 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 8 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 31 Considering the following pi31 tsetupd = 92 & tsetupwen = 9 K31 computed by IM after 31 iterations in 0.573 second: 32 states with 31 transitions explored. tsetupwen >= 8 & 30 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 30 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 8 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 32 Considering the following pi32 tsetupd = 96 & tsetupwen = 9 K32 computed by IM after 31 iterations in 0.679 second: 33 states with 33 transitions explored. tsetupwen >= 8 & 30 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 30 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 8 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 33 Considering the following pi33 tsetupd = 98 & tsetupwen = 9 K33 computed by IM after 32 iterations in 0.622 second: 33 states with 32 transitions explored. tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 99 >= tsetupd & tsetupd >= 97 OR tsetupd >= 97 & tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 34 Considering the following pi34 tsetupd = 100 & tsetupwen = 9 K34 computed by IM after 33 iterations in 0.726 second: 36 states with 37 transitions explored. tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 103 >= tsetupd & tsetupd >= 99 OR tsetupd >= 99 & tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 103 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 35 Considering the following pi35 tsetupd = 104 & tsetupwen = 9 K35 computed by IM after 33 iterations in 0.611 second: 35 states with 35 transitions explored. tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 106 >= tsetupd & tsetupd >= 103 OR tsetupd >= 103 & tsetupd >= 87 + tsetupwen & tsetupwen >= 8 & 106 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 36 Considering the following pi36 tsetupd = 107 & tsetupwen = 9 K36 computed by IM after 33 iterations in 0.648 second: 34 states with 33 transitions explored. tsetupd >= 95 + tsetupwen & tsetupwen >= 8 & 110 >= tsetupd & tsetupd >= 106 OR tsetupd >= 106 & tsetupd >= 95 + tsetupwen & tsetupwen >= 8 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 37 Considering the following pi37 tsetupd = 98 & tsetupwen = 12 K37 computed by IM after 32 iterations in 0.640 second: 33 states with 32 transitions explored. 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 99 >= tsetupd & tsetupd >= 97 OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 97 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 38 Considering the following pi38 tsetupd = 107 & tsetupwen = 13 K38 computed by IM after 33 iterations in 0.685 second: 34 states with 33 transitions explored. tsetupd >= 87 + tsetupwen & tsetupwen + 95 >= tsetupd & 110 >= tsetupd & tsetupd >= 106 OR tsetupwen + 95 >= tsetupd & tsetupd >= 106 & tsetupd >= 87 + tsetupwen & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 39 Considering the following pi39 tsetupd = 100 & tsetupwen = 14 K39 computed by IM after 33 iterations in 0.773 second: 36 states with 37 transitions explored. 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 103 >= tsetupd & tsetupd >= 99 OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 99 & 103 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 40 Considering the following pi40 tsetupd = 104 & tsetupwen = 18 K40 computed by IM after 33 iterations in 0.747 second: 34 states with 33 transitions explored. 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 106 >= tsetupd & tsetupd >= 103 OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 103 & 106 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 41 Considering the following pi41 tsetupd = 107 & tsetupwen = 21 K41 computed by IM after 33 iterations in 0.734 second: 34 states with 33 transitions explored. 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 110 >= tsetupd & tsetupd >= 106 OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 106 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 42 Considering the following pi42 tsetupd = 65 & tsetupwen = 31 K42 computed by IM after 34 iterations in 0.711 second: 35 states with 34 transitions explored. 66 >= tsetupd & 34 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 30 OR 34 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 30 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 43 Considering the following pi43 tsetupd = 67 & tsetupwen = 31 K43 computed by IM after 34 iterations in 0.708 second: 37 states with 37 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 30 & 34 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 34 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 30 & 69 >= tsetupd OR 34 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 30 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 44 Considering the following pi44 tsetupd = 70 & tsetupwen = 31 K44 computed by IM after 32 iterations in 0.685 second: 33 states with 32 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 34 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 30 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 45 Considering the following pi45 tsetupd = 76 & tsetupwen = 31 K45 computed by IM after 32 iterations in 0.689 second: 33 states with 32 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 34 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 30 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 46 Considering the following pi46 tsetupd = 79 & tsetupwen = 31 K46 computed by IM after 32 iterations in 0.695 second: 33 states with 32 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 34 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 30 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 47 Considering the following pi47 tsetupd = 83 & tsetupwen = 31 K47 computed by IM after 32 iterations in 0.699 second: 33 states with 32 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 34 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 30 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 48 Considering the following pi48 tsetupd = 92 & tsetupwen = 31 K48 computed by IM after 32 iterations in 0.774 second: 35 states with 36 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 34 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 30 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 49 Considering the following pi49 tsetupd = 96 & tsetupwen = 31 K49 computed by IM after 32 iterations in 0.735 second: 33 states with 32 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 34 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 30 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 50 Considering the following pi50 tsetupd = 98 & tsetupwen = 31 K50 computed by IM after 33 iterations in 0.664 second: 34 states with 33 transitions explored. tsetupwen >= 30 & 34 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 34 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 30 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 51 Considering the following pi51 tsetupd = 100 & tsetupwen = 31 K51 computed by IM after 36 iterations in 0.781 second: 36 states with 36 transitions explored. 103 > tsetupd & 34 > tsetupwen & tsetupwen > 30 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 52 Considering the following pi52 tsetupd = 103 & tsetupwen = 31 K52 computed by IM after 36 iterations in 0.839 second: 44 states with 43 transitions explored. 106 > tsetupd & 34 > tsetupwen & tsetupwen > 30 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 53 Considering the following pi53 tsetupd = 106 & tsetupwen = 31 K53 computed by IM after 36 iterations in 0.782 second: 36 states with 36 transitions explored. tsetupwen + 76 > tsetupd & 34 > tsetupwen & tsetupwen > 30 & tsetupd > 103 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 54 Considering the following pi54 tsetupd = 107 & tsetupwen = 31 K54 computed by IM after 36 iterations in 0.728 second: 37 states with 38 transitions explored. 34 > tsetupwen & tsetupwen > 30 & tsetupd > 106 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 55 Considering the following pi55 tsetupd = 100 & tsetupwen = 34 K55 computed by IM after 36 iterations in 0.822 second: 39 states with 42 transitions explored. 103 > tsetupd & 37 > tsetupwen & tsetupwen > 30 & tsetupd > 99 Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 56 Considering the following pi56 tsetupd = 103 & tsetupwen = 34 K56 computed by IM after 36 iterations in 1.168 seconds: 47 states with 49 transitions explored. 106 > tsetupd & 37 > tsetupwen & tsetupwen > 30 & tsetupd > 100 Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 57 Considering the following pi57 tsetupd = 106 & tsetupwen = 34 K57 computed by IM after 36 iterations in 0.989 second: 39 states with 42 transitions explored. 37 > tsetupwen & tsetupwen + 76 > tsetupd & tsetupwen > 30 & tsetupd > 103 & 110 >= tsetupd Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 58 Considering the following pi58 tsetupd = 110 & tsetupwen = 34 K58 computed by IM after 36 iterations in 0.884 second: 40 states with 44 transitions explored. 37 > tsetupwen & tsetupwen > 30 & tsetupd > 106 & 110 >= tsetupd Constraint larger than another one previously computed: replace. ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 59 Considering the following pi59 tsetupd = 65 & tsetupwen = 35 K59 computed by IM after 34 iterations in 0.729 second: 35 states with 34 transitions explored. 66 >= tsetupd & 37 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 34 OR 37 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 34 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 60 Considering the following pi60 tsetupd = 67 & tsetupwen = 35 K60 computed by IM after 34 iterations in 0.708 second: 37 states with 37 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 34 & 37 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 37 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 34 & 69 >= tsetupd OR 37 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 34 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 61 Considering the following pi61 tsetupd = 70 & tsetupwen = 35 K61 computed by IM after 32 iterations in 0.633 second: 33 states with 32 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 37 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 34 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 62 Considering the following pi62 tsetupd = 76 & tsetupwen = 35 K62 computed by IM after 32 iterations in 0.690 second: 33 states with 32 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 37 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 34 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 63 Considering the following pi63 tsetupd = 79 & tsetupwen = 35 K63 computed by IM after 32 iterations in 0.662 second: 33 states with 32 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 37 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 34 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 64 Considering the following pi64 tsetupd = 83 & tsetupwen = 35 K64 computed by IM after 32 iterations in 0.646 second: 33 states with 32 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 37 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 34 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 65 Considering the following pi65 tsetupd = 92 & tsetupwen = 35 K65 computed by IM after 32 iterations in 0.648 second: 33 states with 32 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 37 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 34 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 66 Considering the following pi66 tsetupd = 96 & tsetupwen = 35 K66 computed by IM after 32 iterations in 0.703 second: 35 states with 36 transitions explored. tsetupwen >= 34 & 37 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 37 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 34 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 67 Considering the following pi67 tsetupd = 98 & tsetupwen = 35 K67 computed by IM after 33 iterations in 0.741 second: 34 states with 33 transitions explored. tsetupd >= 97 & tsetupd >= 61 + tsetupwen & tsetupwen >= 34 & 37 >= tsetupwen & 99 >= tsetupd OR 99 >= tsetupd & 37 >= tsetupwen & tsetupd >= 97 & tsetupd >= 61 + tsetupwen & tsetupwen >= 34 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 68 Considering the following pi68 tsetupd = 100 & tsetupwen = 37 K68 computed by IM after 36 iterations in 0.909 second: 37 states with 38 transitions explored. 103 > tsetupd & tsetupwen > 34 & tsetupd > 61 + tsetupwen & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 69 Considering the following pi69 tsetupd = 103 & tsetupwen = 37 K69 computed by IM after 36 iterations in 0.921 second: 45 states with 45 transitions explored. 42 > tsetupwen & 106 > tsetupd & tsetupwen > 34 & tsetupd > 61 + tsetupwen & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 70 Considering the following pi70 tsetupd = 106 & tsetupwen = 37 K70 computed by IM after 36 iterations in 0.859 second: 37 states with 38 transitions explored. 42 > tsetupwen & tsetupwen > 34 & tsetupd > 103 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 71 Considering the following pi71 tsetupd = 65 & tsetupwen = 38 K71 computed by IM after 34 iterations in 0.796 second: 35 states with 34 transitions explored. 66 >= tsetupd & 42 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 37 OR 42 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 37 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 72 Considering the following pi72 tsetupd = 67 & tsetupwen = 38 K72 computed by IM after 34 iterations in 0.740 second: 37 states with 37 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 37 & 42 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 42 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 37 & 69 >= tsetupd OR 42 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 37 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 73 Considering the following pi73 tsetupd = 70 & tsetupwen = 38 K73 computed by IM after 32 iterations in 0.717 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 42 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 37 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 74 Considering the following pi74 tsetupd = 76 & tsetupwen = 38 K74 computed by IM after 32 iterations in 0.667 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 42 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 37 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 75 Considering the following pi75 tsetupd = 79 & tsetupwen = 38 K75 computed by IM after 32 iterations in 0.789 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 42 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 37 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 76 Considering the following pi76 tsetupd = 83 & tsetupwen = 38 K76 computed by IM after 32 iterations in 0.659 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 42 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 37 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 77 Considering the following pi77 tsetupd = 92 & tsetupwen = 38 K77 computed by IM after 32 iterations in 0.695 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 42 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 37 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 78 Considering the following pi78 tsetupd = 96 & tsetupwen = 38 K78 computed by IM after 32 iterations in 0.661 second: 33 states with 32 transitions explored. tsetupwen >= 37 & 42 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 42 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 37 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 79 Considering the following pi79 tsetupd = 98 & tsetupwen = 38 K79 computed by IM after 33 iterations in 0.760 second: 34 states with 33 transitions explored. tsetupd >= 97 & tsetupwen >= 37 & 42 >= tsetupwen & tsetupwen + 61 >= tsetupd & 99 >= tsetupd OR 42 >= tsetupwen & tsetupwen + 61 >= tsetupd & tsetupd >= 97 & tsetupwen >= 37 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 80 Considering the following pi80 tsetupd = 100 & tsetupwen = 39 K80 computed by IM after 36 iterations in 0.840 second: 38 states with 40 transitions explored. 103 > tsetupd & 42 > tsetupwen & tsetupwen > 37 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 81 Considering the following pi81 tsetupd = 100 & tsetupwen = 42 K81 computed by IM after 36 iterations in 1.279 seconds: 36 states with 37 transitions explored. 103 > tsetupd & tsetupwen + 61 > tsetupd & 45 > tsetupwen & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 82 Considering the following pi82 tsetupd = 103 & tsetupwen = 42 K82 computed by IM after 36 iterations in 1.486 seconds: 46 states with 48 transitions explored. 106 > tsetupd & 45 > tsetupwen & tsetupwen > 37 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 83 Considering the following pi83 tsetupd = 106 & tsetupwen = 42 K83 computed by IM after 36 iterations in 1.281 seconds: 36 states with 37 transitions explored. tsetupwen > 37 & 45 > tsetupwen & tsetupd > 61 + tsetupwen & tsetupd > 103 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 84 Considering the following pi84 tsetupd = 65 & tsetupwen = 43 K84 computed by IM after 33 iterations in 0.809 second: 34 states with 33 transitions explored. 66 >= tsetupd & 45 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 42 OR 45 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 42 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 85 Considering the following pi85 tsetupd = 67 & tsetupwen = 43 K85 computed by IM after 33 iterations in 0.805 second: 36 states with 36 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 42 & 45 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 45 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 42 & 69 >= tsetupd OR 45 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 42 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 86 Considering the following pi86 tsetupd = 70 & tsetupwen = 43 K86 computed by IM after 31 iterations in 0.754 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 45 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 42 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 87 Considering the following pi87 tsetupd = 76 & tsetupwen = 43 K87 computed by IM after 31 iterations in 0.849 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 45 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 42 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 88 Considering the following pi88 tsetupd = 79 & tsetupwen = 43 K88 computed by IM after 31 iterations in 0.791 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 45 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 42 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 89 Considering the following pi89 tsetupd = 83 & tsetupwen = 43 K89 computed by IM after 31 iterations in 0.679 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 45 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 42 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 90 Considering the following pi90 tsetupd = 92 & tsetupwen = 43 K90 computed by IM after 31 iterations in 0.672 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 45 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 42 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 91 Considering the following pi91 tsetupd = 96 & tsetupwen = 43 K91 computed by IM after 31 iterations in 0.696 second: 32 states with 31 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 45 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 42 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 92 Considering the following pi92 tsetupd = 98 & tsetupwen = 43 K92 computed by IM after 32 iterations in 0.842 second: 33 states with 32 transitions explored. tsetupwen >= 42 & 45 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 45 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 42 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 93 Considering the following pi93 tsetupd = 100 & tsetupwen = 45 K93 computed by IM after 35 iterations in 0.806 second: 36 states with 37 transitions explored. 103 > tsetupd & 46 > tsetupwen & tsetupwen > 42 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 94 Considering the following pi94 tsetupd = 103 & tsetupwen = 45 K94 computed by IM after 35 iterations in 0.889 second: 44 states with 44 transitions explored. tsetupwen + 61 > tsetupd & 106 > tsetupd & 46 > tsetupwen & tsetupwen > 42 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 95 Considering the following pi95 tsetupd = 106 & tsetupwen = 45 K95 computed by IM after 35 iterations in 0.877 second: 38 states with 41 transitions explored. 46 > tsetupwen & tsetupwen > 42 & tsetupd > 103 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 96 Considering the following pi96 tsetupd = 65 & tsetupwen = 46 K96 computed by IM after 33 iterations in 0.824 second: 36 states with 37 transitions explored. 66 >= tsetupd & 54 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 45 OR 54 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 45 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 97 Considering the following pi97 tsetupd = 67 & tsetupwen = 46 K97 computed by IM after 33 iterations in 0.920 second: 38 states with 40 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 45 & 54 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 54 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 45 & 69 >= tsetupd OR 54 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 45 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 98 Considering the following pi98 tsetupd = 70 & tsetupwen = 46 K98 computed by IM after 31 iterations in 0.878 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 54 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 45 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 99 Considering the following pi99 tsetupd = 76 & tsetupwen = 46 K99 computed by IM after 31 iterations in 0.840 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 54 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 45 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 100 Considering the following pi100 tsetupd = 79 & tsetupwen = 46 K100 computed by IM after 31 iterations in 0.844 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 54 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 45 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 101 Considering the following pi101 tsetupd = 83 & tsetupwen = 46 K101 computed by IM after 31 iterations in 0.863 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 54 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 45 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 102 Considering the following pi102 tsetupd = 92 & tsetupwen = 46 K102 computed by IM after 31 iterations in 0.828 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 54 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 45 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 103 Considering the following pi103 tsetupd = 96 & tsetupwen = 46 K103 computed by IM after 31 iterations in 0.829 second: 34 states with 35 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 54 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 45 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 104 Considering the following pi104 tsetupd = 98 & tsetupwen = 46 K104 computed by IM after 32 iterations in 0.824 second: 35 states with 36 transitions explored. tsetupwen >= 45 & 54 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 54 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 45 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 105 Considering the following pi105 tsetupd = 100 & tsetupwen = 46 K105 computed by IM after 35 iterations in 0.903 second: 37 states with 39 transitions explored. 103 > tsetupd & 54 > tsetupwen & tsetupwen > 45 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 106 Considering the following pi106 tsetupd = 103 & tsetupwen = 46 K106 computed by IM after 35 iterations in 0.936 second: 45 states with 46 transitions explored. 106 > tsetupd & 54 > tsetupwen & tsetupwen > 45 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 107 Considering the following pi107 tsetupd = 106 & tsetupwen = 46 K107 computed by IM after 35 iterations in 0.915 second: 37 states with 39 transitions explored. 54 > tsetupwen & tsetupwen + 61 > tsetupd & tsetupwen > 45 & tsetupd > 103 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 108 Considering the following pi108 tsetupd = 107 & tsetupwen = 46 K108 computed by IM after 35 iterations in 0.947 second: 38 states with 41 transitions explored. 54 > tsetupwen & tsetupwen > 45 & tsetupd > 106 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 109 Considering the following pi109 tsetupd = 100 & tsetupwen = 54 K109 computed by IM after 35 iterations in 0.952 second: 37 states with 39 transitions explored. 103 > tsetupd & 60 > tsetupwen & tsetupwen > 46 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 110 Considering the following pi110 tsetupd = 103 & tsetupwen = 54 K110 computed by IM after 35 iterations in 1.079 seconds: 45 states with 46 transitions explored. 106 > tsetupd & 60 > tsetupwen & tsetupwen > 46 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 111 Considering the following pi111 tsetupd = 106 & tsetupwen = 54 K111 computed by IM after 35 iterations in 1.019 seconds: 37 states with 39 transitions explored. 107 > tsetupd & 60 > tsetupwen & tsetupwen > 46 & tsetupd > 103 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 112 Considering the following pi112 tsetupd = 107 & tsetupwen = 54 K112 computed by IM after 35 iterations in 0.949 second: 36 states with 37 transitions explored. 60 > tsetupwen & tsetupwen + 61 > tsetupd & tsetupwen > 46 & tsetupd > 106 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 113 Considering the following pi113 tsetupd = 65 & tsetupwen = 55 K113 computed by IM after 33 iterations in 0.832 second: 34 states with 33 transitions explored. 66 >= tsetupd & 60 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 54 OR 60 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 54 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 114 Considering the following pi114 tsetupd = 67 & tsetupwen = 55 K114 computed by IM after 33 iterations in 0.923 second: 36 states with 36 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 54 & 60 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 60 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 54 & 69 >= tsetupd OR 60 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 54 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 115 Considering the following pi115 tsetupd = 70 & tsetupwen = 55 K115 computed by IM after 31 iterations in 0.767 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 60 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 54 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 116 Considering the following pi116 tsetupd = 76 & tsetupwen = 55 K116 computed by IM after 31 iterations in 0.788 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 60 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 54 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 117 Considering the following pi117 tsetupd = 79 & tsetupwen = 55 K117 computed by IM after 31 iterations in 0.807 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 60 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 54 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 118 Considering the following pi118 tsetupd = 83 & tsetupwen = 55 K118 computed by IM after 31 iterations in 0.792 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 60 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 54 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 119 Considering the following pi119 tsetupd = 92 & tsetupwen = 55 K119 computed by IM after 31 iterations in 0.765 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 60 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 54 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 120 Considering the following pi120 tsetupd = 96 & tsetupwen = 55 K120 computed by IM after 31 iterations in 0.756 second: 32 states with 31 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 60 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 54 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 121 Considering the following pi121 tsetupd = 98 & tsetupwen = 55 K121 computed by IM after 32 iterations in 0.816 second: 33 states with 32 transitions explored. tsetupwen >= 54 & 60 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 60 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 54 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 122 Considering the following pi122 tsetupd = 100 & tsetupwen = 60 K122 computed by IM after 35 iterations in 0.903 second: 36 states with 37 transitions explored. 103 > tsetupd & tsetupwen > 54 & tsetupd > 99 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 123 Considering the following pi123 tsetupd = 103 & tsetupwen = 60 K123 computed by IM after 35 iterations in 0.932 second: 44 states with 44 transitions explored. 106 > tsetupd & tsetupwen > 54 & tsetupd > 100 ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 124 Considering the following pi124 tsetupd = 106 & tsetupwen = 60 K124 computed by IM after 35 iterations in 0.824 second: 36 states with 37 transitions explored. tsetupwen > 54 & tsetupd > 103 & 110 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 125 Considering the following pi125 tsetupd = 65 & tsetupwen = 61 K125 computed by IM after 33 iterations in 0.742 second: 34 states with 33 transitions explored. 66 >= tsetupd & 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 60 OR 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 60 & 66 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 126 Considering the following pi126 tsetupd = 67 & tsetupwen = 61 K126 computed by IM after 33 iterations in 0.794 second: 36 states with 36 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 69 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 60 & 65 >= tsetupwen & 69 >= tsetupd & tsetupd >= 67 OR 65 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 60 & 69 >= tsetupd OR 65 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 60 & 69 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 127 Considering the following pi127 tsetupd = 70 & tsetupwen = 61 K127 computed by IM after 31 iterations in 0.713 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 75 >= tsetupd & tsetupd >= 69 OR 65 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 60 & 75 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 128 Considering the following pi128 tsetupd = 76 & tsetupwen = 61 K128 computed by IM after 31 iterations in 0.730 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 78 >= tsetupd & tsetupd >= 75 OR 65 >= tsetupwen & tsetupd >= 75 & tsetupwen >= 60 & 78 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 129 Considering the following pi129 tsetupd = 79 & tsetupwen = 61 K129 computed by IM after 31 iterations in 0.675 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 82 >= tsetupd & tsetupd >= 78 OR 65 >= tsetupwen & tsetupd >= 78 & tsetupwen >= 60 & 82 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 130 Considering the following pi130 tsetupd = 83 & tsetupwen = 61 K130 computed by IM after 31 iterations in 0.697 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 91 >= tsetupd & tsetupd >= 82 OR 65 >= tsetupwen & tsetupd >= 82 & tsetupwen >= 60 & 91 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 131 Considering the following pi131 tsetupd = 92 & tsetupwen = 61 K131 computed by IM after 31 iterations in 0.681 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 95 >= tsetupd & tsetupd >= 91 OR 65 >= tsetupwen & tsetupd >= 91 & tsetupwen >= 60 & 95 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 132 Considering the following pi132 tsetupd = 96 & tsetupwen = 61 K132 computed by IM after 31 iterations in 0.716 second: 32 states with 31 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 65 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 60 & 97 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 133 Considering the following pi133 tsetupd = 98 & tsetupwen = 61 K133 computed by IM after 32 iterations in 0.665 second: 33 states with 32 transitions explored. tsetupwen >= 60 & 65 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 65 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 60 & 99 >= tsetupd ************************************************** BEHAVIORAL CARTOGRAPHY ALGORITHM: 134 Considering the following pi134 tsetupd = 65 & tsetupwen = 66 K134 computed by IM after 3 iterations in 0.048 second: 2 states with 1 transition explored. tsetupd >= 0 & tsetupwen > 65 & 110 >= tsetupd ************************************************** END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM Size of V0: 3082 Unsuccessful points: 2948 130 different constraints were computed. Average number of states : 35 Average number of transitions : 35 Global time spent : 106.355113983 s Time spent on IM : 99.2104394436 s Time spent to compute next point: 6.71764612198 s ************************************************** Generation of the graphical cartography... Plot cartography in 2D projected on parameters tsetupd and tsetupwen to file './test/spsmall_cart_bc.png'. IMITATOR successfully terminated (after 110.538 seconds) salloc: Relinquishing job allocation 96645 hoangia90@magi1:~/imitator$