PRISM-TUM

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:actuators (prob-reach)
Invocation (specific)
./pet/bin/pet reachability --heuristic DIFFERENCE --precision 0.001 --relative-error --only-result -m embedded.prism -p embedded.props --property actuators --const MAX_COUNT=8,T=12
DIFFERENCE is a slightly more greedy sampling heuristic which performs way better on this model.
Execution
Walltime:2.4949018955230713s
Return code:0
Relative Error:0.00031371377017248283
Log
0.1053366910