[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> 写道：



    Hello,

    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
    information.

       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. 

Thanks,
Markus

--
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.