Import existing TLA files

[Alexander Bakst]

Hi all,

I wrote a couple TLA files using a text editor that for the sake of anonymity we will call vimacs. I'd like to import them into the TLA Toolbox, however I can't quite figure out how to do that -- is there a way other than creating a new spec then copying/pasting the files that I wrote in vimacs?

Thanks,

Alexander

[Markus Kuppe]

File > Open Spec > Add New Spec... > Browse - Select the root module of
a set of modules > Finish

Markus

[Carl Thuringer]

The toolbox makes this confusing. 

1. File > Open Spec > Add New Spec... > Browse - select the .tla file which you want to create models for. 

2. "MySpec.tla already exists, do you want to replace it?" : This is misleading. It will not replace the spec. Just click 'replace'.

3. If you're re-importing a forgotten module, ensure 'Import Existing Models' is checked.

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ec5e901d-8a75-6cc2-4b94-359c14c27744%40lemmster.de.

--

Cheers,

Carl Thuringer

[Alexander Bakst]

Aha, thanks Markus and Carl. Yes, rather confusing — also, the file appears greyed out. But chugging along does indeed import the file.

—Alexander

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAGFfb%3Da0syqi-nOnX_FZaRziRsQL9TZCGanJshtRTixZXsnFzg%40mail.gmail.com.

[Markus Kuppe]

On 01.05.20 09:02, Alexander Bakst wrote:
> Aha, thanks Markus and Carl. Yes, rather confusing — also, the file
> appears greyed out. But chugging along does indeed import the file.
>

Hi Alexander, Hi Carl,

would either one of you please open an issue [1] that outlines a
workflow that you think is less confusing. Please include the OS you
are on because the file chooser is OS-specific.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues

[Alexander Bakst]

Sure, I’ll do so right now.

> [1] https://urldefense.com/v3/__https://github.com/tlaplus/tlaplus/issues__;!!Mih3wA!XNjKg-42J1V5Ac-aVG6C82aEcSL_MwROOI-gJE4_v_Zvtg-wXeWzp94Cg862J2IQ$

>
> --
> 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 view this discussion on the web visit https://urldefense.com/v3/__https://groups.google.com/d/msgid/tlaplus/002529a1-5620-7201-94ee-42f2a083e646*40lemmster.de__;JQ!!Mih3wA!XNjKg-42J1V5Ac-aVG6C82aEcSL_MwROOI-gJE4_v_Zvtg-wXeWzp94Cg9KHePrK$ .