Benchmark

Model: | haddad-monmege v.1 (DTMC) |

Parameter(s) | N = 100, p = 0.7 |

Property: | target (prob-reach) |

Invocation (default)

mono mcsta/mcsta.exe haddad-monmege.jani --props target -E N=100,p=0.7 --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: | 7.584120035171509s |

Return code: | 0 |

Note(s): | The tool result '1104407476063/1000000000000000000000000000000000000' is tagged as incorrect. The reference result is '3152519739159347/4503599627370496' (approx. 0.7) which means a relative error of '1.0' which is larger than the goal precision '0.001'. |

Relative Error: | 1.0 |

Log

haddad-monmege.jani:model: info: haddad-monmege is a DTMC model. haddad-monmege.jani: info: Need 2 bytes per state. haddad-monmege.jani: info: Explored 201 states for N=100, p=0.7. Peak memory usage: 42 MB Analysis results for haddad-monmege.jani Experiment N=100, p=0.7 + State space exploration State size: 2 bytes States: 201 Transitions: 201 Branches: 400 Rate: 5912 states/s Time: 0.0 s + Property target Probability: 1.104407476063E-24 Bounds: [1.104407476063E-24, 1] Time: 6.7 s + Value iteration Final error: 9.9999900012859E-07 Iterations: 1000002 Time: 6.7 s