(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.9.2-working "Butter Incaberry" (build 2363) * Git : explorder/5c40e39 * Model : '/media/gia/Data/Example-Models/flipflop-P/flipflop-P.imi' * Generated: Sat Jun 17, 2017 01:52:12 * Command : /home/gia/Desktop/imitator/bin/imitator /media/gia/Data/Example-Models/flipflop-P/flipflop-P.imi -mode EF -explOrder layerBFS -output-states -output-cart -output-result -output-trace-set -incl2 -time-limit 900 -output-prefix /media/gia/Data/Example-Models/flipflop-P/flipflop-P-layerBFS-incl2-EF ************************************************************) ------------------------------------------------------------ Number of IPTAs : 6 Number of clocks : 5 Has stopwatches? : false L/U subclass : not L/U Number of parameters : 12 Number of discrete variables : 0 Number of actions : 13 Total number of locations : 52 Average locations per IPTA : 8.6 ------------------------------------------------------------ BEGIN CONSTRAINT dG1_l >= 0 & tHold >= 0 & dG4_l >= 0 & dG2_l > dG3_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= tHold & tHI >= tHold & dG1_u >= dG1_l & dG2_u >= dG2_l & dG3_u >= dG3_l & tSetup >= 0 & tLO >= tSetup OR tHold + dG1_u >= dG2_l & dG1_u + dG3_u > dG2_l & dG1_l >= 0 & dG2_l >= 0 & tHold >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG3_l > dG4_u & dG3_u >= dG2_l & dG2_u >= dG2_l & dG1_u >= dG1_l & tHI >= tHold & dG1_u >= tHold & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tLO >= tSetup OR dG1_u >= tHold & dG1_l >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & dG3_l > tHold & dG4_u >= dG4_l & dG2_u >= dG2_l & tHold >= 0 & dG1_u >= dG1_l & dG3_u >= dG3_l & tSetup >= 0 & dG4_u >= dG3_l & tLO >= tSetup OR tSetup >= 0 & dG1_l >= 0 & tHold >= dG3_l & dG2_l + dG3_l > dG3_u + dG4_u & dG2_u >= dG1_l & dG1_u >= dG1_l & tHI >= tHold & dG1_u >= tHold & tHI >= dG2_l + dG3_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & tLO >= tSetup OR dG3_l >= 0 & tHold + dG1_u >= dG2_l & tHold >= 0 & dG2_u >= dG2_l & dG1_l >= 0 & dG2_u >= dG3_l & dG4_l >= 0 & dG2_l >= 0 & dG4_u >= dG4_l & dG3_u + dG4_u >= dG2_l + dG3_l & dG1_u >= dG1_l & dG2_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG1_u >= tHold & tLO >= tSetup OR tHold > dG1_u & dG3_l > dG1_u & dG4_l >= 0 & tHI > dG3_u + dG4_u & dG2_l > dG1_u & dG4_u >= dG4_l & tHI >= tHold & dG1_l >= 0 & tSetup >= 0 & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup & dG4_u >= dG3_l & dG1_u >= dG1_l OR dG1_l >= 0 & tHold >= 0 & dG3_u >= dG3_l & dG4_u >= dG3_l & dG4_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG1_l & dG3_l >= 0 & tHI > dG3_u + dG4_u & dG2_l > tHold + dG1_u & dG1_u >= tHold & dG3_u + dG4_u >= dG2_l + dG3_l & tSetup >= 0 & dG2_u >= dG2_l & tLO >= tSetup OR tSetup >= 0 & dG3_l >= 0 & dG1_l >= 0 & dG1_u >= dG3_l & dG4_l >= 0 & dG2_l > tHold & tHold > dG1_u & 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 tHI + tHold > dG2_l + dG3_l & dG3_l >= 0 & dG1_l >= 0 & dG1_u >= dG3_l & tHold + dG1_l > dG2_u & tHold >= dG2_l & dG4_l >= 0 & dG2_l >= 0 & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG2_u >= dG2_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= dG3_l & tHI >= tHold & dG1_u >= dG1_l & tLO >= tSetup OR tHold >= dG3_l & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG2_u >= dG3_l & tHI >= tHold & dG1_u >= tHold & dG1_l > dG2_u & dG3_u >= dG3_l & dG1_u >= dG1_l & dG2_l >= 0 & dG2_u >= dG2_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG4_u >= dG3_l & tLO >= tSetup OR dG1_l >= 0 & dG2_u >= dG1_l & dG3_l >= 0 & dG2_l > tHold & dG4_l >= 0 & tHI >= tHold & tHI > dG3_u + dG4_u & dG2_l + dG3_l > tHI & dG4_u >= dG4_l & tHold >= dG3_l & tSetup >= 0 & dG1_u >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l & tLO >= tSetup OR dG1_l >= 0 & tSetup >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & dG2_l > tHold & dG3_l > dG4_u & dG1_u >= dG1_l & tHI >= tHold & dG2_u >= dG2_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tLO >= tSetup OR dG3_l >= 0 & dG4_l >= 0 & tHold >= dG2_l & tSetup >= 0 & dG1_u >= dG1_l & dG4_u >= dG4_l & tHI >= tHold & dG2_l > dG3_u & tHI > dG3_u + dG4_u & dG2_l > dG1_u & dG1_l >= 0 & dG1_u >= tSetup & dG1_u >= dG3_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG3_u + dG4_u >= dG2_l + dG3_l & tLO >= tSetup OR dG3_u >= dG2_l & dG4_l >= 0 & dG3_l > dG4_u & dG2_l > tHold + dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG3_u >= dG3_l & tSetup >= 0 & dG1_l >= 0 & tHold >= 0 & dG1_u >= dG1_l & dG1_u >= tHold & dG2_u >= dG2_l & tLO >= tSetup OR tSetup >= 0 & dG2_u >= dG2_l & dG1_l >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & dG2_l + dG3_l > tHI & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tSetup & tHold >= dG2_l & tHI >= tHold & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= tHold & tLO >= tSetup OR tHold >= dG3_l & dG4_l >= 0 & dG3_l >= 0 & tSetup >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & dG1_l > dG2_u & dG4_u >= dG4_l & dG1_u >= tSetup & dG2_u >= dG2_l & tHI >= dG2_l + dG3_l & dG1_u >= dG1_l & dG1_u >= tHold & tHI >= tHold & dG4_u >= dG3_l & tLO >= tSetup & dG3_u >= dG3_l OR dG1_u >= dG1_l & tHI >= tHold & tHold >= 0 & dG2_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & tSetup > dG1_u & tHold + dG1_u >= dG2_l & tHI > dG3_u + dG4_u & dG3_l > dG2_u & dG1_u >= tHold & dG2_u >= dG2_l & dG1_l >= 0 & dG4_u >= dG3_l & dG3_u >= dG3_l & tLO >= tSetup OR dG4_l >= 0 & dG3_u + dG4_u >= dG2_l + dG3_l & dG2_u >= dG2_l & dG3_l > tHold & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG1_l > dG2_u & dG4_u >= dG4_l & tHold >= 0 & dG2_u >= dG3_l & dG4_u >= dG3_l & dG3_u >= dG3_l & dG1_u >= dG1_l & tLO >= tSetup OR tHold >= dG2_l & dG3_l > dG4_u & dG2_l > dG1_u & tHI > dG3_u + dG4_u & dG1_l >= 0 & tHI >= tHold & tSetup >= 0 & dG4_l >= 0 & dG2_u >= dG2_l & dG4_u >= dG4_l & dG3_u >= dG3_l & tLO >= tSetup & dG3_u >= dG2_l & dG1_u >= dG1_l OR tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & tHI > dG2_u + dG4_u & dG1_l > dG2_u & dG2_l > dG3_u & dG3_l > dG4_u & dG4_u >= dG4_l & dG1_u >= dG1_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= dG2_l OR tHI >= tHold & dG2_u + dG4_u >= tHI & tSetup >= 0 & dG1_l >= 0 & tHold + dG1_l > dG2_u & dG4_l >= 0 & dG2_l > dG3_u & dG3_l > dG4_u & tHI > dG2_u & 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 & dG3_u >= dG3_l & tLO >= tSetup OR dG1_u >= dG1_l & dG2_u >= dG1_l & tHold >= dG2_l & tHold > dG1_u & dG4_l >= 0 & dG3_l > dG4_u & tHI > dG1_u + dG4_u & tHI > dG3_u + dG4_u & dG2_l > dG3_u & tHold + dG1_l > dG2_u & dG4_u >= dG4_l & dG1_l >= 0 & tSetup >= 0 & dG2_u >= dG2_l & dG3_u >= dG3_l & tHI >= tHold & tLO >= tSetup OR dG1_l >= 0 & dG2_l > dG3_u & tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & dG4_u >= dG4_l & tHold >= dG2_l & dG1_u >= dG1_l & tHI >= tHold & dG2_u >= tHI & tLO >= tSetup & dG1_u + dG4_u >= tHI & dG3_u >= dG3_l OR tHI > dG3_u + dG4_u & tSetup >= 0 & dG1_l >= 0 & dG3_l > dG4_u & tHold > dG1_u & dG2_l > dG3_u & tHI > dG2_u & dG1_u >= dG1_l & dG4_l >= 0 & dG4_u >= dG4_l & tHold >= dG2_l & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= tHold + dG1_l OR dG2_u >= dG2_l & dG1_l >= 0 & dG4_l >= 0 & tHI >= tHold & dG2_l >= 0 & dG4_u >= dG4_l & dG1_u >= dG2_l & tHold + dG1_l > dG2_u & dG1_u >= dG1_l & tSetup > dG1_u & tHold > dG1_u & tHI > dG3_u + dG4_u & dG3_l > dG2_u & dG4_u >= dG3_l & tLO >= tSetup & dG3_u >= dG3_l OR dG3_u >= dG2_l & dG3_l >= 0 & dG1_l >= 0 & tHI >= tHold & tHI > dG1_u + dG4_u & dG2_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & tSetup > dG1_u & dG1_u >= dG2_l & dG2_u >= tHI & dG1_u >= dG1_l & dG2_u >= tHold + dG1_l & dG3_u >= dG3_l & dG4_l >= 0 & dG4_u >= dG4_l & tLO >= tSetup OR dG1_l >= 0 & dG4_l >= 0 & dG3_l >= 0 & dG1_u >= dG3_l & dG2_l > dG3_u & dG4_u >= dG4_l & tHold >= dG2_l & tHold > dG1_u & dG4_u >= dG3_l & tHI > dG3_u + dG4_u & tHI >= tHold & dG3_u >= dG3_l & tSetup > dG1_u & dG2_u >= tHold + dG1_l & dG1_u >= dG1_l & tLO >= tSetup OR dG3_l >= 0 & tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & dG1_l > dG2_u & tHI > dG2_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & dG4_u >= dG4_l & dG4_u >= dG3_l & dG1_u >= tSetup & dG1_u >= dG1_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG2_u >= dG2_l OR dG2_u + dG4_u >= tHI & tSetup >= 0 & tHI >= tHold & dG1_l >= 0 & dG3_l >= 0 & tHold + dG1_l > dG2_u & dG4_l >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & tHI > dG3_u + dG4_u & tHold > dG1_u & tHI > dG2_u & dG4_u >= dG4_l & dG1_u >= dG1_l & dG1_u >= tSetup & dG4_u >= dG3_l & tHold >= dG2_l & dG1_u + dG4_u >= tHI & dG2_u >= dG2_l & dG3_u >= dG3_l & tLO >= tSetup OR tSetup + tHold > 0 & dG1_u >= dG3_l & tHold >= dG2_l & tHI >= tHold & tSetup >= 0 & dG1_l >= 0 & tHI > dG1_u + dG4_u & dG2_u >= dG1_l & tHI > dG3_u + dG4_u & tHI + dG1_u > dG3_u + dG4_u & tHold > dG1_u & dG2_l + dG3_l > dG3_u + dG4_u & tHI > dG4_u & tHold + dG1_l > dG2_u & dG4_l >= 0 & dG3_l >= 0 & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG4_u >= dG3_l & dG1_u >= tSetup & dG3_u >= dG3_l & tLO >= tSetup OR dG3_l >= 0 & dG1_l >= 0 & dG2_l + dG3_l > dG3_u + dG4_u & tSetup >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & tHold >= dG2_l & dG1_u >= dG1_l & dG1_u >= tSetup & dG1_u + dG4_u >= tHI & dG4_u >= dG3_l & tHI >= tHold & dG3_u >= dG3_l & dG2_u >= tHI & tLO >= tSetup OR dG1_u >= dG1_l & dG3_l >= 0 & tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & tHI > dG2_u & tHI > dG3_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & dG4_u >= dG4_l & dG1_u >= tSetup & dG1_u >= dG3_l & tHold >= dG2_l & dG2_u >= tHold + dG1_l & dG1_l >= 0 & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR dG2_u >= dG2_l & dG3_l >= 0 & dG4_l >= 0 & tHold >= dG2_l & tHI > dG3_u + dG4_u & dG2_l > dG1_u & dG1_l > tSetup & dG4_u >= dG4_l & tHI >= tHold & dG1_u >= dG3_l & tSetup >= 0 & tLO >= tSetup & dG4_u >= dG3_l & dG3_u >= dG2_l & dG1_u >= dG1_l OR dG2_u >= dG1_l & dG2_u >= dG2_l & dG1_l >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & tSetup > dG1_u & dG2_l + dG3_l > tHI & dG4_u >= dG4_l & dG1_u >= dG1_l & tHold >= dG2_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= tHold & tHI >= tHold & tLO >= tSetup OR tSetup >= 0 & tHold >= dG3_l & tHI > dG3_u + dG4_u & dG2_l > tHold & dG2_l + dG3_l > tHI & dG1_l > dG2_u & dG1_u >= tSetup & tHI >= tHold & dG1_u >= dG1_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG2_u >= dG2_l & tLO >= tSetup & dG3_u >= dG3_l & dG4_u >= dG3_l OR dG1_l >= 0 & tSetup >= 0 & dG4_l >= 0 & tHold > dG1_u & dG2_l > dG3_u & dG3_l > dG4_u & tHI > dG2_u + dG4_u & dG4_u >= dG4_l & dG2_u >= dG1_l & tHI >= tHold & dG3_u >= dG3_l & dG2_u >= dG2_l & dG1_u + dG4_u >= tHI & tLO >= tSetup OR tSetup >= 0 & tHI > dG3_u + dG4_u & dG1_l >= 0 & tHI >= tHold & tHI > dG1_u + dG4_u & dG3_l > dG4_u & tHold > dG1_u & dG2_l > dG3_u & dG2_u >= tHI & dG1_u >= dG1_l & tLO >= tSetup & tHold >= dG2_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= tHold + dG1_l 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 & tHold + dG1_l > dG2_u & dG1_l >= 0 & dG4_l >= 0 & tHI > dG3_u + dG4_u & tHI > dG2_u & dG3_l > dG4_u & tHold > dG1_u & tSetup > 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_l >= 0 & dG2_u >= dG1_l & dG2_u >= dG2_l & dG1_l >= 0 & tHold > dG1_u & tHI > dG1_u + dG4_u & tHold + dG1_l > dG2_u & tHI > dG3_u + dG4_u & dG3_l > dG4_u & tSetup > dG1_u & dG3_u >= dG2_l & dG1_u >= dG2_l & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & tHI >= tHold & tLO >= tSetup & dG1_u >= dG1_l OR dG4_l >= 0 & dG1_l >= 0 & dG2_u >= tHI & dG2_l >= 0 & dG3_l > dG4_u & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_u >= dG1_l & tHI >= tHold & tLO >= tSetup & dG1_u + dG4_u >= tHI & dG3_u >= dG3_l OR dG4_l >= 0 & dG1_u >= dG2_l & dG1_u >= dG1_l & dG2_l >= 0 & tHI > dG2_u & dG3_l > dG4_u & tSetup > dG1_u & tHold > dG1_u & tHI > dG3_u + dG4_u & dG4_u >= dG4_l & dG3_u >= dG2_l & tLO >= tSetup & dG1_l >= 0 & dG3_u >= dG3_l & dG2_u >= tHold + dG1_l OR tHold > dG1_u & dG4_l >= 0 & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHI > dG2_u & dG3_l > dG1_u & dG4_u >= dG4_l & dG2_u >= tHold + dG1_l & dG1_u >= dG1_l & dG2_l >= 0 & dG1_u >= dG2_l & dG1_l >= 0 & dG3_u >= dG3_l & dG4_u >= dG3_l & tLO >= tSetup OR tHold > dG1_u & dG1_l >= 0 & dG4_l >= 0 & dG2_u >= dG3_l & dG2_l >= 0 & tHI > dG3_u + dG4_u & dG3_l > dG1_u & tSetup > dG1_u & tHold + dG1_l > dG2_u & dG4_u >= dG4_l & dG1_u >= dG2_l & tHI >= tHold & tLO >= tSetup & dG3_u >= dG3_l & dG4_u >= dG3_l & dG1_u >= dG1_l OR dG3_l >= 0 & tHold >= dG2_l & dG1_u >= dG1_l & dG2_l >= 0 & dG4_l >= 0 & tSetup > dG1_u & tHI > dG2_u & tHI > dG3_u + dG4_u & tHI > dG1_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_l >= 0 & dG1_u >= dG3_l & dG3_u >= dG3_l & dG4_u >= dG3_l & dG2_u >= tHold + dG1_l & tLO >= tSetup OR dG1_l >= 0 & dG2_l >= 0 & dG4_l >= 0 & dG3_l >= 0 & tSetup > dG1_u & tHI > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG3_u >= dG2_l & dG1_u >= dG1_l & dG4_u >= dG3_l & tHI >= tHold & dG1_u + dG4_u >= tHI & dG3_u >= dG3_l & dG2_u >= tHold + dG1_l & tLO >= tSetup OR tHI >= tHold & dG1_u >= dG3_l & dG1_l >= 0 & tHI > dG3_u + dG4_u & dG2_l > dG1_u & dG3_l >= 0 & tHold >= dG2_l & dG4_l >= 0 & dG1_u >= dG1_l & dG4_u >= dG4_l & dG2_u >= tHold + dG1_l & tSetup >= dG1_l & tLO >= tSetup & dG4_u >= dG3_l & dG3_u >= dG2_l & dG2_u >= tHI OR tSetup >= 0 & dG1_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & tHI > dG2_u + dG4_u & dG2_l + dG3_l > dG3_u + dG4_u & tHold > dG1_u & dG4_u >= dG4_l & dG4_u >= dG3_l & dG2_u >= dG1_l & dG1_u >= tSetup & dG1_u + dG4_u >= tHI & tHI >= tHold & dG3_u >= dG3_l & dG2_u >= dG2_l & tLO >= tSetup OR tSetup >= 0 & dG4_l >= 0 & dG3_l >= 0 & tHold > dG1_u & dG2_l + dG3_l > dG3_u + dG4_u & dG1_u >= dG1_l & dG4_u >= dG4_l & tHold >= dG2_l & dG2_u >= tHold + dG1_l & tHI >= tHold & dG1_u >= dG3_l & dG4_u >= dG3_l & tHI > dG3_u + dG4_u & dG3_u >= dG3_l & dG1_u >= tSetup & dG1_l >= 0 & tLO >= tSetup & tHI > dG1_u + dG4_u & dG2_u >= tHI OR dG1_l >= 0 & dG1_u >= dG3_l & dG2_u >= dG2_l & tHI >= tHold & dG2_l > dG1_u & tHI > dG3_u + dG4_u & tHold + dG1_l > dG2_u & tHold >= dG2_l & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & tLO >= tSetup & tSetup >= dG1_l & dG4_u >= dG3_l & dG3_u >= dG2_l & dG1_u >= tSetup OR tHI >= tHold & tLO >= tSetup & tSetup > dG1_u & tHI > dG2_u + dG4_u & tHold > dG1_u & dG1_l >= 0 & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l > dG4_u & dG4_l >= 0 & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG3_u >= dG2_l & dG1_u + dG4_u >= tHI & dG2_u >= dG1_l OR tHI > dG3_u + dG4_u & tHI > dG2_u & 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 & dG2_u >= tHold + dG1_l & dG1_u >= tSetup END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 213 Number of transitions : 236 Number of computed states : 244 Total computation time : 121.026 seconds States/second in state space : 1.7 (213/121.026 seconds) Computed states/second : 2.0 (244/121.026 seconds) Estimated memory : 12.803 MiB (i.e., 1678198 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 121.041 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.014 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2304 number of constraints comparisons : 2292 number of new states <= old : 22 number of new states >= old : 9 StateSpace.merging attempts : 0 StateSpace.merges : 0 StatesMerging.merging attempts : 0 StatesMerging.merges : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 121.974 seconds ------------------------------------------------------------