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

[tlaplus] An internal error occurred during: "Azure". java.lang.NullPointerException


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



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/46e140cf-7f67-41c9-8afc-ec72d700871fn%40googlegroups.com.