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

Re: [tlaplus] Run TLC model checker in Azure


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,

On Friday, January 19, 2018 at 8:40:14 AM UTC-8 kapi...@xxxxxxxxx wrote:
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.

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/e5432be2-4bfa-4bde-9900-96e39e8bd0a1n%40googlegroups.com.