Using pcal.trans to write to different file

[Andrew Helwer]

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?

[Hillel Wayne]

I don't believe there is. Anything that did this would also have to change the module name to match the new file. 

H

On Wed, Jul 3, 2019, 12:41 PM Andrew Helwer <andrew...@gmail.com> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.

[Leslie Lamport]

Hi Andrew,

It would take about 10 minutes to add an option to write the output to specname.new, plus about 15 minutes to find where options are handled and where the output file is written.  As Hillel points out, if you want the output to be written to new .tla file, the module name should be changed.  It would take 10 minutes to program that so it works 99.9% of the time.  Making it work right all the time would be somewhat more difficult.  You're welcome to submit an implementation of such a feature.

Leslie

On Wednesday, July 3, 2019 at 11:35:10 AM UTC-7, Hillel Wayne wrote:

I don't believe there is. Anything that did this would also have to change the module name to match the new file. 

H

On Wed, Jul 3, 2019, 12:41 PM Andrew Helwer <andrew.helwer atxx domain name gmail.com> 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 atxx  googlegroups.com.
To post to this group, send email to tlaplus atxx googlegroups.com.

[Amir Hossein Sayyad Abdi]

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...@gmail.com> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.

[Amir Hossein Sayyad Abdi]

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