[tlaplus] Re: Internal Error while translating PlusCal to TLA+

[jack malkovick <sillymouse333@xxxxxxxxx>]

A similar issue seems to affect the TLA+ parser SANY

Starting SANY...
Parsing file ...\MC.tla
Parsing file ...\Model_1\Spec.tla
Labels added.

Fatal errors while parsing TLA+ spec in file MC

java.lang.ArrayIndexOutOfBoundsException: Index 107 out of bounds for length 107
SANY finished.

On Thursday, February 8, 2024 at 3:40:20 PM UTC+2 jack malkovick wrote:

I see that PlusCal's AST.java has this declaration

public static int[] curIndent =  {0, 0, ...}

That has 106 hard-coded 0 elements. This is the reason for failure, my spec makes it reach the 107 element. Could it be updated to a higher value?

On Thursday, February 8, 2024 at 2:35:54 PM UTC+2 jack malkovick wrote:

While I'm translating my PlusCal spec I get this stack trace.

I've got the stack trace after in Toolbox translation failed silently, and then I've run it with the command line

java -cp tla2tools.jar pcal.trans mySpec.tla

Any ideas?

pcal.trans Version 1.11 of 31 December 2020
Labels added.
Parsing completed.
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: Index 107 out of bounds for length 107
at pcal.AST.Indent(AST.java:972)
at pcal.AST.VectorToSeqString(AST.java:1001)
at pcal.AST$Assign.toString(AST.java:539)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST.VectorOfVectorsToSeqString(AST.java:1041)
at pcal.AST$Either.toString(AST.java:642)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST.VectorOfVectorsToSeqString(AST.java:1041)
at pcal.AST$Either.toString(AST.java:642)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST.VectorOfVectorsToSeqString(AST.java:1041)
at pcal.AST$Either.toString(AST.java:642)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST.VectorOfVectorsToSeqString(AST.java:1041)
at pcal.AST$Either.toString(AST.java:642)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST.VectorOfVectorsToSeqString(AST.java:1041)
at pcal.AST$Either.toString(AST.java:642)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:626)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$If.toString(AST.java:629)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$LabelIf.toString(AST.java:740)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$While.toString(AST.java:524)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$LabeledStmt.toString(AST.java:502)
at pcal.AST.VectorToSeqString(AST.java:1006)
at pcal.AST$Uniprocess.toString(AST.java:257)
at pcal.trans.performTranslation(trans.java:1015)
at pcal.trans.performTranslation(trans.java:576)
at pcal.trans.runMe(trans.java:374)
at pcal.trans.main(trans.java:305)

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c25157a1-73af-4924-80e9-bfe015226cdan%40googlegroups.com.