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$