[0m************************************************************
* [1mIMITATOR 2.10.4 "Butter Jellyfish"[0m *
* *
* Etienne Andre et al. *
* 2009 - 2018 *
* LSV, ENS de Cachan & CNRS, France *
* LIPN, Universite Paris 13, France *
* www.imitator.fr *
* *
* Build: 2477 (2018-07-02 09:42:27 UTC) *
* HEAD/5b53333 *
************************************************************[0m
[0mModel: GNC-ReacNGC-param-deadline.imi[0m
[0mMode: EF-synthesis.[0m
[0mConsidering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).[0m
[0mMerging technique of [AFS13] enabled.[0m
[0mThe result will be written to a file.[0m
[0mThis model is an L-PTA.[0m
[0mThe model contains stopwatches.[0m
[0mStarting running algorithm AGsafeā¦
[0m
[0mComputing post^1 from 1 state.[0m
[0mComputing post^2 from 1 state.[0m
[0mComputing post^3 from 4 states.[0m
[0mComputing post^4 from 9 states.[0m
[0mComputing post^5 from 17 states.[0m
[0mComputing post^6 from 29 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^7 from 41 states.[0m
[0mComputing post^8 from 49 states.[0m
[0mComputing post^9 from 53 states.[0m
[0mComputing post^10 from 51 states.[0m
[0mComputing post^11 from 41 states.[0m
[0mComputing post^12 from 28 states.[0m
[0mComputing post^13 from 17 states.[0m
[0mComputing post^14 from 8 states.[0m
[0mComputing post^15 from 2 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^16 from 2 states.[0m
[0mComputing post^17 from 2 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^18 from 5 states.[0m
[0mComputing post^19 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^20 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^21 from 3 states.[0m
[0mComputing post^22 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^23 from 12 states.[0m
[0mComputing post^24 from 21 states.[0m
[0mComputing post^25 from 21 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m 3 states merged within 18 states.[0m
[0mComputing post^26 from 15 states.[0m
[0mComputing post^27 from 9 states.[0m
[0mComputing post^28 from 6 states.[0m
[0mComputing post^29 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^30 from 6 states.[0m
[0mComputing post^31 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^32 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^33 from 3 states.[0m
[0mComputing post^34 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^35 from 15 states.[0m
[0mComputing post^36 from 33 states.[0m
[0mComputing post^37 from 42 states.[0m
[0mComputing post^38 from 33 states.[0m
[0mComputing post^39 from 15 states.[0m
[0mComputing post^40 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^41 from 3 states.[0m
[0mComputing post^42 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^43 from 6 states.[0m
[0mComputing post^44 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^45 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^46 from 3 states.[0m
[0mComputing post^47 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^48 from 12 states.[0m
[0mComputing post^49 from 21 states.[0m
[0mComputing post^50 from 21 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m 1 state merged within 16 states.[0m
[0mComputing post^51 from 15 states.[0m
[0mComputing post^52 from 9 states.[0m
[0mComputing post^53 from 6 states.[0m
[0mComputing post^54 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^55 from 6 states.[0m
[0mComputing post^56 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^57 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^58 from 3 states.[0m
[0mComputing post^59 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^60 from 15 states.[0m
[0mComputing post^61 from 33 states.[0m
[0mComputing post^62 from 42 states.[0m
[0mComputing post^63 from 33 states.[0m
[0mComputing post^64 from 15 states.[0m
[0mComputing post^65 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^66 from 3 states.[0m
[0mComputing post^67 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^68 from 6 states.[0m
[0mComputing post^69 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^70 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^71 from 3 states.[0m
[0mComputing post^72 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^73 from 12 states.[0m
[0mComputing post^74 from 21 states.[0m
[0mComputing post^75 from 21 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m 3 states merged within 18 states.[0m
[0mComputing post^76 from 15 states.[0m
[0mComputing post^77 from 9 states.[0m
[0mComputing post^78 from 6 states.[0m
[0mComputing post^79 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^80 from 6 states.[0m
[0mComputing post^81 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^82 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^83 from 3 states.[0m
[0mComputing post^84 from 3 states.[0m
[0m [AGsafe] Found a new state violating the property.[0m
[0mComputing post^85 from 12 states.[0m
[0mComputing post^86 from 27 states.[0m
[0mComputing post^87 from 58 states.[0m
[0mComputing post^88 from 119 states.[0m
[0mComputing post^89 from 202 states.[0m
[0mComputing post^90 from 270 states.[0m
[0mComputing post^91 from 276 states.[0m
[0mComputing post^92 from 207 states.[0m
[0mComputing post^93 from 105 states.[0m
[0mComputing post^94 from 30 states.[0m
[0mComputing post^95 from 3 states.[0m
[0mComputing post^96 from 3 states.[0m
[0mComputing post^97 from 3 states.[0m
[0mComputing post^98 from 5 states.[0m
[0mComputing post^99 from 2 states.[0m
[0mComputing post^100 from 2 states.[0m
[0mComputing post^101 from 2 states.[0m
[0mComputing post^102 from 2 states.[0m
[0mComputing post^103 from 8 states.[0m
[0mComputing post^104 from 14 states.[0m
[0mComputing post^105 from 14 states.[0m
[0m 2 states merged within 12 states.[0m
[0mComputing post^106 from 10 states.[0m
[0mComputing post^107 from 6 states.[0m
[0mComputing post^108 from 4 states.[0m
[0mComputing post^109 from 2 states.[0m
[0mComputing post^110 from 4 states.[0m
[0mComputing post^111 from 2 states.[0m
[0mComputing post^112 from 2 states.[0m
[0mComputing post^113 from 2 states.[0m
[0mComputing post^114 from 2 states.[0m
[0mComputing post^115 from 10 states.[0m
[0mComputing post^116 from 22 states.[0m
[0mComputing post^117 from 28 states.[0m
[0mComputing post^118 from 22 states.[0m
[0mComputing post^119 from 10 states.[0m
[0mComputing post^120 from 2 states.[0m
[0mComputing post^121 from 2 states.[0m
[0mComputing post^122 from 2 states.[0m
[0mComputing post^123 from 4 states.[0m
[0mComputing post^124 from 2 states.[0m
[0mComputing post^125 from 2 states.[0m
[0mComputing post^126 from 2 states.[0m
[0mComputing post^127 from 2 states.[0m
[0mComputing post^128 from 8 states.[0m
[0mComputing post^129 from 14 states.[0m
[0mComputing post^130 from 14 states.[0m
[0m 2 states merged within 12 states.[0m
[0mComputing post^131 from 10 states.[0m
[0mComputing post^132 from 6 states.[0m
[0mComputing post^133 from 4 states.[0m
[0mComputing post^134 from 2 states.[0m
[0mComputing post^135 from 4 states.[0m
[0mComputing post^136 from 2 states.[0m
[0mComputing post^137 from 2 states.[0m
[0mComputing post^138 from 2 states.[0m
[0mComputing post^139 from 2 states.[0m
[0mComputing post^140 from 10 states.[0m
[0mComputing post^141 from 22 states.[0m
[0mComputing post^142 from 28 states.[0m
[0mComputing post^143 from 22 states.[0m
[0mComputing post^144 from 10 states.[0m
[0mComputing post^145 from 2 states.[0m
[0mComputing post^146 from 2 states.[0m
[0mComputing post^147 from 2 states.[0m
[0mComputing post^148 from 4 states.[0m
[0mComputing post^149 from 2 states.[0m
[0mComputing post^150 from 2 states.[0m
[0mComputing post^151 from 2 states.[0m
[0mComputing post^152 from 2 states.[0m
[0mComputing post^153 from 8 states.[0m
[0mComputing post^154 from 14 states.[0m
[0mComputing post^155 from 14 states.[0m
[0m 2 states merged within 12 states.[0m
[0mComputing post^156 from 10 states.[0m
[0mComputing post^157 from 6 states.[0m
[0mComputing post^158 from 4 states.[0m
[0mComputing post^159 from 2 states.[0m
[0mComputing post^160 from 4 states.[0m
[0mComputing post^161 from 2 states.[0m
[0mComputing post^162 from 2 states.[0m
[0mComputing post^163 from 2 states.[0m
[0mComputing post^164 from 2 states.[0m
[0mComputing post^165 from 8 states.[0m
[0mComputing post^166 from 18 states.[0m
[0mComputing post^167 from 38 states.[0m
[0mComputing post^168 from 76 states.[0m
[0mComputing post^169 from 128 states.[0m
[0mComputing post^170 from 174 states.[0m
[0mComputing post^171 from 184 states.[0m
[0mComputing post^172 from 144 states.[0m
[0mComputing post^173 from 78 states.[0m
[0mComputing post^174 from 26 states.[0m
[0mComputing post^175 from 4 states.[0m
[0mComputing post^176 from 4 states.[0m
[0mComputing post^177 from 4 states.[0m
[0mComputing post^178 from 6 states.[0m
[0mComputing post^179 from 2 states.[0m
[0mComputing post^180 from 2 states.[0m
[0mComputing post^181 from 2 states.[0m
[0mComputing post^182 from 2 states.[0m
[0mComputing post^183 from 6 states.[0m
[0mComputing post^184 from 8 states.[0m
[0mComputing post^185 from 6 states.[0m
[0mComputing post^186 from 2 states.[0m
[0m
Fixpoint reached at a depth of 187: 10195 states with 17905 transitions in the final state space.[0m
[0m
[AGsafe] Algorithm completed after 172.962 seconds.[0m
[0m
Final constraint such that the system is correct:[0m
[92;40m deadlineT2 >= 11
& deadlineT1 >= 4
& 5 >= deadlineT1
& 20 >= deadlineT2
& deadlineT3 = 60[0m
[94mThis good constraint is exact (sound and complete)[0m
[0m
Result written to file 'GNC-ReacNGC-param-deadline.res'.[0m
[0m[1mIMITATOR successfully terminated[0m (after 172.972 seconds)[0m