Hello,
I have made a small patch to TLC -dump option, which outputs state fingerprint and transition information to TLC -dump file,
and a ruby script 'tla2dot', which parses the dump file and outputs graphviz dot notation.
The patch, the pathced tla2tools.jar, and the ruby script are available in https://github.com/jarjuk/tla2dot under MIT licences.
I have used the tool only in small scale mainly to better understand state space generation, and to communicate, how tla2tool works.
Is it be possible to add the patch https://github.com/jarjuk/tla2dot/blob/master/tla2dot.patch to tlatools trunk?
BR,
Jukka
On Sunday, December 13, 2015 at 4:38:50 PM UTC+2, Stephan Merz wrote:
TLC explores the entire graph of reachable states of the instance you give it to verify. If no error is found, the Toolbox displays some quantitative information, including how many states TLC visited and coverage information about the underlying specification. It does not visualize the entire state space, if that's what you mean.
Regards,
Stephan
> On 13 Dec 2015, at 14:25, sawsa...@xxxxxxxxx wrote:
>
> Hello
> I am working on TLA in order to analyze the filters in Dynamic networks, how can I see the states and the results of TLC models checking if there no error trace>
> Second question: I am working on windows not linux, is that a reason for not finding TLC Trace viewer? cause I dwonloaded the zip file but still I could not find a way to see the results or save it
> Thank you in advance
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.