java.lang.StackOverflowError during Model Parsing

[nixbg]

Hi,

I have an automatically generated prism model with 21862 states and
between 3 to 8 transitions per state. The code is 190667 lines. When I
attempt to check the model, prism gives the following error:

Exception in thread "main" java.lang.StackOverflowError
at parser.visitor.ASTTraverseModify.visitPre(ASTTraverseModify.java:
397)
at parser.visitor.ASTTraverseModify.visit(ASTTraverseModify.java:400)
at parser.ast.ExpressionBinaryOp.accept(ExpressionBinaryOp.java:214)
at parser.visitor.ASTTraverseModify.visit(ASTTraverseModify.java:401)
at parser.ast.ExpressionBinaryOp.accept(ExpressionBinaryOp.java:214)

With the last two lines repeated many times. I tried increasing both
PRISM_JAVAMAXMEM and the cudd memory but the problem persists. I am
wondering if I can try anything else. Any tips are welcome!

Nikolay

[Artur Rataj]

It seems that the parser runs out of stack size for your large input file.

You may enlarge the stack by adding -Xss8192m or the like into the last line of bin/prism, after "$PRISM_JAVA".

Cheers,
Artur

[nixbg]

Artur,

Thank you so much for your response! Increasing the stack size solved
the problem.

The model building time was 6 hours for the following model size:

States: 21862 (1 initial)
Transitions: 314422
Choices: 168796

Transition matrix: 110636 nodes (25 terminal), 314422 minterms, vars:
15r/15c/8nd

Is this normal or is there a way to speed it up?

Nikolay

[Dave Parker]

> Is this normal or is there a way to speed it up?

For a situation like this where the model description itself is very big
(190667 lines), it is quite common to be slow, yes.

Is the model auto-generated somehow? If so, you could consider importing
the transition matrix directly:

http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

But there are some limitations on the kind of model checking that you
can do, this way.

Dave.

[wang...@gmail.com]

Hi Artur:

I encounter the same problem. But I didn't find such place to insert -Xss8192m in bin/prism or "$PRISM_JAVA".

Can you tell me the exact location to insert such an option?

Best regards,

Jingyi

[Dave Parker]

Dear Jingyi,

On Linux/Mac, look for the line starting "$PRISM_JAVA" near the end of
the file bin/prism and add -Xss8192m directly after "$PRISM_JAVA". In
the latest version (4.3), you can instead just change the value of
PRISM_JAVASTACKSIZE further up in bin/prism.

On Windows, look for the last line (starting 'java') in bin/prism.bat,
or the line starting 'start "PRISM" javaw' near the end of bin/prism.bat.

Best wishes,

Dave.

> --
> 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 prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.