hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/A1.imi ./test/A1.v0 -mode cover -EFIM -merge -output-cart with -depth-limit 10 -time-limit 4500
salloc: Granted job allocation 96653
*** Warning: The argument 'with' will be ignored.
************************************************************
* IMITATOR 2.6.2 *
* *
* Etienne Andre, Ulrich Kuehne et al. *
* 2009 - 2014 *
* LSV, ENS de Cachan & CNRS, France *
* Universite Paris 13, Sorbonne Paris Cite, LIPN, France *
* *
* Build: 1311 (2014-11-17 19:19:49 UTC) *
************************************************************
Analysis time: Mon Nov 17, 2014 22:07:43
Model: ./test/A1.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: Considering a limit of 10 for the depth of the Post operation.
*** Warning: The program will try to stop after 4500 seconds.
Parsing completed after 0.011 second.
*** Warning: Parameter 'a' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'a >= 0' to the initial state of the model.
*** Warning: Parameter 'b' is not necessarily positive in the initial constraint. The behavior of IMITATOR is unspecified in this case. You are advised to add inequality 'b >= 0' to the initial state of the model.
Memory for abstract model: 134.597 KiB (i.e., 34457 words)
**************************************************
START THE BEHAVIORAL CARTOGRAPHY ALGORITHM
**************************************************
Parametric rectangle V0:
a = 0..10
& b = 0..10
Number of points inside V0: 121
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 1
Considering the following pi1
a = 0
& b = 0
*** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore.
*** Warning: This execution of IM has stopped prematurely.
K1 computed by IM after 11 iterations in 0.031 second: 11 states with 10 transitions explored.
This constraint is discarded due to premature termination.
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 2
Considering the following pi2
a = 1
& b = 0
K2 computed by IM after 2 iterations in 0.002 second: 1 state with 0 transition explored.
a > b
& 2 > b
& b >= 0
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 3
Considering the following pi3
a = 0
& b = 1
*** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore.
*** Warning: This execution of IM has stopped prematurely.
K3 computed by IM after 11 iterations in 0.030 second: 20 states with 19 transitions explored.
This constraint is valid despite premature termination.
b >= a
& 5*b >= 1
OR
b >= a
& 9*b >= 2
OR
b >= a
& 4*b >= 1
OR
b >= a
& 7*b >= 2
OR
b >= a
& 3*b >= 1
OR
b >= a
& 5*b >= 2
OR
b >= a
& 2*b >= 1
OR
b >= a
& 3*b >= 2
OR
b >= a
& b >= 1
**************************************************
BEHAVIORAL CARTOGRAPHY ALGORITHM: 4
Considering the following pi4
a = 3
& b = 2
K4 computed by IM after 2 iterations in 0.003 second: 2 states with 1 transition explored.
b >= 2
**************************************************
END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM
Size of V0: 121
Unsuccessful points: 117
3 different constraints were computed.
Average number of states : 11
Average number of transitions : 10
Global time spent : 0.0773718357086 s
Time spent on IM : 0.0674681663513 s
Time spent to compute next point: 0.00471472740173 s
**************************************************
Generation of the graphical cartography...
Plot cartography in 2D projected on parameters a and b to file './test/A1_cart_bc.png'.
IMITATOR successfully terminated (after 0.492 second)
salloc: Relinquishing job allocation 96653
salloc: Job allocation 96653 has been revoked.
hoangia90@magi1:~/imitator$