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

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

On 09/27/2013 04:07 PM, Amira Methni wrote:
> Hi Markus,
> I want to display graph generated by TLC but i don't understand how your plugin 
> works.
> Could you explain to me how can i execute it and what it takes as entry.

Hi Amira,

I have made a special build available [1] that comes with the TLC Trace
File Viewer installed. Just grab a zip for your architecture.

You can open the corresponding TLC Trace Viewer via "CTRL+3" and
typing "Trace File Viewer" [2]. The view that opens up has an "Open
Trace" in its view menu [3] where you are prompted for trace and spec.

The input it takes are the trace file (.st) with all (explored) states
and the original spec.

Do not expect the graph to scale beyond a few states though (I have
never tried it on more the 100 states).

HTH
Markus

PS: If there is demand, the trace viewer could easily be added to the
next toolbox release.

[1] https://tla.msr-inria.inria.fr/kuppe/traceviewer
[2]
https://tla.msr-inria.inria.fr/kuppe/traceviewer/OpenTLCTraceFileViewer.png
[3] https://tla.msr-inria.inria.fr/kuppe/traceviewer/OpenTraceAndSpec.png