epmc

Benchmark
Model:eajs v.1 (MDP)
Parameter(s)N = 5, energy_capacity = 250, B = 11
Property:ExpUtil (exp-reward)
Invocation (default)
./fix-syntax java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files eajs.5.prism --property-input-files eajs.props --property-input-names ExpUtil --translate-messages false --value-floating-point-output-native true --const energy_capacity=250,B=11
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:204.72263193130493s
Return code:1
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property ExpUtil
STDERR
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at epmc.expression.standard.ExpressionOperator.replaceChildren(ExpressionOperator.java:134)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:926)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:872)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:924)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:872)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:924)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:872)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:924)
	at epmc.prism.model.convert.PRISM2JANIConverter.prism2jani(PRISM2JANIConverter.java:872)
	at epmc.prism.model.convert.PRISM2JANIConverter.moduleToAutomaton(PRISM2JANIConverter.java:830)
	at epmc.prism.model.convert.PRISM2JANIConverter.computeAutomata(PRISM2JANIConverter.java:663)
	at epmc.prism.model.convert.PRISM2JANIConverter.convert(PRISM2JANIConverter.java:228)
	at epmc.prism.model.LowLevelPRISMBuilder.toJANI(LowLevelPRISMBuilder.java:80)
	at epmc.prism.model.LowLevelPRISMBuilder.build(LowLevelPRISMBuilder.java:93)
	at epmc.modelchecker.UtilModelChecker.buildLowLevel(UtilModelChecker.java:150)
	at epmc.modelchecker.UtilModelChecker.buildLowLevel(UtilModelChecker.java:169)
	at epmc.modelchecker.ModelChecker.prepareLowLevel(ModelChecker.java:222)
	at epmc.modelchecker.ModelChecker.checkProperty(ModelChecker.java:247)
	at epmc.modelchecker.ModelChecker.check(ModelChecker.java:192)
	at epmc.command.CommandTaskCheck.executeInServer(CommandTaskCheck.java:67)
	at epmc.jani.interaction.Analyse.execute(Analyse.java:111)
	at epmc.jani.interaction.commandline.StartInConsoleJaniInteractionNoJani.execute(StartInConsoleJaniInteractionNoJani.java:91)
	at epmc.jani.interaction.commandline.StartInConsoleJaniInteractionNoJani.process(StartInConsoleJaniInteractionNoJani.java:68)
	at epmc.main.EPMC.main(EPMC.java:52)