epmc

Benchmark
Model:bluetooth v.1 (DTMC)
Parameter(s)mrec = 1
Property:time (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files bluetooth.prism --property-input-files bluetooth.props --property-input-names time --translate-messages false --value-floating-point-output-native true --const mrec=1
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:131.1619610786438s
Return code:1
Note(s):The tool result '655809805393219/5000000000000' is tagged as incorrect. The reference result is '8229' (approx. 8229.0) which means a relative error of '0.9840610084969444' which is larger than the goal precision '0.001'.
Relative Error:0.9840610084969444
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property time
start-building-explorer
start-building-initial-states-explorer
STDERR
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.base/java.util.HashMap.resize(HashMap.java:704)
	at java.base/java.util.HashMap.putVal(HashMap.java:663)
	at java.base/java.util.HashMap.put(HashMap.java:612)
	at epmc.jani.explorer.VariableValuesEnumerator.lambda$generalEnumerateBDD$0(VariableValuesEnumerator.java:473)
	at epmc.jani.explorer.VariableValuesEnumerator$$Lambda$40/1291586632.call(Unknown Source)
	at epmc.dd.EnumerateSAT.terminalCase(EnumerateSAT.java:178)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:135)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:145)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)
	at epmc.dd.EnumerateSAT.recurse(EnumerateSAT.java:151)