epmc

Benchmark
Model:resource-gathering v.2 (MDP)
Parameter(s)B = 1300, GOLD_TO_COLLECT = 100, GEM_TO_COLLECT = 100
Property:expsteps (exp-steps)
Invocation (default)
./fix-syntax java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files resource-gathering.pm --property-input-files resource-gathering.prctl --property-input-names expsteps --translate-messages false --value-floating-point-output-native true --const B=1300,GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100
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.9709126949310303s
Return code:0
Note(s):The tool result '1' is tagged as incorrect. The reference result is '34900/27' (approx. 1292.5925925925926) which means a relative error of '0.9992263610315186' which is larger than the goal precision '0.001'.
Relative Error:0.9992263610315186
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property expsteps
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 99 0
iterating
iterating-done 2 0
model-checking-done 0
expsteps: 1.0