(TLAPS) ptl_to_trp source code?

[Gianluca Guida <glg...@xxxxxxxxx>]

Hello,

I am not entirely convinced this is the right list to ask this question, but I read on the TLAPS FAQ that I should be encouraged to discuss about TLAPS in this list, so here it goes.

I am compiling TLAPS from scratch, backends included, as I am interested in running the system on OpenBSD -- so far the only non-trivial part has been adding OpenBSD support to PolyML.

examples/cantor/* are successfully running. I am having trouble in proofs that require PTL, as I get this error message:

    /bin/sh: ptl_to_trp: not found

Digging a bit on the code it seems that this is a necessary step to run ls4, and that ptl_to_trp code is taken in the tlaps-release.sh script from:

    svn+ssh://${MSR_SVN_USER}@svn.msr-inria.inria.fr/var/lib/svn/repository/t
la/trunk/translate

It doesn't seem to exist an anonymous svn access from that server. Is the code publicly available? Is there something I am missing? Do I really need it?

I am quite new to TLAPS, so apologies in case the question is trivial.

Thanks in advance,
Gianluca