CTMC, 'StackOverflow'

[Yingke Chen]

Hi, PRISM

I am checking a tree-shape CTMC properties.

However, the following exception keep popping up (almost always).

Could you please provide me some suggestions?  Many  thanks.

The model file and the property file are attached below.

This model has around 2k states. 

Thanks,

Exception in thread "main" java.lang.StackOverflowError

at explicit.StateModelChecker.checkExpression(StateModelChecker.java:352)

at explicit.NonProbModelChecker.checkExpression(NonProbModelChecker.java:63)

at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:459)

at explicit.StateModelChecker.checkExpressionBinaryOp(StateModelChecker.java:445)

at explicit.StateModelChecker.checkExpression(StateModelChecker.java:352)

at explicit.NonProbModelChecker.checkExpression(NonProbModelChecker.java:63)

at explicit.ProbModelChecker.checkExpression(ProbModelChecker.java:459)

at explicit.StateModelChecker.checkExpressionBinaryOp(StateModelChecker.java:445)

Yingke

[Marcin Copik]

Hi Yingke,

it seems that your model description is very large. Have you tried increasing the stack size? The solution is described on Prism's website:
http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/MemoryProblems#memout_parse

Best regards,

Marcin

--
You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchecker+unsubscribe@googlegroups.com.
To post to this group, send email to prismmodelchecker@googlegroups.com.
Visit this group at http://groups.google.com/group/prismmodelchecker.
For more options, visit https://groups.google.com/d/optout.