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