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

[Markus Kuppe]

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