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, |