epmc

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:up_time (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files embedded.prism --property-input-files embedded.props --property-input-names up_time --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:1.4541740417480469s
Return code:0
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property up_time
model-checking-done 0
up_time: Could not evaluate expression i. Please check for misspelled identifiers or missing constant definitions.