hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/A1.imi ./test/A1.v0 -mode EF -merge -output-cart -depth-limit 10
salloc: Granted job allocation 96631
************************************************************
* 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:17:11
Model: ./test/A1.imi
Mode: EF-synthesis.
*** Warning: The pi0 file ./test/A1.v0 will be ignored since this is a synthesis with respect to a property.
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.
Parsing completed after 0.024 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: 119.269 KiB (i.e., 30533 words)
Computing post^1 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^2 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^3 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^4 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^5 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^6 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^7 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^8 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^9 from 1 state.
[EF-synthesis]: Found a state violating the property.
Computing post^10 from 1 state.
[EF-synthesis]: Found a state violating the property.
*** Warning: The limit depth (10) has been reached. The exploration now stops, although there were still 1 state to explore.
Fixpoint reached after 11 iterations: 21 states with 20 transitions explored.
State space exploration completed after 0.073 second.
Final constraint such that the property is *violated* (10 inequalities):
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
OR
b >= 2
Generation of the graphical cartography...
Plot cartography in 2D projected on parameters a and b to file './test/A1_cart_ef.png'.
IMITATOR successfully terminated (after 0.374 second)
salloc: Relinquishing job allocation 96631
hoangia90@magi1:~/imitator$