epmc

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:actuators (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files embedded.prism --property-input-files embedded.props --property-input-names actuators --translate-messages false --value-floating-point-output-native true --const MAX_COUNT=8,T=12
Default settings. The option --translate-messages is set to false to ease the parsing of the output while the --value-floating-point-output-native is set to true to get the float values printed in full, instead of with only 7 digits of precision given by the default %.7f format.
Execution
Walltime:11.910166263580322s
Return code:0
Relative Error:1.5198135697932536e-05
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property actuators
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 8548 0
iterating
iterating-progress-unbounded 20350 5.555208092034025E-6 1
iterating-progress-unbounded 42206 1.7794939590753955E-6 2
iterating-progress-unbounded 64049 5.269459539547494E-7 3
iterating-progress-unbounded 85905 1.695537930335167E-7 4
iterating-progress-unbounded 107800 4.9689928074969636E-8 5
iterating-progress-unbounded 129754 1.375552349802689E-8 6
iterating-progress-unbounded 151702 3.6833076588749236E-9 7
iterating-progress-unbounded 173633 9.658057131822773E-10 8
iterating-progress-unbounded 195565 2.494838780009445E-10 9
iterating-done 210282 9
model-checking-done 10
actuators: 0.10530205537387796