************************************************************ * IMITATOR 2.9.2-working "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2017 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, France * * www.imitator.fr * * * * Build: 2363 (2017-06-08 17:40:33 UTC) * * explorder/5c40e39 * ************************************************************ Analysis time: Sat Jun 17, 2017 01:45:17  Model: /media/gia/Data/Example-Models/flipflop-P/flipflop-P.imi Mode: EF-synthesis. Exploration order: queue-based BFS with ranking system [WORK IN PROGRESS]. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). The cartography will be drawn. The result will be written to a file. The trace set(s) will be generated in a graphical mode. Description of states will be output.  Abstract model built after 0.017 second. Memory for abstract model: 1535.546 KiB (i.e., 393100 words)  Starting running algorithm AGsafe…  Entering explore_queue_bfs!!!  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property. End of Ordering!!!   Fixpoint reached: 230 states with 252 transitions in the final state space. Exiting explore_queue_bfs!!!  [AGsafe] Algorithm completed after 59.377 seconds.  Final constraint such that the system is correct:  tSetup >= 0 & dG2_u >= dG1_l & tHI >= tHold & dG3_l >= 0 & dG1_l >= 0 & tHold >= 0 & dG4_l >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & tHI + dG1_u > dG3_u + dG4_u & tHI > dG3_u + dG4_u & tHI > dG2_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG1_u >= tSetup & tHold + dG1_u >= dG3_l & dG1_u >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR dG1_l >= 0 & tHI >= tHold & dG3_l >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & dG1_u >= tHold & dG1_u > dG3_l & dG4_l >= 0 & tSetup >= 0 & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG2_u >= dG1_l & dG1_u >= tSetup & tHold >= 0 & dG3_u >= dG3_l & dG4_u >= dG3_l & tHold + dG1_u >= tHI & dG2_u >= tHI & tLO >= tSetup OR dG4_u >= dG3_l & dG4_l >= 0 & tHold + dG1_u >= dG3_l & dG1_l >= 0 & tSetup >= 0 & tHold >= 0 & tHI > dG3_u + dG4_u & dG2_l > tHold + dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tSetup & dG1_u >= tHold & dG3_u >= dG3_l & dG3_l >= 0 & dG2_u >= dG2_l & dG3_u + dG4_u >= dG2_l + dG3_l & tLO >= tSetup OR tHold >= 0 & dG2_u >= dG1_l & dG1_u >= dG1_l & tSetup >= 0 & dG2_l > dG3_u & tHI > dG3_u + dG4_u & dG1_u >= tHold & tHI >= tHold & dG1_l >= 0 & dG3_l > dG4_u & dG1_u >= tSetup & dG4_l >= 0 & dG4_u >= dG4_l & dG2_u >= dG2_l & dG3_u >= dG3_l & dG2_u >= tHI & tLO >= tSetup OR tSetup >= 0 & tHold >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & dG1_l > dG2_u & tHI > dG3_u + dG4_u & tHI >= tHold & dG4_u >= dG3_l & dG4_l >= 0 & dG4_u >= dG4_l & dG1_u >= tSetup & dG2_u >= dG2_l & dG3_l >= 0 & dG3_u >= dG3_l & dG1_u >= dG1_l & tLO >= tSetup OR dG1_l > dG2_u & tHI > dG2_u + dG4_u & dG3_l >= 0 & dG4_l >= 0 & tHold >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG1_u >= tHold & dG2_l >= 0 & dG2_u >= dG2_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR tSetup >= 0 & dG4_l >= 0 & dG2_u >= dG1_l & dG1_l >= 0 & tHold >= 0 & tHI > dG2_u & tHI > dG1_u + dG4_u & dG2_l > dG3_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tHold & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR tHI >= tHold & tSetup >= 0 & dG1_u >= dG1_l & dG2_u >= dG1_l & tHold >= 0 & dG4_l >= 0 & dG2_l > dG3_u & tHI > dG2_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= tHold & dG1_l >= 0 & dG1_u >= tSetup & dG2_u >= dG2_l & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI & tLO >= tSetup OR dG3_l > tHold + dG1_u & dG4_l >= 0 & dG2_l > tHold + dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & tHold >= 0 & tSetup >= 0 & dG1_u >= tSetup & dG1_u >= tHold & dG1_l >= 0 & dG3_u >= dG3_l & tLO >= tSetup & dG4_u >= dG3_l OR tHI > tHold + dG1_u & dG2_l + dG3_l > dG3_u + dG4_u & tHold >= 0 & dG2_l > tHold & dG3_l >= 0 & dG4_l >= 0 & dG1_l >= 0 & tSetup >= 0 & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG1_u >= tSetup & tHold + dG1_u >= dG3_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= tHold & tLO >= tSetup & dG2_u >= tHI OR dG4_l >= 0 & dG2_l >= 0 & tHold >= 0 & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG1_l > dG2_u & tSetup > dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= tHold & tHI >= tHold & dG1_u >= dG1_l & dG3_u >= dG3_l & tLO >= tSetup OR dG4_l >= 0 & tSetup >= 0 & tHold >= 0 & dG1_l > dG2_u & dG2_l > dG3_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= tSetup & dG1_u >= tHold & tHI >= tHold & dG2_u >= dG2_l & dG1_u >= dG1_l & tLO >= tSetup & dG3_u >= dG3_l OR dG4_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & dG3_l > dG4_u & dG2_l > dG3_u & dG1_l > dG2_u & dG4_u >= dG4_l & dG2_u >= dG2_l & tSetup >= 0 & dG1_u >= dG1_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l OR dG1_l >= 0 & dG3_l > dG4_u & tHI > dG2_u & tHold > dG1_u & dG2_l > tHold & tHI > dG3_u + dG4_u & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tSetup >= 0 & dG1_u >= dG1_l & tLO >= tSetup & dG2_u >= dG2_l OR dG4_l >= 0 & tSetup >= 0 & tHold >= dG2_l & dG1_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG1_u >= tSetup & dG2_l > dG1_u & tHI > dG3_u + dG4_u & dG3_u >= dG2_l & dG3_l > dG4_u & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR tHI >= tHold & tHI > dG3_u + dG4_u & tHold > dG1_u & dG3_l > dG4_u & dG4_l >= 0 & dG4_u >= dG4_l & dG2_u >= dG2_l & dG3_u >= dG3_l & dG2_l > tHold & tSetup >= dG1_l & dG1_u >= dG1_l & dG2_u >= tHI & dG1_l >= 0 & tLO >= tSetup OR tHI >= tHold & tHI > dG3_u + dG4_u & dG1_l >= 0 & tHold > dG1_u & dG3_l > dG4_u & dG2_l > dG3_u & dG4_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG1_l & tSetup >= dG1_l & tHold >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup & dG2_u >= tHI OR dG2_u >= dG3_l & dG4_l >= 0 & dG2_l >= 0 & dG3_l >= 0 & dG1_l > dG2_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & tHold > dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG4_u >= dG3_l & dG1_u >= dG1_l & dG3_u >= dG3_l & tHI >= tHold & tLO >= tSetup OR dG1_l >= 0 & tHold > dG1_u & dG4_l >= 0 & dG3_l > dG2_u & tHI > dG3_u + dG4_u & dG2_l > dG1_u & dG4_u >= dG4_l & tHI >= tHold & tSetup >= 0 & dG1_u >= dG1_l & dG2_u >= dG2_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR tHold >= dG2_l & dG2_u >= dG3_l & dG1_l >= 0 & dG2_l > dG1_u & dG4_l >= 0 & dG3_l > dG1_u & tHI > dG3_u + dG4_u & tHI > dG2_u & dG4_u >= dG4_l & dG2_u >= dG2_l & tHI >= tHold & tSetup >= 0 & dG1_u >= dG1_l & dG3_u >= dG3_l & tLO >= tSetup & dG4_u >= dG3_l OR tHI >= tHold & dG2_u >= dG3_l & dG3_u >= dG3_l & dG2_l >= 0 & dG1_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & tHI > dG2_u + dG4_u & dG2_u >= dG1_l & tHold >= dG3_l & dG2_u >= dG2_l & dG1_u + dG4_u >= tHI & dG4_l >= 0 & dG3_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & tLO >= tSetup OR tHI > dG2_u & dG3_l >= 0 & dG4_l >= 0 & tHold > dG1_u & dG2_l > tHold & tHI > dG3_u + dG4_u & dG2_u >= dG3_l & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_l >= 0 & tSetup >= 0 & dG1_u >= dG1_l & dG1_u >= tSetup & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR dG1_l >= 0 & dG2_l > dG1_u & dG4_l >= 0 & tHI > dG3_u + dG4_u & dG3_l > dG1_u & tHI > tHold + dG1_u & dG4_u >= dG4_l & tHold >= dG2_l & tSetup >= 0 & dG1_u >= dG1_l & dG3_u >= dG3_l & tLO >= tSetup & dG4_u >= dG3_l & dG2_u >= tHI OR dG1_u >= dG3_l & dG1_l >= 0 & tSetup >= 0 & tHI > tHold + dG1_u & dG2_l + dG3_l > dG3_u + dG4_u & dG1_u >= tSetup & dG1_u >= dG1_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tHold >= dG2_l & dG3_l >= 0 & tLO >= tSetup & dG2_u >= tHI OR tHold >= dG2_l & dG3_l >= 0 & tHI > dG1_u + dG4_u & dG3_u >= dG3_l & dG2_u >= dG2_l & dG4_l >= 0 & dG2_l > dG1_u & dG1_l > tSetup & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG4_u >= dG3_l & dG1_u >= dG3_l & tHI >= tHold & tSetup >= 0 & dG1_u >= dG1_l & dG3_u + dG4_u >= dG2_l + dG3_l & tLO >= tSetup OR tHold >= dG2_l & tSetup >= 0 & dG1_l >= 0 & dG4_l >= 0 & dG2_l > dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG1_u >= tSetup & dG2_u >= dG2_l & dG3_l >= 0 & dG3_u + dG4_u >= dG2_l + dG3_l & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI & tLO >= tSetup OR dG4_l >= 0 & dG2_u >= dG2_l & dG2_l > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG1_u & dG4_u >= dG4_l & dG3_u >= dG3_l & dG1_l >= 0 & dG1_u >= tSetup & tHold + dG1_u >= tHI & tSetup >= 0 & dG1_u >= dG1_l & tHI >= tHold & dG4_u >= dG3_l & tLO >= tSetup & dG2_u >= tHI OR dG2_u >= dG1_l & tHI >= tHold & tHold >= 0 & dG4_l >= 0 & dG1_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG3_l > dG4_u & dG2_l > tHold & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tHold & dG1_u + dG4_u >= tHI & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG3_l & dG4_l >= 0 & dG2_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG3_l > tHold + dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_l >= 0 & tHold >= 0 & dG1_u >= dG1_l & dG1_u >= tHold & dG3_u >= dG3_l & tLO >= tSetup & dG4_u >= dG3_l OR tHI >= tHold & tHold >= 0 & dG2_u + dG4_u >= tHI & dG2_l > tHold & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG1_l > dG2_u & dG2_u >= dG2_l & dG4_l >= 0 & dG3_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & dG3_u >= dG3_l & tLO >= tSetup & dG1_u >= dG1_l OR dG2_u >= dG1_l & dG2_u >= dG3_l & dG2_u >= dG2_l & dG4_l >= 0 & dG1_l >= 0 & tHold >= 0 & tHI > dG1_u + dG4_u & dG2_l > tHold & dG3_l > tHold & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tHold & dG3_u >= dG3_l & tHold + dG1_u >= dG3_l & dG3_u >= dG2_l & tLO >= tSetup & dG4_u >= dG3_l OR dG2_u >= dG3_l & dG4_l >= 0 & dG2_u >= dG1_l & dG2_l >= 0 & dG1_l >= 0 & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG3_l > tHold & dG4_u >= dG4_l & tHold >= dG2_l & dG1_u >= dG1_l & dG1_u >= tHold & tHold + dG1_u >= dG3_l & dG4_u >= dG3_l & dG3_u >= dG3_l & tLO >= tSetup OR tHold >= 0 & tHI >= tHold & dG3_l >= 0 & dG1_l >= 0 & dG2_u >= dG1_l & dG4_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG2_l > tHold & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u + dG4_u >= tHI & dG4_u >= dG3_l & dG2_u >= tHI & dG1_u >= tHold & dG3_u >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup OR dG4_l >= 0 & dG1_u + dG4_u >= tHI & tHold >= dG2_l & dG3_l >= 0 & dG1_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG2_l > dG3_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG4_u >= dG3_l & dG2_u + dG4_u >= tHI & dG2_u >= dG2_l & dG1_u >= tHold & dG3_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG2_l & dG2_l > tHold + dG1_u & dG3_l > dG4_u & tHI > dG3_u + dG4_u & dG4_l >= 0 & dG1_u >= dG1_l & tSetup >= 0 & dG4_u >= dG4_l & tHold >= 0 & dG1_u >= tSetup & dG3_u >= dG3_l & dG1_l >= 0 & dG1_u >= tHold & tLO >= tSetup & dG3_u >= dG2_l OR dG2_u >= dG1_l & dG1_l >= 0 & tHold > dG1_u & tSetup >= 0 & tHold >= dG2_l & dG4_l >= 0 & dG2_l > dG3_u & tHI > dG1_u + dG4_u & dG3_l > dG4_u & tHI > dG2_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & tHI >= tHold & dG1_u >= dG1_l & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR tHI >= tHold & dG2_l >= 0 & dG1_l >= 0 & tHI > dG2_u & tSetup > dG1_u & dG3_l > dG4_u & tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & dG3_u >= dG2_l & tHold >= dG2_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG2_u >= dG1_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tLO >= tSetup OR tHold >= dG2_l & dG1_l >= 0 & dG2_l >= 0 & tSetup > dG1_u & dG3_l > dG4_u & tHI > dG2_u + dG4_u & tHI > dG3_u + dG4_u & dG2_u >= dG2_l & dG2_u >= dG1_l & tHI >= tHold & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI & tLO >= tSetup OR dG2_l > dG3_u & dG2_u >= dG1_l & dG2_l + dG3_l > dG3_u + dG4_u & tHI >= tHold & dG3_l >= 0 & dG4_l >= 0 & tSetup >= 0 & tHI > dG2_u & dG1_l > tSetup & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHold >= dG2_l & dG2_u >= dG2_l & dG1_u + dG4_u >= tHI & tLO >= tSetup & dG3_u >= dG3_l OR tHI >= tHold & tHI > dG1_u + dG4_u & dG3_u >= dG2_l & tHold >= dG2_l & dG1_l >= 0 & dG2_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & dG3_l > dG4_u & tSetup > dG1_u & dG1_u >= dG1_l & dG3_u >= dG3_l & dG4_l >= 0 & dG4_u >= dG4_l & tLO >= tSetup & dG2_u >= tHI OR dG1_u >= dG2_l & dG4_l >= 0 & dG1_u >= dG1_l & tHold > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG2_u & tSetup > dG1_u & dG4_u >= dG4_l & tHI >= tHold & dG1_l >= 0 & dG2_l >= 0 & dG2_u >= dG2_l & dG4_u >= dG3_l & tLO >= tSetup & dG3_u >= dG3_l OR dG4_l >= 0 & dG1_u >= dG3_l & dG3_l >= 0 & dG1_l >= 0 & dG2_l > dG3_u & dG4_u >= dG4_l & tHold >= dG2_l & dG1_u >= dG1_l & tHold > dG1_u & tHI >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & tHI > dG3_u + dG4_u & tSetup > dG1_u & tLO >= tSetup & dG2_u >= tHI OR dG1_u >= dG3_l & dG3_l >= 0 & dG4_l >= 0 & dG2_u >= tHI & tSetup >= 0 & tHI > dG3_l & tHold > dG1_u & dG1_l > tSetup & dG2_l > tHold & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup OR dG3_l >= 0 & tHold >= dG2_l & dG1_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG3_l & dG2_l > dG3_u & tSetup >= dG1_l & tHI > dG3_u + dG4_u & tHI >= tHold & dG1_u >= tSetup & tHI > dG1_u + dG4_u & dG2_l > dG1_u & dG2_u >= dG2_l & dG3_u + dG4_u >= dG2_l + dG3_l & dG3_u >= dG3_l & tLO >= tSetup OR dG2_l >= 0 & dG2_u >= dG2_l & dG4_l >= 0 & dG3_l > dG1_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG4_u >= dG4_l & tHold + dG1_u >= tHI & dG1_l >= 0 & dG1_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup & dG2_u >= tHI OR dG1_l >= 0 & dG2_u >= dG2_l & dG2_l >= 0 & tHI > dG1_u + dG4_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG1_u >= dG1_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tHold + dG1_u >= tHI & dG1_u >= tHold & tLO >= tSetup & dG2_u >= tHI OR dG1_u >= tHold & tHold >= dG2_l & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG1_l > dG2_u & tHI >= tHold & dG2_u + dG4_u >= tHI & dG3_l >= 0 & dG4_l >= 0 & dG2_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG2_l & dG4_u >= dG3_l & dG1_u >= dG1_l & dG3_u >= dG3_l & tLO >= tSetup OR dG1_u >= tHold & tHold + dG1_u >= dG3_l & dG4_l >= 0 & dG1_l >= 0 & dG2_l > dG3_u & dG3_l > tHold & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHI > dG2_u & dG4_u >= dG4_l & dG2_u >= dG1_l & dG1_u >= dG1_l & tHold >= 0 & dG2_u >= dG2_l & dG4_u >= dG3_l & dG3_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG1_l & dG3_l >= 0 & dG1_l >= 0 & dG4_l >= 0 & dG2_l > tHold & tHI > dG1_u + dG4_u & tHI > dG2_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tHold & dG4_u >= dG3_l & dG3_u >= dG3_l & tHold >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup OR tHold + dG1_u >= dG3_l & tHold >= 0 & dG1_l >= 0 & tHI > dG1_u + dG4_u & dG3_u >= dG3_l & dG2_l > dG3_u & dG4_l >= 0 & dG4_u >= dG3_l & dG4_u >= dG4_l & tHI > dG3_u + dG4_u & dG2_u >= dG2_l & dG1_u >= dG1_l & tHI > tHold + dG1_u & dG3_l >= 0 & tSetup > dG1_u & dG1_u >= tHold & tLO >= tSetup & dG2_u >= tHI OR dG4_l >= 0 & dG2_l >= 0 & dG1_l >= 0 & dG3_l >= 0 & dG4_u >= dG4_l & tHold >= dG2_l & dG3_u >= dG2_l & dG2_u >= dG3_l & dG2_u >= dG2_l & dG2_u >= dG1_l & dG1_u >= dG1_l & dG3_u >= dG3_l & tHold >= dG3_l & tHI > dG3_u + dG4_u & dG1_u >= tHold & tSetup > dG1_u & tHI > dG1_u + dG4_u & dG4_u >= dG3_l & tLO >= tSetup OR dG2_l >= 0 & dG4_l >= 0 & tHold > dG1_u & dG3_l > dG4_u & tHI > dG3_u + dG4_u & tHI > dG2_u + dG4_u & dG1_l > dG2_u & tSetup > dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG3_u >= dG2_l & dG1_u >= dG1_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l OR dG2_l >= 0 & dG1_l >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & tHI > dG2_u & tSetup > dG1_u & dG3_l > dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_u >= dG1_l & dG1_u + dG4_u >= tHI & dG2_u + dG4_u >= tHI & tHI >= tHold & dG3_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG1_l & dG1_l >= 0 & dG2_u + dG4_u >= tHI & tHI >= tHold & dG2_l > dG3_u & dG4_l >= 0 & tHI > dG2_u & tHold > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tSetup >= dG1_l & tHold >= dG2_l & dG1_u + dG4_u >= tHI & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR tSetup >= dG1_l & dG3_l >= 0 & dG1_l >= 0 & dG4_l >= 0 & tHold > dG1_u & dG2_l > dG3_u & tHI > dG2_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG1_l & dG1_u >= tSetup & dG1_u + dG4_u >= tHI & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= dG2_l OR tHI >= tHold & tHI > dG1_u + dG4_u & dG4_l >= 0 & tHold > dG1_u & dG3_l > dG4_u & dG2_l > tHold & dG1_l > tSetup & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & tSetup >= 0 & dG1_u >= dG1_l & dG3_u >= dG3_l & dG2_u >= tHI & tLO >= tSetup & dG2_u >= dG2_l OR tHI >= tHold & tHI > dG1_u + dG4_u & tHold > dG1_u & dG4_l >= 0 & dG1_l > tSetup & tHI > dG3_u + dG4_u & dG2_l > dG3_u & dG3_l > dG4_u & dG4_u >= dG4_l & tSetup >= 0 & tHold >= dG2_l & dG1_u >= dG1_l & dG3_u >= dG3_l & tLO >= tSetup & dG2_u >= tHI OR tHold + dG1_u >= tHI & dG3_l >= 0 & dG4_l >= 0 & dG2_l >= 0 & dG1_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & tSetup > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI & tLO >= tSetup & dG2_u >= tHI OR dG2_l > dG3_u & tSetup >= 0 & dG4_l >= 0 & dG3_l > dG4_u & tHold > dG1_u & tHI > dG3_u + dG4_u & dG1_l > tSetup & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG1_u + dG4_u >= tHI & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= tHI OR dG2_u >= dG3_l & dG4_l >= 0 & dG1_l >= 0 & dG3_l >= 0 & dG2_l > tHold & tHI > dG3_u + dG4_u & tSetup > dG1_u & tHI > dG1_u + dG4_u & tHold > dG1_u & tHI > dG2_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup & dG2_u >= dG2_l OR dG2_u >= dG3_l & dG1_l >= 0 & dG2_l >= 0 & dG3_u >= dG3_l & dG3_u >= dG2_l & dG1_u >= dG2_l & dG3_l >= 0 & dG2_u >= dG1_l & dG2_u >= dG2_l & tHI > dG3_u + dG4_u & dG1_u >= dG1_l & tHI > dG2_u & tHI > dG1_u + dG4_u & tHold > dG1_u & tSetup > dG1_u & tHI >= tHold & tLO >= tSetup & dG4_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l OR dG1_l >= 0 & dG1_u >= dG3_l & tHI >= tHold & tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & dG2_l > dG3_u & tSetup > dG1_u & dG1_u >= dG1_l & dG2_u >= dG1_l & tHI > dG2_u & dG2_u >= dG2_l & tLO >= tSetup & tHold >= dG2_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l OR dG1_u >= dG1_l & tHold >= dG2_l & dG4_l >= 0 & dG3_l >= 0 & dG2_u >= dG2_l & dG4_u >= dG4_l & tHI > dG2_u & dG2_l > dG1_u & tHI > dG3_u + dG4_u & tHI >= tHold & tSetup >= dG1_l & dG1_u >= dG3_l & tLO >= tSetup & dG1_l >= 0 & dG4_u >= dG3_l & dG3_u >= dG2_l OR dG3_l >= 0 & dG2_u + dG4_u >= tHI & tHI >= tHold & dG2_u >= dG1_l & dG2_l > dG3_u & dG4_l >= 0 & dG1_l >= 0 & tHI > dG2_u & tHold > dG1_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG4_u >= dG3_l & dG2_u >= dG2_l & dG1_u + dG4_u >= tHI & tLO >= tSetup & dG3_u >= dG3_l OR dG3_l >= 0 & tHold >= dG2_l & dG4_l >= 0 & dG1_u >= dG1_l & tHold >= dG3_l & dG2_l >= 0 & dG1_u + dG4_u >= tHI & dG1_l >= 0 & tHI > dG3_u + dG4_u & tHI > dG2_u & tSetup > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG2_u >= dG1_l & tHI >= tHold & dG4_u >= dG3_l & dG2_u + dG4_u >= tHI & dG3_u >= dG3_l & tLO >= tSetup OR dG4_l >= 0 & dG3_l >= 0 & tHold >= dG2_l & dG2_u >= dG1_l & tSetup >= 0 & dG1_l >= 0 & tHold > dG1_u & tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & tHI > dG2_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG4_u >= dG3_l & dG1_u >= dG3_l & dG1_u >= tSetup & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG1_l & dG2_u + dG4_u >= tHI & dG4_l >= 0 & dG1_l >= 0 & dG3_l >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & tHold >= dG2_l & tSetup >= dG1_l & dG1_u >= tSetup & dG4_u >= dG3_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI OR dG2_l > tHold & dG1_l >= 0 & tHI > dG1_u + dG3_l & dG3_u >= dG3_l & tHI > dG1_u + dG4_u & dG4_l >= 0 & dG4_u >= dG3_l & dG4_u >= dG4_l & tHI > dG3_u + dG4_u & dG2_u >= dG2_l & dG3_l >= 0 & dG1_u >= dG1_l & tHold > dG1_u & tSetup > dG1_u & tHI > tHold + dG1_u & tLO >= tSetup & dG2_u >= tHI OR dG3_u >= dG3_l & dG3_u >= dG2_l & tHI > dG1_u + dG3_l & dG2_l >= 0 & dG1_l >= 0 & tHI > dG1_u + dG4_u & dG4_u >= dG3_l & dG4_l >= 0 & dG4_u >= dG4_l & tHI > dG3_u + dG4_u & dG1_u >= dG2_l & dG3_l >= 0 & dG1_u >= dG1_l & tSetup > dG1_u & tHold > dG1_u & tHI > tHold + dG1_u & tLO >= tSetup & dG2_u >= tHI OR dG1_u >= dG1_l & dG4_l >= 0 & dG3_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_u >= dG3_l & dG4_u >= dG3_l & tSetup >= dG1_l & tHI > dG3_u + dG4_u & tHI > tHold + dG1_u & dG2_l > dG1_u & tLO >= tSetup & tHold >= dG2_l & dG1_l >= 0 & dG2_u >= tHI OR dG1_l >= 0 & dG2_l > tHold & dG4_l >= 0 & tHI > tHold + dG1_u & tHold > dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG2_l & tSetup >= dG1_l & dG1_u >= dG1_l & dG3_l >= 0 & dG3_u >= dG3_l & dG1_u + dG4_u >= tHI & tLO >= tSetup & dG2_u >= tHI OR tHold >= dG3_l & tHold >= dG2_l & dG4_l >= 0 & dG1_l >= 0 & tSetup > dG1_u & tHI > tHold + dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG3_u >= dG3_l & dG3_u >= dG2_l & dG1_u + dG4_u >= tHI & tLO >= tSetup & dG2_l >= 0 & dG3_l >= 0 & dG2_u >= tHI OR dG4_l >= 0 & tHold > dG1_u & tHI > dG3_u + dG4_u & dG2_l > tHold & dG3_l > dG1_u & tHI > tHold + dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_l >= 0 & dG1_u >= tSetup & tSetup >= 0 & dG1_u >= dG1_l & tLO >= tSetup & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= tHI OR tHI >= tHold & dG1_l >= 0 & dG4_l >= 0 & dG3_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & dG2_l > tHold & tHI > dG1_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG3_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tSetup >= dG1_l & dG1_u >= tSetup & dG2_u >= tHI & tLO >= tSetup & dG2_u >= dG2_l OR dG1_u >= dG3_l & dG4_l >= 0 & dG3_l >= 0 & tHold + dG1_u >= tHI & dG1_l >= 0 & tHI >= tHold & tHold > dG1_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG2_l > tHold & dG4_u >= dG4_l & dG1_u >= dG1_l & dG2_u >= tHI & dG4_u >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup & dG3_u >= dG3_l OR dG3_u >= dG2_l & tHold > dG1_u & tHold + dG1_u >= tHI & dG3_l >= 0 & tHold >= dG2_l & dG4_l >= 0 & dG1_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & tHI > dG1_u + dG4_u & dG1_u >= dG3_l & dG4_u >= dG3_l & tHI > dG3_u + dG4_u & dG2_l >= 0 & tSetup > dG1_u & tLO >= tSetup & dG2_u >= tHI OR dG2_l + dG3_l > dG3_u + dG4_u & tHold + dG1_u >= tHI & dG1_u >= dG3_l & dG3_l >= 0 & tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & tHI > dG3_l & tHI > dG3_u + dG4_u & dG1_l > tSetup & dG4_u >= dG4_l & tHold >= dG2_l & dG1_u >= dG1_l & dG4_u >= dG3_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= tHI OR dG2_u >= dG1_l & tHI > dG1_u + dG4_u & tHold >= 0 & dG4_l >= 0 & dG2_u >= dG2_l & dG1_l >= 0 & tHI > dG3_u + dG4_u & tHI > dG2_u & dG3_l > dG4_u & dG2_l > tHold & tSetup > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG3_u >= dG3_l & dG1_u >= tHold & dG3_u >= dG2_l & tLO >= tSetup OR tHold >= dG2_l & dG1_l >= 0 & dG2_u >= dG2_l & dG1_u + dG4_u >= tHI & dG1_u >= dG1_l & dG2_l >= 0 & dG4_l >= 0 & tHI > dG2_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG2_u >= dG1_l & tHI >= tHold & dG1_u >= tHold & dG2_u + dG4_u >= tHI & dG3_u >= dG3_l & tLO >= tSetup OR tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & tHold >= 0 & dG2_u >= dG2_l & dG1_l >= 0 & dG3_l > dG4_u & tHI > tHold + dG1_u & dG2_l > dG3_u & tSetup > dG1_u & dG1_u >= dG1_l & tLO >= tSetup & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG1_u >= tHold & dG2_u >= tHI OR tHold >= 0 & dG4_l >= 0 & tHI > dG1_u + dG4_u & dG1_l >= 0 & tHI > tHold + dG1_u & dG2_l > tHold & tHI > dG3_u + dG4_u & dG3_l > dG4_u & tSetup > dG1_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG3_u >= dG3_l & dG1_u >= tHold & dG3_u >= dG2_l & tLO >= tSetup & dG2_u >= tHI OR dG1_u >= tHold & dG3_u >= dG2_l & dG4_l >= 0 & dG1_l >= 0 & tHI > dG3_u + dG4_u & tHI > tHold + dG1_u & tSetup > dG1_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tLO >= tSetup & tHold >= dG2_l & dG2_l >= 0 & dG3_u >= dG3_l & dG2_u >= tHI OR tHold >= dG2_l & dG2_l >= 0 & tHold + dG1_u >= tHI & dG1_l >= 0 & dG3_l > dG4_u & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG1_u >= dG1_l & dG2_u >= dG1_l & dG1_u >= tHold & tHI >= tHold & dG4_l >= 0 & dG1_u + dG4_u >= tHI & dG4_u >= dG4_l & dG3_u >= dG3_l & tLO >= tSetup & dG2_u >= tHI OR dG4_l >= 0 & dG2_u >= dG1_l & dG1_l >= 0 & tHold >= 0 & tHI > dG1_u + dG4_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG2_u & dG2_l > tHold & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tHold & dG2_u >= dG2_l & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR dG4_l >= 0 & dG1_u >= dG1_l & tHold >= dG2_l & dG3_l > dG2_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHI >= tHold & dG4_u >= dG4_l & dG1_u >= tHold & dG1_l >= 0 & dG2_l >= 0 & dG2_u >= dG2_l & dG2_u >= dG1_l & dG4_u >= dG3_l & tLO >= tSetup & dG3_u >= dG3_l OR dG1_l >= 0 & dG4_l >= 0 & tSetup > dG1_u & dG3_l > tHold & tHI > dG2_u + dG4_u & tHI > dG3_u + dG4_u & dG2_l > tHold & dG4_u >= dG4_l & dG2_u >= dG1_l & dG3_u >= dG2_l & dG3_u >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup & tHold >= 0 & dG4_u >= dG3_l & dG1_u + dG4_u >= tHI OR dG1_l >= 0 & dG3_u >= dG3_l & dG3_l >= 0 & tHold >= 0 & dG4_l >= 0 & tHI > dG2_u & dG2_l > tHold & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG2_u >= dG1_l & dG4_u >= dG3_l & tLO >= tSetup & dG3_u >= dG2_l & dG1_u + dG4_u >= tHI & dG2_u + dG4_u >= tHI OR dG3_l >= 0 & dG4_l >= 0 & tHI > dG1_u + dG4_u & dG1_l >= 0 & tHI > tHold + dG1_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG2_l > tHold & dG4_u >= dG4_l & dG1_u >= dG1_l & tHold >= dG3_l & dG1_u >= tHold & dG4_u >= dG3_l & dG3_u >= dG2_l & tLO >= tSetup & dG2_u >= tHI OR dG2_u >= dG2_l & tHI > dG1_u + dG4_u & dG3_u >= dG3_l & dG1_l >= 0 & dG2_l > tHold & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG1_u >= dG1_l & dG1_u >= tHold & tLO >= tSetup & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & tHold + dG1_u >= tHI & dG2_u >= tHI OR tHI > dG3_u + dG4_u & tHI >= tHold & tLO >= tSetup & tSetup >= dG1_l & tHold > dG1_u & dG1_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= dG2_l & dG2_l > tHold & dG1_u >= tSetup & tHold + dG1_u >= tHI & dG1_u + dG4_u >= tHI & dG2_u >= tHI OR tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & tHI >= tHold & tLO >= tSetup & tSetup >= dG1_l & tHold >= dG2_l & tHold > dG1_u & dG1_l >= 0 & dG1_u >= dG3_l & dG2_l + dG3_l > dG3_u + dG4_u & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= tSetup & tHold + dG1_u >= tHI & dG2_u >= tHI OR tHI > dG3_u + dG4_u & tHI >= tHold & tLO >= tSetup & tSetup >= dG1_l & tHold >= dG2_l & dG1_l >= 0 & dG1_u >= dG3_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & dG3_u >= dG2_l & dG2_l > dG1_u & dG1_u >= tSetup & tHold + dG1_u >= tHI & dG2_u >= tHI OR dG2_l > dG3_u & tHI > dG3_u + dG4_u & tHI > dG2_u & tLO >= tSetup & tSetup > dG1_u & tHold >= dG3_l & dG1_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG2_u >= dG1_l & dG1_u >= tHold & dG2_l > tHold & dG1_u + dG4_u >= tHI & dG2_u + dG4_u >= tHI OR tHI > dG1_u + dG4_u & tLO >= tSetup & tSetup > dG1_u & tHold >= dG2_l & dG1_l >= 0 & dG2_l > dG3_u & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= dG1_l & dG1_u >= tHold & tHold + dG1_u >= tHI & dG2_u >= tHI OR tHI > dG3_u + dG4_u & tHI >= tHold & tLO >= tSetup & tSetup > dG1_u & tHold >= dG3_l & tHold >= dG2_l & dG1_l >= 0 & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG3_u >= dG2_l & dG1_u >= dG1_l & dG2_u >= dG1_l & dG1_u >= tHold & tHold + dG1_u >= tHI & dG1_u + dG4_u >= tHI & dG2_u >= tHI This good constraint is exact (sound and complete) 14.228 MiB (i.e., 1864899 words of size 8)  Result written to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-queueBFSRS-incl-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 230 Number of transitions : 252 Number of computed states : 253 Total computation time : 139.822 seconds States/second in state space : 1.6 (230/139.822 seconds) Computed states/second : 1.8 (253/139.822 seconds) Estimated memory : 17.145 MiB (i.e., 2247245 words of size 8)  Generating graphical output to '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-queueBFSRS-incl-EF-statespace.jpg'… Writing the states description to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-queueBFSRS-incl-EF-statespace.states'…  Drawing the cartography… Plot cartography in 2D projected on parameters tHI and tLO to file '/media/gia/Data/Example-Models/flipflop-P/flipflop-P-queueBFSRS-incl-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 139.837 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.014 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1395 number of constraints comparisons : 1389 number of new states <= old : 23 number of new states >= old : 0 StateSpace.merging attempts : 0 StateSpace.merges : 0 StatesMerging.merging attempts : 0 StatesMerging.merges : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 2.023 seconds cartography drawing : 0.530 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 145.588 seconds IMITATOR successfully terminated (after 145.591 seconds) Estimated memory used: 78.183 MiB (i.e., 10247655 words of size 8)