Benchmark

Model: | embedded v.1 (CTMC) |

Parameter(s) | MAX_COUNT = 8, T = 12 |

Property: | actuators (prob-reach) |

Invocation (specific)

mono mcsta/mcsta.exe embedded.jani --props actuators -E MAX_COUNT=8,T=12 --relative-width -O out.txt Minimal --unsafe -S MemorySettings specific for this benchmark: '--unsafe' = compile model without bounds and assignment checks, '-S Memory' = store all data in memory since the model is small.

Execution

Walltime: | 19.746784448623657s |

Return code: | 0 |

Note(s): | The tool result '103509702857121/1000000000000000' is tagged as incorrect. The reference result is '0.1053036557931281923418411522' (approx. 0.1053036557931282) which means a relative error of '0.017035998631723292' which is larger than the goal precision '0.001'. |

Relative Error: | 0.017035998631723292 |

Log

embedded.jani:model: info: embedded is a CTMC model. embedded.jani: info: Need 15 bytes per state. embedded.jani: info: Explored 8548 states for MAX_COUNT=8, T=12.0. Peak memory usage: 50 MB Analysis results for embedded.jani Experiment MAX_COUNT=8, T=12.0 + State space exploration State size: 15 bytes States: 8548 Transitions: 8548 Branches: 36041 Rate: 109590 states/s Time: 0.1 s + Property actuators Probability: 0.103509702857121 Bounds: [0.103509702857121, 1] Time: 18.8 s + Value iteration Final error: 9.99990153185015E-07 Iterations: 94800 Time: 18.8 s