Re: [tlaplus] Using pcal.trans to write to different file

Well, I failed in covering all of the special cases!!!

For example, a spec file that contains the keyword MODULE at its beginning will cause my method to not operate correctly.

Therefore, the code has to be modified to ignore the occurrences of the keyword MODULE without the enclosing ---- characters.

AmirHossein

On Thu, Jul 4, 2019, 2:33 AM Amir Hossein Sayyad Abdi <amir.ahsa.2011@xxxxxxxxx> wrote:

Hi Andrew,

I just wrote a java method that performs the cloning of an original TLA+ spec by changing its MODULE name to a new specified name. I have tried to cover as many "special cases" as I could think of. You may use this method in your future feature's implementation!

The attached java file contains the method and it is commented as well. I hope it is helpful.

Sincerely,
AmirHossein

On Wed, Jul 3, 2019 at 10:11 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
Quick question - when I use "java pcal.trans specname.tla", it modifies the specname.tla file and writes the original contents to specname.old; is there a way to leave specname.tla untouched and specify an output file containing the translated PlusCal?

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1828bef7-a959-4521-b6ee-f3ad90fdaa31%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.