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

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



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


 

--
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/74388273-1c8d-4b8c-bdcb-13e22d3bcd82n%40googlegroups.com.