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