Run TLC model checker in Azure

47 views
Skip to first unread message

Kapil Agarwal

unread,
Jan 18, 2018, 1:50:23 PM1/18/18
to tlaplus
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

unread,
Jan 18, 2018, 2:52:04 PM1/18/18
to tla...@googlegroups.com
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

unread,
Jan 18, 2018, 4:47:17 PM1/18/18
to tla...@googlegroups.com
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

unread,
Jan 19, 2018, 11:40:14 AM1/19/18
to tla...@googlegroups.com
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.
Reply all
Reply to author
Forward
0 new messages