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

[Ouiza <dou...@xxxxxxxxx>]

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

Thank you for your help.
 
Best regards,
Ouiza

On Friday, 9 November 2012 16:10:31 UTC-5, Markus  wrote:

On Friday, November 9, 2012 4:52:00 PM UTC+1, Ouiza 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?

Hi Ouiza,

https://tla.msr-inria.inria.fr/kuppe/org.lamport.tla.toolbox.tool.tlc.ui.trace.zip is the code I hacked a while ago to recreate a visual state graph from the .st file. That might serve as an inspiration.

HTH
Markus