[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to read the graph generated by TLC? Is there a way to specify its location?



Hi Stephan,
Thank you very much for your answer.
I tried the -metadir option and it works.
Ouiza

On Friday, 9 November 2012 11:06:08 UTC-5, Stephan Merz wrote:
Hello Ouiza,

I don't know the reply to your first question. In any case, there is no existing tool that would allow you to analyze the graph, so you'd have to look at the TLC code to interpret the data.

For the second question, you can specify the directory using the -metadir option of TLC when you run it from the command line. (You can download the command-line version from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html). There does not (yet) seem to be a way to pass such parameters to TLC from the Toolbox, but Leslie announced that this will come in a future version.

Hope this helps,
Stephan

On Nov 9, 2012, at 4:52 PM, Ouiza <dou...@xxxxxxxxx> wrote:

Hi everyone,
I have 2 questions related to the graph generated by TLC in the states directory:
1) Is there any way to read it?
2) Is there a way to specify to TLC where to create the states directory, I am running it in a network environment with the "workers" option and I want it to write in the local space of the machine where it's being run, by default it's writing in my home directory.

Thanks and best regards,
Ouiza

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
To unsubscribe from this group, send email to tlaplus+u...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.