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

[Markus <tlaplus-go...@xxxxxxxxxxx>]

On Wednesday, November 14, 2012 5:22:33 PM UTC+1, Ouiza wrote:
> Hi Markus! 
>  I am not used with plugins and to save time, I would like to know if I can run your code outside of Eclipse.
>  I had a look at it and saw that I need packages which I expect to be in the plugins directory under toolbox. When I tried to run javac on your java files, I got this as the first error: 
> org/lamport/tla/toolbox/tool/tlc/ui/trace/TLCTraceFileModelProvider.java:6: package org.lamport.tla.toolbox.util does not exist
> import org.lamport.tla.toolbox.util.RCPNameToFileIStream 

Hi Ouiza,

no, you won't be able to run the code outside the Toolbox or Eclipse. And even running it in the Toolbox requires one to install additional dependencies (GEF zest).

I actually posted the code as a reference on how to parse/read the .st file, not for you to execute it (the UI part won't scale to more than ~10^2 states anyway). The interesting bits are in TLCTraceFileModelProvider.java. Btw. all tlc2.* and util.* imports are part of the Tools distribution [1].

Thanks
Markus

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html