Benchmark

Model: | dpm v.2 (MA) |

Parameter(s) | N = 4, C = 8, TIME_BOUND = 5 |

Property: | PmaxQueuesFullBound (prob-reach-time-bounded) |

Invocation (default)

mono mcsta/mcsta.exe dpm.jani --props PmaxQueuesFullBound -E N=4,C=8,TIME_BOUND=5 --relative-width -O out.txt MinimalDefault settings: '--relative-width' = use relative error for sound methods, '-O out.txt Minimal' = write the property results into file out.txt with minimal formatting (will be read by get_result).

Execution

Walltime: | 295.3775613307953s |

Return code: | 0 |

Relative Error: | 0.0 |

Log

dpm.jani:model: info: dpm is an MA model. dpm.jani: info: Need 15 bytes per state. dpm.jani: info: Explored 356426 states for N=4, C=8, TIME_BOUND=5.0. dpm.jani: info: Identified 356417 maximal end components. dpm.jani: warning: Encountered a value greater than 1 during interval iteration. The final result for property "PmaxQueuesFullBound" is likely affected by floating-point errors. Peak memory usage: 129 MB Analysis results for dpm.jani Experiment N=4, C=8, TIME_BOUND=5.0 + State space exploration State size: 15 bytes States: 356426 Transitions: 418842 Branches: 681242 Rate: 306735 states/s Time: 1.4 s + Property PmaxQueuesFullBound Probability: 2.23352633608459E-08 Bounds: [2.23163925393663E-08, 2.23541341823256E-08] Time: 293.1 s + Precomputations Max. prob. 0 states: 0 Time for max. prob. 0 states: 0.1 s + End components Iterations: 2 Time: 0.2 s MECs: 356417 Transitions: 418842 Branches: 681242 + Unif+ Time: 292.7 s Max. exit rate: 4.1 Iterations (lower bound): 6 Final unif. rate (lower bound): 65.6 Iterations (upper bound): 5 Final unif. rate (upper bound): 32.8