(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.8.1-working "Butter Ham" (build 2104) * Git : learning/5d10a02 * Model : '/home/gia/Desktop/experiments/Etienne/AndOr/AndOr.imi' * Generated: Sat Dec 3, 2016 03:08:32 * Command : /home/gia/Desktop/imitator/bin/imitator /home/gia/Desktop/experiments/Etienne/AndOr/AndOr.imi -mode LoopSynth -output-result -time-limit 3600 -output-prefix /home/gia/Desktop/experiments/Etienne/AndOr/LoopSynth ************************************************************) ------------------------------------------------------------ Number of IPTAs : 4 Number of clocks : 4 Has stopwatches? : false L/U subclass : L/U-PTA Number of parameters : 4 Number of discrete variables : 0 Number of actions : 9 Total number of locations : 27 Average locations per IPTA : 6.7 ------------------------------------------------------------ BEGIN CONSTRAINT dAnd_l > 0 & dOr_u >= 12 & dOr_l > 0 & 14 >= dOr_l & 20 >= dAnd_l & dOr_u >= dOr_l & dAnd_u >= dAnd_l OR 20 >= dAnd_l & 8 >= dOr_l & dAnd_l > 0 & dOr_l > 0 & dOr_u >= dOr_l & dAnd_u >= dAnd_l OR dAnd_u >= 1 + dAnd_l & dOr_u + dAnd_u >= 19 + dAnd_l & 6 >= dAnd_l & dOr_u >= dAnd_l & dAnd_u >= 5 & dAnd_l > 0 & dOr_u >= dOr_l & dOr_l > 0 OR 6 >= dAnd_l & dOr_u >= 12 + dAnd_l & dAnd_l > 0 & dAnd_u >= dAnd_l & dOr_u >= dOr_l & dOr_l > 0 OR dAnd_u >= 1 & dAnd_l > 0 & dOr_u >= 16 & dAnd_u >= dAnd_l & 7 >= dAnd_l & dOr_u >= dOr_l & dOr_l > 0 OR dOr_u + 8 >= dAnd_l & dOr_u + dAnd_u >= 21 & dOr_u >= 1 & dAnd_u >= 19 & 14 >= dAnd_l & dAnd_l > 0 & dOr_u >= dOr_l & dOr_l > 0 OR dAnd_l > 0 & dAnd_u >= 19 & dOr_u >= 16 & dAnd_u >= dAnd_l & 20 >= dAnd_l & dOr_u >= dOr_l & dOr_l > 0 OR dOr_u >= 4 + dAnd_l & 14 >= dAnd_l & dAnd_u >= 8 & dAnd_l > 0 & dOr_u >= 16 & dAnd_u >= dAnd_l & dOr_u >= dOr_l & dOr_l > 0 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : possible under-approximation Termination : time limit (4304 successors unexplored) Constraint nature : good ------------------------------------------------------------ Number of states : 23574 Number of transitions : 29511 Number of computed states : 29512 Total computation time : 5387.056 seconds States/second in state space : 4.3 (23574/5387.056 seconds) Computed states/second : 5.4 (29512/5387.056 seconds) Estimated memory : 10.466 GiB (i.e., 1404791362 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ dynamic clock elimination (preparation) : 0.000 second dynamic clock elimination : 0.000 second (0 call) ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.007 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 49970717 number of constraints comparisons : 32344171 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ cartography drawing : 0.000 second state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 5387.087 seconds ------------------------------------------------------------