Run TLC model checker in Azure

[Kapil Agarwal]

Hi

I am trying to run TLA+ model checker in Azure. Following the guide at https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/index.html, I have set up the certificate and environment variables. I get the following error on running the model checker-

"Could not setup any viable authentication method "

Any help is appreciated.

Thanks

Kapil

[Markus Alexander Kuppe]

Hi Kapil,

are you on Windows 10 and can you privately send me the .log file
located in your home directory under .tlaplus/.metadata/? Also is your
SSH key protected by a passphrase? Lastly, did you upgrade to Toolbox
1.5.5 from an earlier version or did you start fresh by downloading a
Toolbox 1.5.5 zip file?

Thanks

Markus

[Kapil]

Hi Markus

I sent you an email for the same.

Thanks

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/BLp-AJhw3K8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Kapil Agarwal]

Thanks Markus for the help.

I was able to get this running by using version 1.5.6 of the toolbox and by ensuring that there were no whitespaces in the path to the pkcs12 key.

[Chris Ortiz]

Hello,

I am new to TLA+/TLC and I am trying the HourClock example from Leslie Lamport's Specifying Systems book. I was able to run it on the Toolbox. The next thing I was trying is if I can run it on Azure with our subscription. I followed all the instruction in the How To Run for Azure. It connected and created resources in our Azure account. The toolbox later on bailed out with Problem Occurred discussing about exception in java on the code SkuNotAvailable with message that the requested sized for resource is currently not available in location eastus zone. I believe it is asking for Standard_D14 VM resource. I am wondering if anyone have successfully tried the Toolbox to run in Azure recently or is there anything I would need to setup in my Toolbox or Azure account. Kindly advise. We believe TLA+/TLC is important to our process but we will need the help of the cloud for it.  I really appreciate the help on this matter. 

Best regards,

Chris