************************************************************
 *  IMITATOR 2.9.2-working "Butter Incaberry"               *
 *                                                          *
 *                     Etienne Andre, Ulrich Kuehne et al.  *
 *                                             2009 - 2018  *
 *                       LSV, ENS de Cachan & CNRS, France  *
 *                       LIPN, Universite Paris 13, France  *
 *                                         www.imitator.fr  *
 *                                                          *
 *                   Build: 2402 (2018-06-07 12:48:12 UTC)  *
 *                                            HEAD/0999a7d  *
 ************************************************************
 Model: /home/royal/Desktop/experiments/Etienne/S/simop/simop.imi
 Mode: parametric non-Zeno emptiness checking (CUB transformation).
 Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).
 Time elapsing will be applied at the beginning of the computation of a new state.
 Merging technique of [AFS13] enabled.
 The result will be written to a file.
 Generating the transformed model…
  Automaton name: PLC, Number of models: 2
 Automaton name: COM, Number of models: 2
 Automaton name: NET, Number of models: 12
 Automaton name: RIO, Number of models: 1
 Automaton name: ENV, Number of models: 1
 
 Transformation completed
 Starting running algorithm NZCUB…
 
 Computing post^1 from 1 state.
 Computing post^2 from 18 states.
 Computing post^3 from 124 states.
 Computing post^4 from 474 states.
 Computing post^5 from 1206 states.
 Computing post^6 from 2156 states.
 Computing post^7 from 2861 states.
 Computing post^8 from 2954 states.
 Computing post^9 from 2536 states.
 Computing post^10 from 1872 states.
 Computing post^11 from 1222 states.
   96 states merged within 680 states.
 Computing post^12 from 584 states.
   96 states merged within 352 states.
 Computing post^13 from 256 states.
   1 state merged within 201 states.
 Computing post^14 from 200 states.
   18 states merged within 298 states.
 Computing post^15 from 280 states.
   16 states merged within 256 states.
 Computing post^16 from 240 states.
   51 states merged within 363 states.
 Computing post^17 from 312 states.
   33 states merged within 321 states.
 Computing post^18 from 288 states.
   58 states merged within 426 states.
 Computing post^19 from 368 states.
   39 states merged within 391 states.
 Computing post^20 from 352 states.
   73 states merged within 497 states.
 Computing post^21 from 424 states.
   52 states merged within 476 states.
 Computing post^22 from 424 states.
   140 states merged within 612 states.
 Computing post^23 from 472 states.
   89 states merged within 577 states.
 Computing post^24 from 488 states.
   184 states merged within 752 states.
 Computing post^25 from 568 states.
   132 states merged within 748 states.
 Computing post^26 from 616 states.
   238 states merged within 966 states.
 Computing post^27 from 728 states.
   184 states merged within 976 states.
 Computing post^28 from 792 states.
   344 states merged within 1232 states.
 Computing post^29 from 888 states.
   320 states merged within 1256 states.
 Computing post^30 from 952 states.
   537 states merged within 1529 states.
 Computing post^31 from 1024 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   517 states merged within 1581 states.
 Computing post^32 from 1104 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   716 states merged within 1868 states.
 Computing post^33 from 1224 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   638 states merged within 1894 states.
 Computing post^34 from 1344 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   800 states merged within 2224 states.
 Computing post^35 from 1504 states.
   [NZCUB] Found a cycle.
   781 states merged within 2229 states.
 Computing post^36 from 1552 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   1026 states merged within 2634 states.
 Computing post^37 from 1752 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1040 states merged within 2728 states.
 Computing post^38 from 1824 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   1210 states merged within 3026 states.
 Computing post^39 from 1976 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1164 states merged within 3036 states.
 Computing post^40 from 2040 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1297 states merged within 3345 states.
 Computing post^41 from 2248 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   1344 states merged within 3536 states.
 Computing post^42 from 2416 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1564 states merged within 3900 states.
 Computing post^43 from 2576 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1584 states merged within 4192 states.
 Computing post^44 from 2852 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   1852 states merged within 4512 states.
 Computing post^45 from 2924 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   1863 states merged within 4687 states.
 Computing post^46 from 3144 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   2159 states merged within 5119 states.
 Computing post^47 from 3328 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   2078 states merged within 5254 states.
 Computing post^48 from 3592 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   2381 states merged within 5837 states.
 Computing post^49 from 3952 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   2421 states merged within 5941 states.
 Computing post^50 from 3992 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   2554 states merged within 6314 states.
 Computing post^51 from 4280 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   2576 states merged within 6472 states.
 Computing post^52 from 4392 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   2697 states merged within 6721 states.
 Computing post^53 from 4568 states.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   3135 states merged within 7111 states.
 Computing post^54 from 4664 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   3130 states merged within 7418 states.
 Computing post^55 from 5000 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   3197 states merged within 7862 states.
 Computing post^56 from 5352 states.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   [NZCUB] Found a cycle.
   [NZCUB] Cycle found, but in 0-time
   3164 states merged within 7984 states.
 
 State space exploration stopped at a depth of 57: 96169 states with 212028 transitions in the final state space.
 
   [NZCUB] Algorithm completed after 3889.634 seconds.
 
 Final constraint such that the system is correct:
 False
 This good constraint is an under-approximation of the actual result (or the actual result itself)
 
 Result written to file '/home/royal/Desktop/experiments/Etienne/S/simop/NZCUBtrans.res'.

 IMITATOR successfully terminated (after 3889.641 seconds)