[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Add some TLC debug info : An internal error occurred during: "Azure". java.lang.NullPointerException

On 14.12.20 00:07, Earnshaw wrote:

在2020年12月14日星期一 UTC+8 下午4:01:20<Earnshaw> 写道:


    Iam trying to learn how to run a spec in cloud based distributed mode.
    So I config TLC to inter-operate wuth Azure according to the user Help.

      no matter how simple the spec I tried to run is, the result is
    always  "java.lang.NullPointerException" , and I can't get any more

       The Tool Box version is 1.7.1 and JRE version is 8

      Below is my test spec . Can some body give me some advices?

      Thanks in advance

    -------------------------------- MODULE GCD
    EXTENDS Sequences, Integers, TLC, FiniteSets,  Naturals

    CONSTANT xque

    VARIABLE queue

    Init == /\ queue = xque

    Next == /\ queue # <<>>
            /\ queue' = <<1,2>>

I've opened https://github.com/tlaplus/tlaplus/issues/552 to track this issue. Please attach the *full* log file there.


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/d8409c86-4c96-c3b3-2e79-c4e2bda4da77%40lemmster.de.