hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/spsmall.imi ./test/spsmall.v0 -mode EF -merge -output-cart salloc: Granted job allocation 94517 ************************************************************ * 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: 1308 (2014-11-12 11:09:33 UTC) * ************************************************************ Analysis time: Mon Nov 17, 2014 14:59:27 Model: ./test/spsmall.imi Mode: EF-synthesis. *** Warning: The pi0 file ./test/spsmall.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. Parsing completed after 0.030 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. Memory for abstract model: 835.628 KiB (i.e., 213921 words) Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 1 state. Computing post^4 from 2 states. 1 state merged within 3 states. Computing post^5 from 2 states. 1 state merged within 4 states. Computing post^6 from 3 states. 2 states merged within 5 states. Computing post^7 from 3 states. 2 states merged within 5 states. Computing post^8 from 3 states. 2 states merged within 5 states. Computing post^9 from 3 states. 2 states merged within 6 states. Computing post^10 from 5 states. 6 states merged within 11 states. Computing post^11 from 7 states. 6 states merged within 16 states. Computing post^12 from 12 states. 13 states merged within 25 states. Computing post^13 from 14 states. 10 states merged within 26 states. Computing post^14 from 17 states. 14 states merged within 29 states. Computing post^15 from 17 states. 11 states merged within 23 states. Computing post^16 from 17 states. 9 states merged within 24 states. Computing post^17 from 21 states. 11 states merged within 24 states. Computing post^18 from 20 states. 9 states merged within 21 states. Computing post^19 from 19 states. 7 states merged within 19 states. Computing post^20 from 17 states. 5 states merged within 17 states. Computing post^21 from 17 states. 5 states merged within 17 states. Computing post^22 from 17 states. 5 states merged within 18 states. Computing post^23 from 18 states. 5 states merged within 19 states. Computing post^24 from 19 states. 6 states merged within 20 states. Computing post^25 from 19 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 7 states merged within 23 states. Computing post^26 from 21 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 8 states merged within 26 states. Computing post^27 from 26 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 13 states merged within 28 states. Computing post^28 from 25 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 13 states merged within 30 states. Computing post^29 from 25 states. [EF-synthesis]: Found a state violating the property. 14 states merged within 29 states. Computing post^30 from 26 states. 11 states merged within 20 states. Computing post^31 from 20 states. 6 states merged within 11 states. Computing post^32 from 11 states. 3 states merged within 6 states. Computing post^33 from 6 states. [EF-synthesis]: Found a state violating the property. 2 states merged within 4 states. Computing post^34 from 4 states. 2 states merged within 2 states. Computing post^35 from 2 states. Fixpoint reached after 36 iterations: 355 states with 443 transitions explored. State space exploration completed after 8.002 seconds. Final constraint such that the property is *violated* (45 inequalities): 30 >= tsetupwen & 67 >= tsetupd & tsetupd >= 65 & tsetupwen >= 0 OR tsetupd >= 66 & tsetupwen >= 30 & 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & 95 >= tsetupd OR 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & tsetupd >= 66 & tsetupwen >= 30 & 95 >= tsetupd OR 66 >= tsetupd & 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 30 OR tsetupd >= 67 & tsetupwen >= 30 & 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & 95 >= tsetupd OR tsetupwen >= 42 & 65 >= tsetupwen & 99 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 0 & 30 >= tsetupwen & 67 >= tsetupd & tsetupd >= 66 OR tsetupwen >= 42 & 65 >= tsetupwen & 99 >= tsetupd & tsetupd >= 67 OR tsetupwen >= 30 & 34 >= tsetupwen & 97 >= tsetupd & tsetupd >= 61 + tsetupwen OR tsetupwen >= 30 & 65 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR tsetupwen >= 0 & 30 >= tsetupwen & 103 >= tsetupd & tsetupd >= 99 OR tsetupd >= 67 & tsetupwen >= 4 & 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 95 >= tsetupd OR 66 >= tsetupd & 30 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 0 OR 30 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 0 & 67 >= tsetupd OR tsetupd >= 69 & tsetupwen >= 30 & 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & 95 >= tsetupd OR tsetupwen >= 0 & 30 >= tsetupwen & 110 >= tsetupd & tsetupd >= 103 OR tsetupwen >= 0 & 4 >= tsetupwen & 99 >= tsetupd & tsetupd >= 67 OR tsetupwen >= 34 & 65 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 66 >= tsetupd & 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 42 OR 65 >= tsetupwen & tsetupd >= 66 & tsetupwen >= 42 & 99 >= tsetupd OR 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 30 & 66 >= tsetupd OR 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & tsetupd >= 67 & tsetupwen >= 30 & 95 >= tsetupd OR tsetupwen >= 8 & 30 >= tsetupwen & 97 >= tsetupd & tsetupd >= 95 OR 65 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 42 & 99 >= tsetupd OR 65 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 42 & 66 >= tsetupd OR tsetupwen >= 0 & 4 >= tsetupwen & 99 >= tsetupd & tsetupd >= 69 OR 65 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 34 & 97 >= tsetupd OR tsetupwen >= 42 & 65 >= tsetupwen & 99 >= tsetupd & tsetupd >= 69 OR 4 >= tsetupwen & tsetupd >= 67 & tsetupwen >= 0 & 99 >= tsetupd OR tsetupwen >= 4 & 8 >= tsetupwen & 97 >= tsetupd & tsetupd >= 87 + tsetupwen OR 30 >= tsetupwen & tsetupd >= 103 & tsetupwen >= 0 & 110 >= tsetupd OR 34 >= tsetupwen & tsetupd >= 61 + tsetupwen & tsetupwen >= 30 & 97 >= tsetupd OR 65 >= tsetupwen & tsetupwen + 61 >= tsetupd & tsetupd >= 69 & tsetupwen >= 30 & 95 >= tsetupd OR 65 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 30 & 99 >= tsetupd OR tsetupwen >= 4 & 30 >= tsetupwen & 99 >= tsetupd & tsetupd >= 97 OR 30 >= tsetupwen & tsetupd >= 99 & tsetupwen >= 0 & 103 >= tsetupd OR tsetupd >= 69 & tsetupwen >= 4 & 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & 95 >= tsetupd OR 30 >= tsetupwen & tsetupd >= 65 & tsetupwen >= 0 & 66 >= tsetupd OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 67 & tsetupwen >= 4 & 95 >= tsetupd OR 30 >= tsetupwen & tsetupd >= 95 & tsetupwen >= 8 & 97 >= tsetupd OR 4 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 0 & 99 >= tsetupd OR 30 >= tsetupwen & tsetupwen + 87 >= tsetupd & tsetupd >= 69 & tsetupwen >= 4 & 95 >= tsetupd OR 30 >= tsetupwen & tsetupd >= 97 & tsetupwen >= 4 & 99 >= tsetupd OR 65 >= tsetupwen & tsetupd >= 69 & tsetupwen >= 42 & 99 >= tsetupd OR 8 >= tsetupwen & tsetupd >= 87 + tsetupwen & tsetupwen >= 4 & 97 >= tsetupd Generation of the graphical cartography... Plot cartography in 2D projected on parameters tsetupd and tsetupwen to file './test/spsmall_cart_ef.png'. IMITATOR successfully terminated (after 8.826 seconds) salloc: Relinquishing job allocation 94517 salloc: Job allocation 94517 has been revoked. hoangia90@magi1:~/imitator$